diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 8916ed13..aea9ff06 100644 --- a/mythril/analysis/modules/integer.py +++ b/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])