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

Differently than the bit vector addition, an overflowed bit vector
multiplication does not necessarily result in a value less than any
of its operands (e.g., the multiplication of two 8-bit vectors 0x7 and
4 produces 0xC). Fix this issue by using Z3 BVMulNoOverflow in 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 = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0))
     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: