revert changes to support z3 4.5

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))
+        # constraint = Not(BVAddNoOverflow(op0, op1, signed=False))
     else:
         expr = op1 * op0
-        constraint = Not(BVMulNoOverflow(op0, op1, signed=False))
+        # constraint = Not(BVMulNoOverflow(op0, op1, signed=False))
 
+    constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0))
     # Check satisfiable
     model = _try_constraints(node.constraints, [constraint])