From 972d5974c0160494942e0ee46025fb78e4c309ba Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Wed, 27 Mar 2019 00:19:22 +0530 Subject: [PATCH 1/2] Use the current state constraints over the constraint at the annotation time --- mythril/analysis/modules/integer.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 94b3588b..8c460394 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -290,7 +290,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): try: transaction_sequence = solver.get_transaction_sequence( - state, node.constraints + [annotation.constraint] + state, state.node.constraints + [annotation.constraint] ) except UnsatError: continue From 9c22872a72af25c4d61d2f6e72a4d7d16495a094 Mon Sep 17 00:00:00 2001 From: JoranHonig Date: Thu, 28 Mar 2019 15:37:59 +0530 Subject: [PATCH 2/2] Use mstate over node constraints Co-Authored-By: norhh --- mythril/analysis/modules/integer.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 8c460394..d98ed069 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -290,7 +290,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): try: transaction_sequence = solver.get_transaction_sequence( - state, state.node.constraints + [annotation.constraint] + state, state.mstate.constraints + [annotation.constraint] ) except UnsatError: continue