Merge pull request #648 from hzzhang/hzzhang/fix-bvmul-overflow-check

analysis/integer: fix the overflow check of bit vector multiplication

mythril/analysis/modules/integer.py

@@ -72,11 +72,12 @@ def _check_integer_overflow(statespace, state, node):
     # Formulate expression
     if instruction["opcode"] == "ADD":
         expr = op0 + op1
+        constraint = Not(BVAddNoOverflow(op0, op1, signed=False))
     else:
         expr = op1 * op0
+        constraint = Not(BVMulNoOverflow(op0, op1, signed=False))
 
     # Check satisfiable
-    constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0))
     model = _try_constraints(node.constraints, [constraint])
 
     if model is None:

requirements.txt

@@ -24,5 +24,5 @@ pytest_mock
 requests
 rlp>=1.0.1
 transaction>=2.2.1
-z3-solver>=4.5
+z3-solver>=4.8
 pysha3

setup.py

@@ -75,7 +75,7 @@ setup(
     install_requires=[
         "coloredlogs>=10.0",
         "ethereum>=2.3.2",
-        "z3-solver>=4.5",
+        "z3-solver>=4.8",
         "requests",
         "py-solc",
         "plyvel",