From 9cbf1d55e5781fdae8ec64f18b9edb5f15b732f8 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 31 Oct 2018 20:57:37 +0100 Subject: [PATCH] revert changes to support z3 4.5 --- mythril/analysis/modules/integer.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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])