fix: smt encoding for evm div-by-zero

[daejunpark]

Fix the SMT encoding of division (and modulo) by zero.

In EVM, division (and modulo) by zero is defined to be zero, whereas they are defined differently in SMT-LIB.

Thus, the EVM division (evm_bvudiv_N x y) should be encoded as:

(ite (= y (_ bv0 N)) (_ bv0 N) (bvudiv x y))

where N is the bitsize. The EVM modulo operation should be encoded similarly.

[daejunpark]

Can be merged after #340

[karmacoma-eth]

it would be nice to have a test that demonstrates the issue that this fixes. What about this?

    function check_Div(uint num, uint256 den) public pure {
        vm.assume(num > den);
        uint256 y;

        assembly {
            y := div(num, den)
        }

        assert(y != 0);
    }

We currently get

# of potential paths involving assertion violations: 1 / 2  (--solver-threads 20)
  Checking again with refinement
  Invalid path; ignored (path id: 1)
[PASS] check_Div(uint256,uint256) (paths: 2, time: 12.51s (paths: 0.03s, models: 12.49s), bounds: [])

but we should get a counterexample with den == 0, right?

[daejunpark]

new tests are added: a5199df

[karmacoma-eth]

neat, thank you!