From 5334f72b4bb0b1f9152fb4c3360b89cb24fe8aa5 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Sun, 25 Nov 2018 16:34:01 +0530
Subject: [PATCH 01/16] Use previous solver to recalculate

---
 mythril/laser/ethereum/state/constraints.py | 34 ++++++++++++++++++---
 mythril/laser/ethereum/svm.py               |  5 +++
 2 files changed, 35 insertions(+), 4 deletions(-)

diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py
index ed676521..b047583e 100644
--- a/mythril/laser/ethereum/state/constraints.py
+++ b/mythril/laser/ethereum/state/constraints.py
@@ -1,3 +1,7 @@
+from z3 import Solver, unsat
+from copy import copy
+
+
 class Constraints(list):
     """
     This class should maintain a solver and it's constraints, This class tries to make the Constraints() object
@@ -7,29 +11,51 @@ class Constraints(list):
 
     def __init__(self, constraint_list=None, solver=None, possibility=None):
         super(Constraints, self).__init__(constraint_list or [])
-        self.solver = solver
+        self.solver = solver or Solver()
+        self.solver.set("timeout", 1)
         self.__possibility = possibility
 
     def check_possibility(self):
-        return True
+        if self.__possibility is None:
+            self.__possibility = (self.solver.check() != unsat)
+        if self.__possibility is False:
+            self.solver = None
+        return self.__possibility
 
     def append(self, constraint):
+        self.__possibility = None
         super(Constraints, self).append(constraint)
+        if self.solver is not None:
+            self.solver.add(constraint)
 
     def pop(self, index=-1):
         raise NotImplementedError
 
     def __copy__(self):
         constraint_list = super(Constraints, self).copy()
-        return Constraints(constraint_list)
+        if self.solver is not None:
+            solver = copy(self.solver)
+        else:
+            solver = None
+        return Constraints(constraint_list, solver)
 
     def __deepcopy__(self, memodict=None):
         return self.__copy__()
 
     def __add__(self, constraints):
         constraints_list = super(Constraints, self).__add__(constraints)
-        return Constraints(constraint_list=constraints_list)
+        if self.solver is not None:
+            solver = copy(self.solver)
+            for constraint in constraints:
+                solver.add(constraint)
+        else:
+            solver = None
+        return Constraints(constraint_list=constraints_list, solver=solver)
 
     def __iadd__(self, constraints):
         super(Constraints, self).__iadd__(constraints)
+        if self.solver is None:
+            return self
+        for constraint in constraints:
+            self.solver.add(constraint)
         return self
diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index 8bd38ef2..14f0dea6 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -189,6 +189,9 @@ class LaserEVM:
             except NotImplementedError:
                 logging.debug("Encountered unimplemented instruction")
                 continue
+
+            new_states = [state for state in new_states if state.mstate.constraints.check_possibility()]
+
             self.manage_cfg(op_code, new_states)
 
             if new_states:
@@ -196,6 +199,8 @@ class LaserEVM:
             elif track_gas:
                 final_states.append(global_state)
             self.total_states += len(new_states)
+            del global_state.mstate.constraints.solver
+
         return final_states if track_gas else None
 
     def execute_state(

From f6dbd95cb566423aa573ecccd2259aceb69e27a0 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Sun, 25 Nov 2018 16:38:14 +0530
Subject: [PATCH 02/16] Reformat files with black

---
 mythril/laser/ethereum/state/constraints.py | 2 +-
 mythril/laser/ethereum/svm.py               | 6 +++++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py
index b047583e..e3254d35 100644
--- a/mythril/laser/ethereum/state/constraints.py
+++ b/mythril/laser/ethereum/state/constraints.py
@@ -17,7 +17,7 @@ class Constraints(list):
 
     def check_possibility(self):
         if self.__possibility is None:
-            self.__possibility = (self.solver.check() != unsat)
+            self.__possibility = self.solver.check() != unsat
         if self.__possibility is False:
             self.solver = None
         return self.__possibility
diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index 14f0dea6..70dc6d2c 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -190,7 +190,11 @@ class LaserEVM:
                 logging.debug("Encountered unimplemented instruction")
                 continue
 
-            new_states = [state for state in new_states if state.mstate.constraints.check_possibility()]
+            new_states = [
+                state
+                for state in new_states
+                if state.mstate.constraints.check_possibility()
+            ]
 
             self.manage_cfg(op_code, new_states)
 

From 2a2b4767fbb61d658a4092db6289b8e3901dc479 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Thu, 29 Nov 2018 20:33:39 +0530
Subject: [PATCH 03/16] Add global state split block

---
 mythril/laser/ethereum/instructions.py       | 54 +++++++++++---------
 mythril/laser/ethereum/state/constraints.py  |  9 ++--
 mythril/laser/ethereum/state/global_state.py | 10 ++++
 3 files changed, 44 insertions(+), 29 deletions(-)

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 4cbc06c5..ccc6b60a 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -150,7 +150,6 @@ class Instruction:
 
         if instruction_mutator is None:
             raise NotImplementedError
-
         return instruction_mutator(global_state)
 
     @StateTransition()
@@ -1089,47 +1088,54 @@ class Instruction:
             simplify(Not(condition)) if type(condition) == BoolRef else condition == 0
         )
 
-        if (type(negated) == bool and negated) or (
-            type(negated) == BoolRef and not is_false(negated)
-        ):
-            new_state = copy(global_state)
+        # True case
+        condi = simplify(condition) if type(condition) == BoolRef else condition != 0
+
+        # Get jump destination
+        index = util.get_instruction_index(disassembly.instruction_list, jump_addr)
+
+        negated_cond = (type(negated) == bool and negated) or ( type(negated) == BoolRef and not is_false(negated))
+        positive_cond = (type(condi) == bool and condi) or ( type(condi) == BoolRef and not is_false(condi) )
+        branched = False
+
+        if index and negated_cond and positive_cond:
+            new_state1, new_state2 = global_state.split_global_state()
+        else:
+            new_state1, new_state2 = copy(global_state), copy(global_state)
+
+        if negated_cond:
             # add JUMPI gas cost
-            new_state.mstate.min_gas_used += min_gas
-            new_state.mstate.max_gas_used += max_gas
+            new_state1.mstate.min_gas_used += min_gas
+            new_state1.mstate.max_gas_used += max_gas
 
             # manually increment PC
-            new_state.mstate.depth += 1
-            new_state.mstate.pc += 1
-            new_state.mstate.constraints.append(negated)
-            states.append(new_state)
+            new_state1.mstate.depth += 1
+            new_state1.mstate.pc += 1
+            new_state1.mstate.constraints.append(negated)
+            states.append(new_state1)
         else:
             logging.debug("Pruned unreachable states.")
 
         # True case
 
-        # Get jump destination
-        index = util.get_instruction_index(disassembly.instruction_list, jump_addr)
         if not index:
             logging.debug("Invalid jump destination: " + str(jump_addr))
             return states
 
         instr = disassembly.instruction_list[index]
 
-        condi = simplify(condition) if type(condition) == BoolRef else condition != 0
         if instr["opcode"] == "JUMPDEST":
-            if (type(condi) == bool and condi) or (
-                type(condi) == BoolRef and not is_false(condi)
-            ):
-                new_state = copy(global_state)
+            if positive_cond:
+                new_state2 = copy(global_state)
                 # add JUMPI gas cost
-                new_state.mstate.min_gas_used += min_gas
-                new_state.mstate.max_gas_used += max_gas
+                new_state2.mstate.min_gas_used += min_gas
+                new_state2.mstate.max_gas_used += max_gas
 
                 # manually set PC to destination
-                new_state.mstate.pc = index
-                new_state.mstate.depth += 1
-                new_state.mstate.constraints.append(condi)
-                states.append(new_state)
+                new_state2.mstate.pc = index
+                new_state2.mstate.depth += 1
+                new_state2.mstate.constraints.append(condi)
+                states.append(new_state2)
             else:
                 logging.debug("Pruned unreachable states.")
         del global_state
diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py
index e3254d35..317ce2a5 100644
--- a/mythril/laser/ethereum/state/constraints.py
+++ b/mythril/laser/ethereum/state/constraints.py
@@ -33,11 +33,10 @@ class Constraints(list):
 
     def __copy__(self):
         constraint_list = super(Constraints, self).copy()
-        if self.solver is not None:
-            solver = copy(self.solver)
-        else:
-            solver = None
-        return Constraints(constraint_list, solver)
+        return Constraints(constraint_list, self.solver)
+
+    def copy_solver(self):
+        self.solver = copy(self.solver)
 
     def __deepcopy__(self, memodict=None):
         return self.__copy__()
diff --git a/mythril/laser/ethereum/state/global_state.py b/mythril/laser/ethereum/state/global_state.py
index b8dad5d7..ef47887b 100644
--- a/mythril/laser/ethereum/state/global_state.py
+++ b/mythril/laser/ethereum/state/global_state.py
@@ -75,3 +75,13 @@ class GlobalState:
     def new_bitvec(self, name: str, size=256) -> BitVec:
         transaction_id = self.current_transaction.id
         return BitVec("{}_{}".format(transaction_id, name), size)
+
+    def split_global_state(self):
+        global_state1 = copy(self)
+        global_state2 = copy(self)
+
+        global_state1.mstate.constraints.copy_solver()
+        global_state2.mstate.constraints.copy_solver()
+
+        return global_state1, global_state2
+

From bbd2dc52d8218574aa686bd28f0faa941e1164ff Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Thu, 29 Nov 2018 20:38:04 +0530
Subject: [PATCH 04/16] Set solver to None after usage

---
 mythril/laser/ethereum/svm.py | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index 70dc6d2c..fb37322a 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -203,7 +203,9 @@ class LaserEVM:
             elif track_gas:
                 final_states.append(global_state)
             self.total_states += len(new_states)
+            
             del global_state.mstate.constraints.solver
+            global_state.mstate.constraints.solver = None
 
         return final_states if track_gas else None
 

From ac2e801d2bf30d751d9d25c611ced6d3e1237980 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Thu, 29 Nov 2018 20:40:21 +0530
Subject: [PATCH 05/16] Black fixes

---
 mythril/laser/ethereum/instructions.py       | 8 ++++++--
 mythril/laser/ethereum/state/global_state.py | 1 -
 mythril/laser/ethereum/svm.py                | 2 +-
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index abcc1d75..a99aedbc 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -1092,8 +1092,12 @@ class Instruction:
         # Get jump destination
         index = util.get_instruction_index(disassembly.instruction_list, jump_addr)
 
-        negated_cond = (type(negated) == bool and negated) or ( type(negated) == BoolRef and not is_false(negated))
-        positive_cond = (type(condi) == bool and condi) or ( type(condi) == BoolRef and not is_false(condi) )
+        negated_cond = (type(negated) == bool and negated) or (
+            type(negated) == BoolRef and not is_false(negated)
+        )
+        positive_cond = (type(condi) == bool and condi) or (
+            type(condi) == BoolRef and not is_false(condi)
+        )
         branched = False
 
         if index and negated_cond and positive_cond:
diff --git a/mythril/laser/ethereum/state/global_state.py b/mythril/laser/ethereum/state/global_state.py
index 6585ef03..e52e6778 100644
--- a/mythril/laser/ethereum/state/global_state.py
+++ b/mythril/laser/ethereum/state/global_state.py
@@ -87,4 +87,3 @@ class GlobalState:
         global_state2.mstate.constraints.copy_solver()
 
         return global_state1, global_state2
-
diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index fb37322a..3d2a1bc4 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -203,7 +203,7 @@ class LaserEVM:
             elif track_gas:
                 final_states.append(global_state)
             self.total_states += len(new_states)
-            
+
             del global_state.mstate.constraints.solver
             global_state.mstate.constraints.solver = None
 

From cbe8f7eb259603c4e33c2d7dfa087d3fe4df5d1a Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Mon, 31 Dec 2018 11:13:06 +0530
Subject: [PATCH 06/16] Just send constraint list to nodes

---
 mythril/laser/ethereum/transaction/symbolic.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py
index 117322d8..9d2ed029 100644
--- a/mythril/laser/ethereum/transaction/symbolic.py
+++ b/mythril/laser/ethereum/transaction/symbolic.py
@@ -118,7 +118,7 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None:
         )
 
         global_state.mstate.constraints += transaction.world_state.node.constraints
-        new_node.constraints = global_state.mstate.constraints
+        new_node.constraints = global_state.mstate.constraints[:]
 
     global_state.world_state.transaction_sequence.append(transaction)
     global_state.node = new_node

From 5ca8dec4be40c19cb298b27e7cc760bbaca6f909 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Thu, 24 Jan 2019 13:59:34 +0530
Subject: [PATCH 07/16] Remove solver per branch and dynamically construct
 solver

---
 mythril/laser/ethereum/instructions.py       |  5 +--
 mythril/laser/ethereum/state/constraints.py  | 41 +++++++-------------
 mythril/laser/ethereum/state/global_state.py |  9 -----
 3 files changed, 15 insertions(+), 40 deletions(-)

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 410db672..93cdcfb8 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -1494,10 +1494,7 @@ class Instruction:
         )
         branched = False
 
-        if index and negated_cond and positive_cond:
-            new_state1, new_state2 = global_state.split_global_state()
-        else:
-            new_state1, new_state2 = copy(global_state), copy(global_state)
+        new_state1, new_state2 = copy(global_state), copy(global_state)
 
         if negated_cond:
             new_state = copy(global_state)
diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py
index 22bd2c67..dab6ca07 100644
--- a/mythril/laser/ethereum/state/constraints.py
+++ b/mythril/laser/ethereum/state/constraints.py
@@ -1,8 +1,8 @@
 """This module contains the class used to represent state-change constraints in
 the call graph."""
 
-from z3 import Solver, unsat
-from copy import copy
+from mythril.laser.smt import Solver
+from z3 import unsat
 
 
 class Constraints(list):
@@ -13,23 +13,23 @@ class Constraints(list):
     TODO: add the solver to this class after callback refactor
     """
 
-    def __init__(self, constraint_list=None, solver=None, possibility=None):
+    def __init__(self, constraint_list=None, possibility=None):
         """
 
         :param constraint_list:
-        :param solver:
         :param possibility:
         """
         super(Constraints, self).__init__(constraint_list or [])
-        self.solver = solver or Solver()
-        self.solver.set("timeout", 1)
         self.__possibility = possibility
 
     def check_possibility(self):
-        if self.__possibility is None:
-            self.__possibility = self.solver.check() != unsat
-        if self.__possibility is False:
-            self.solver = None
+        if self.__possibility is not None:
+            return self.__possibility
+        solver = Solver()
+        solver.set_timeout(10)
+        for constraint in self[:]:
+            solver.add(constraint)
+        self.__possibility = solver.check() != unsat
         return self.__possibility
 
     def append(self, constraint):
@@ -38,8 +38,7 @@ class Constraints(list):
         :param constraint:
         """
         super(Constraints, self).append(constraint)
-        if self.solver is not None:
-            self.solver.add(constraint.raw)
+        self.__possibility = None
 
     def pop(self, index=-1):
         """
@@ -54,10 +53,7 @@ class Constraints(list):
         :return:
         """
         constraint_list = super(Constraints, self).copy()
-        return Constraints(constraint_list, self.solver)
-
-    def copy_solver(self):
-        self.solver = copy(self.solver)
+        return Constraints(constraint_list, possibility=self.__possibility)
 
     def __deepcopy__(self, memodict=None):
         """
@@ -74,13 +70,7 @@ class Constraints(list):
         :return:
         """
         constraints_list = super(Constraints, self).__add__(constraints)
-        if self.solver is not None:
-            solver = copy(self.solver)
-            for constraint in constraints:
-                solver.add(constraint.raw)
-        else:
-            solver = None
-        return Constraints(constraint_list=constraints_list, solver=solver)
+        return Constraints(constraint_list=constraints_list, possibility=None)
 
     def __iadd__(self, constraints):
         """
@@ -89,8 +79,5 @@ class Constraints(list):
         :return:
         """
         super(Constraints, self).__iadd__(constraints)
-        if self.solver is None:
-            return self
-        for constraint in constraints:
-            self.solver.add(constraint.raw)
+        self.__possibility = None
         return self
diff --git a/mythril/laser/ethereum/state/global_state.py b/mythril/laser/ethereum/state/global_state.py
index 2c228fae..8facc663 100644
--- a/mythril/laser/ethereum/state/global_state.py
+++ b/mythril/laser/ethereum/state/global_state.py
@@ -114,15 +114,6 @@ class GlobalState:
         transaction_id = self.current_transaction.id
         return symbol_factory.BitVecSym("{}_{}".format(transaction_id, name), size)
 
-    def split_global_state(self):
-        global_state1 = copy(self)
-        global_state2 = copy(self)
-
-        global_state1.mstate.constraints.copy_solver()
-        global_state2.mstate.constraints.copy_solver()
-
-        return global_state1, global_state2
-
     def annotate(self, annotation: StateAnnotation) -> None:
         """
 

From 792adf884dcb1ff1bb0752e36f73f1a485c431d7 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Thu, 24 Jan 2019 14:17:16 +0530
Subject: [PATCH 08/16] Add type hints and function documentation for the class

---
 mythril/laser/ethereum/state/constraints.py | 64 ++++++++++++---------
 1 file changed, 36 insertions(+), 28 deletions(-)

diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py
index dab6ca07..b8fdfd90 100644
--- a/mythril/laser/ethereum/state/constraints.py
+++ b/mythril/laser/ethereum/state/constraints.py
@@ -1,7 +1,9 @@
 """This module contains the class used to represent state-change constraints in
 the call graph."""
 
-from mythril.laser.smt import Solver
+from mythril.laser.smt import Solver, Bool
+
+from typing import List, Optional
 from z3 import unsat
 
 
@@ -10,74 +12,80 @@ class Constraints(list):
     tries to make the Constraints() object as a simple list of constraints with
     some background processing.
 
-    TODO: add the solver to this class after callback refactor
     """
 
-    def __init__(self, constraint_list=None, possibility=None):
+    def __init__(
+        self,
+        constraint_list: Optional[List[Bool]] = None,
+        is_possible: Optional[bool] = None,
+    ) -> None:
         """
 
-        :param constraint_list:
-        :param possibility:
+        :param constraint_list: List of constraints
+        :param is_possible: Whether it is possible to satisfy the constraints or not
         """
         super(Constraints, self).__init__(constraint_list or [])
-        self.__possibility = possibility
+        self.__default_timeout = 10
+        self.__is_possible = is_possible
 
-    def check_possibility(self):
-        if self.__possibility is not None:
-            return self.__possibility
+    def check_possibility(self) -> bool:
+        """
+        :return: True/False based on the existence of solution of constraints
+        """
+        if self.__is_possible is not None:
+            return self.__is_possible
         solver = Solver()
-        solver.set_timeout(10)
+        solver.set_timeout(self.__default_timeout)
         for constraint in self[:]:
             solver.add(constraint)
-        self.__possibility = solver.check() != unsat
-        return self.__possibility
+        self.__is_possible = solver.check() != unsat
+        return self.__is_possible
 
-    def append(self, constraint):
+    def append(self, constraint: Bool) -> None:
         """
 
-        :param constraint:
+        :param constraint: The constraint to be appended
         """
         super(Constraints, self).append(constraint)
-        self.__possibility = None
+        self.__is_possible = None
 
-    def pop(self, index=-1):
+    def pop(self, index: int = -1) -> None:
         """
 
-        :param index:
+        :param index: Index to be popped from the list
         """
         raise NotImplementedError
 
-    def __copy__(self):
+    def __copy__(self) -> "Constraints":
         """
 
-        :return:
+        :return: The copied constraint List
         """
         constraint_list = super(Constraints, self).copy()
-        return Constraints(constraint_list, possibility=self.__possibility)
+        return Constraints(constraint_list, is_possible=self.__is_possible)
 
-    def __deepcopy__(self, memodict=None):
+    def __deepcopy__(self, memodict=None) -> "Constraints":
         """
 
         :param memodict:
-        :return:
+        :return: The copied constraint List
         """
         return self.__copy__()
 
-    def __add__(self, constraints):
+    def __add__(self, constraints: List[Bool]) -> "Constraints":
         """
 
         :param constraints:
-        :return:
+        :return: the new list after the + operation
         """
         constraints_list = super(Constraints, self).__add__(constraints)
-        return Constraints(constraint_list=constraints_list, possibility=None)
+        return Constraints(constraint_list=constraints_list, is_possible=None)
 
-    def __iadd__(self, constraints):
+    def __iadd__(self, constraints: List[Bool]) -> None:
         """
 
         :param constraints:
         :return:
         """
         super(Constraints, self).__iadd__(constraints)
-        self.__possibility = None
-        return self
+        self.__is_possible = None

From fcddf06e985a579e09b1a0cba2e1f905fd4c3625 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Thu, 24 Jan 2019 14:26:48 +0530
Subject: [PATCH 09/16] Clean up instructions.py and refactor with black

---
 mythril/laser/ethereum/instructions.py        | 30 ++++++++-----------
 mythril/laser/ethereum/state/constraints.py   |  9 +++++-
 mythril/laser/ethereum/svm.py                 |  2 --
 .../laser/ethereum/transaction/symbolic.py    |  2 +-
 4 files changed, 22 insertions(+), 21 deletions(-)

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 93cdcfb8..02a97a51 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -1492,21 +1492,18 @@ class Instruction:
         positive_cond = (type(condi) == bool and condi) or (
             isinstance(condi, Bool) and not is_false(condi)
         )
-        branched = False
-
-        new_state1, new_state2 = copy(global_state), copy(global_state)
 
         if negated_cond:
             new_state = copy(global_state)
             # add JUMPI gas cost
-            new_state1.mstate.min_gas_used += min_gas
-            new_state1.mstate.max_gas_used += max_gas
+            new_state.mstate.min_gas_used += min_gas
+            new_state.mstate.max_gas_used += max_gas
 
             # manually increment PC
-            new_state1.mstate.depth += 1
-            new_state1.mstate.pc += 1
-            new_state1.mstate.constraints.append(negated)
-            states.append(new_state1)
+            new_state.mstate.depth += 1
+            new_state.mstate.pc += 1
+            new_state.mstate.constraints.append(negated)
+            states.append(new_state)
         else:
             log.debug("Pruned unreachable states.")
 
@@ -1520,19 +1517,18 @@ class Instruction:
 
         if instr["opcode"] == "JUMPDEST":
             if positive_cond:
-                new_state2 = copy(global_state)
+                new_state = copy(global_state)
                 # add JUMPI gas cost
-                new_state2.mstate.min_gas_used += min_gas
-                new_state2.mstate.max_gas_used += max_gas
+                new_state.mstate.min_gas_used += min_gas
+                new_state.mstate.max_gas_used += max_gas
 
                 # manually set PC to destination
-                new_state2.mstate.pc = index
-                new_state2.mstate.depth += 1
-                new_state2.mstate.constraints.append(condi)
-                states.append(new_state2)
+                new_state.mstate.pc = index
+                new_state.mstate.depth += 1
+                new_state.mstate.constraints.append(condi)
+                states.append(new_state)
             else:
                 log.debug("Pruned unreachable states.")
-        del global_state
         return states
 
     @StateTransition()
diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py
index b8fdfd90..bf0808ee 100644
--- a/mythril/laser/ethereum/state/constraints.py
+++ b/mythril/laser/ethereum/state/constraints.py
@@ -56,6 +56,12 @@ class Constraints(list):
         """
         raise NotImplementedError
 
+    def get_list(self) -> List[Bool]:
+        """
+        :return: returns the list of constraints
+        """
+        return self[:]
+
     def __copy__(self) -> "Constraints":
         """
 
@@ -81,7 +87,7 @@ class Constraints(list):
         constraints_list = super(Constraints, self).__add__(constraints)
         return Constraints(constraint_list=constraints_list, is_possible=None)
 
-    def __iadd__(self, constraints: List[Bool]) -> None:
+    def __iadd__(self, constraints: List[Bool]) -> "Constraints":
         """
 
         :param constraints:
@@ -89,3 +95,4 @@ class Constraints(list):
         """
         super(Constraints, self).__iadd__(constraints)
         self.__is_possible = None
+        return self
diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index 9bd66116..27818c13 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -255,8 +255,6 @@ class LaserEVM:
                 final_states.append(global_state)
             self.total_states += len(new_states)
 
-            global_state.mstate.constraints.solver = None
-
         return final_states if track_gas else None
 
     def _add_world_state(self, global_state: GlobalState):
diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py
index a4c77116..bb33ebfa 100644
--- a/mythril/laser/ethereum/transaction/symbolic.py
+++ b/mythril/laser/ethereum/transaction/symbolic.py
@@ -133,7 +133,7 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None:
             )
 
         global_state.mstate.constraints += transaction.world_state.node.constraints
-        new_node.constraints = global_state.mstate.constraints[:]
+        new_node.constraints = global_state.mstate.constraints.get_list()
 
     global_state.world_state.transaction_sequence.append(transaction)
     global_state.node = new_node

From cb0156c5208ea8784cf46d6145dbf24f4362162c Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Thu, 24 Jan 2019 14:47:02 +0530
Subject: [PATCH 10/16] Move back the index variable in instructions.py

---
 mythril/laser/ethereum/instructions.py | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 02a97a51..37fa177b 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -1483,9 +1483,6 @@ class Instruction:
         condi = simplify(condition) if isinstance(condition, Bool) else condition != 0
         condi.simplify()
 
-        # Get jump destination
-        index = util.get_instruction_index(disassembly.instruction_list, jump_addr)
-
         negated_cond = (type(negated) == bool and negated) or (
             isinstance(negated, Bool) and not is_false(negated)
         )
@@ -1509,6 +1506,9 @@ class Instruction:
 
         # True case
 
+        # Get jump destination
+        index = util.get_instruction_index(disassembly.instruction_list, jump_addr)
+
         if not index:
             log.debug("Invalid jump destination: " + str(jump_addr))
             return states

From 7656287409fbf0c91fd1aa9afc32dc5b7653497d Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Tue, 29 Jan 2019 15:46:18 +0530
Subject: [PATCH 11/16] Change get_list() to as_list()

---
 mythril/laser/ethereum/state/constraints.py    | 3 ++-
 mythril/laser/ethereum/transaction/symbolic.py | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py
index bf0808ee..ad07fc09 100644
--- a/mythril/laser/ethereum/state/constraints.py
+++ b/mythril/laser/ethereum/state/constraints.py
@@ -56,7 +56,8 @@ class Constraints(list):
         """
         raise NotImplementedError
 
-    def get_list(self) -> List[Bool]:
+    @property
+    def as_list(self) -> List[Bool]:
         """
         :return: returns the list of constraints
         """
diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py
index bb33ebfa..802fe580 100644
--- a/mythril/laser/ethereum/transaction/symbolic.py
+++ b/mythril/laser/ethereum/transaction/symbolic.py
@@ -133,7 +133,7 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None:
             )
 
         global_state.mstate.constraints += transaction.world_state.node.constraints
-        new_node.constraints = global_state.mstate.constraints.get_list()
+        new_node.constraints = global_state.mstate.constraints.as_list()
 
     global_state.world_state.transaction_sequence.append(transaction)
     global_state.node = new_node

From 25346d32c10834453b7996870b245bcc95916f96 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Tue, 29 Jan 2019 15:58:13 +0530
Subject: [PATCH 12/16] remove the paranthesis for as_list

---
 mythril/laser/ethereum/transaction/symbolic.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py
index 802fe580..a827623e 100644
--- a/mythril/laser/ethereum/transaction/symbolic.py
+++ b/mythril/laser/ethereum/transaction/symbolic.py
@@ -133,7 +133,7 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None:
             )
 
         global_state.mstate.constraints += transaction.world_state.node.constraints
-        new_node.constraints = global_state.mstate.constraints.as_list()
+        new_node.constraints = global_state.mstate.constraints.as_list
 
     global_state.world_state.transaction_sequence.append(transaction)
     global_state.node = new_node

From 2b98ae7163a1415bd816ef26b818847f06c235dd Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Tue, 29 Jan 2019 19:07:02 +0530
Subject: [PATCH 13/16] Remove __

---
 mythril/laser/ethereum/state/constraints.py | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py
index ad07fc09..36116b24 100644
--- a/mythril/laser/ethereum/state/constraints.py
+++ b/mythril/laser/ethereum/state/constraints.py
@@ -25,21 +25,21 @@ class Constraints(list):
         :param is_possible: Whether it is possible to satisfy the constraints or not
         """
         super(Constraints, self).__init__(constraint_list or [])
-        self.__default_timeout = 10
-        self.__is_possible = is_possible
+        self._default_timeout = 100
+        self._is_possible = is_possible
 
     def check_possibility(self) -> bool:
         """
         :return: True/False based on the existence of solution of constraints
         """
-        if self.__is_possible is not None:
-            return self.__is_possible
+        if self._is_possible is not None:
+            return self._is_possible
         solver = Solver()
-        solver.set_timeout(self.__default_timeout)
+        solver.set_timeout(self._default_timeout)
         for constraint in self[:]:
             solver.add(constraint)
-        self.__is_possible = solver.check() != unsat
-        return self.__is_possible
+        self._is_possible = solver.check() != unsat
+        return self._is_possible
 
     def append(self, constraint: Bool) -> None:
         """
@@ -47,7 +47,7 @@ class Constraints(list):
         :param constraint: The constraint to be appended
         """
         super(Constraints, self).append(constraint)
-        self.__is_possible = None
+        self._is_possible = None
 
     def pop(self, index: int = -1) -> None:
         """
@@ -69,7 +69,7 @@ class Constraints(list):
         :return: The copied constraint List
         """
         constraint_list = super(Constraints, self).copy()
-        return Constraints(constraint_list, is_possible=self.__is_possible)
+        return Constraints(constraint_list, is_possible=self._is_possible)
 
     def __deepcopy__(self, memodict=None) -> "Constraints":
         """
@@ -95,5 +95,5 @@ class Constraints(list):
         :return:
         """
         super(Constraints, self).__iadd__(constraints)
-        self.__is_possible = None
+        self._is_possible = None
         return self

From f9aafe8a9fa497130808422067a9422afdbaf24d Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Thu, 31 Jan 2019 22:33:12 +0530
Subject: [PATCH 14/16] Add a execution-time require checker flag

---
 mythril/analysis/solver.py            | 11 +++++++----
 tests/laser/evm_testsuite/evm_test.py |  3 ++-
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 2eb057f6..98d3633a 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -13,18 +13,21 @@ import logging
 log = logging.getLogger(__name__)
 
 
-def get_model(constraints, minimize=(), maximize=()):
+def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True):
     """
 
     :param constraints:
     :param minimize:
     :param maximize:
+    :param enforce_execution_time: Bool variable which enforces --execution-timeout's time
     :return:
     """
     s = Optimize()
-    timeout = min(100000, time_handler.time_remaining() - 500)
-    if timeout <= 0:
-        raise UnsatError
+    timeout = 100000
+    if enforce_execution_time:
+        timeout = min(timeout, time_handler.time_remaining() - 500)
+        if timeout <= 0:
+            raise UnsatError
     s.set_timeout(timeout)
     for constraint in constraints:
         if type(constraint) == bool and not constraint:
diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py
index 4f32cc6d..6227b3ce 100644
--- a/tests/laser/evm_testsuite/evm_test.py
+++ b/tests/laser/evm_testsuite/evm_test.py
@@ -127,7 +127,8 @@ def test_vmtest(
         assert len(laser_evm.open_states) == 1
         world_state = laser_evm.open_states[0]
         model = get_model(
-            next(iter(laser_evm.nodes.values())).states[0].mstate.constraints
+            next(iter(laser_evm.nodes.values())).states[0].mstate.constraints,
+            enforce_execution_time=False,
         )
 
         for address, details in post_condition.items():

From 49027947584fd1a972fd6ae642483b248880b048 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Fri, 1 Feb 2019 16:53:09 +0530
Subject: [PATCH 15/16] Change Constraints.check_possibility() to
 Constraints.is_possible

---
 mythril/laser/ethereum/state/constraints.py | 3 ++-
 mythril/laser/ethereum/svm.py               | 4 +---
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py
index 36116b24..e13e13c4 100644
--- a/mythril/laser/ethereum/state/constraints.py
+++ b/mythril/laser/ethereum/state/constraints.py
@@ -28,7 +28,8 @@ class Constraints(list):
         self._default_timeout = 100
         self._is_possible = is_possible
 
-    def check_possibility(self) -> bool:
+    @property
+    def is_possible(self) -> bool:
         """
         :return: True/False based on the existence of solution of constraints
         """
diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index 47cda5a8..f70312f7 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -235,9 +235,7 @@ class LaserEVM:
                 continue
 
             new_states = [
-                state
-                for state in new_states
-                if state.mstate.constraints.check_possibility()
+                state for state in new_states if state.mstate.constraints.is_possible
             ]
 
             self.manage_cfg(op_code, new_states)

From 26e6e1777be41be28c2f43c189c061b2261690ed Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Mon, 4 Feb 2019 14:20:13 +0530
Subject: [PATCH 16/16] Fix typehint for __iadd__

---
 mythril/laser/ethereum/state/constraints.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py
index e13e13c4..b967ea8e 100644
--- a/mythril/laser/ethereum/state/constraints.py
+++ b/mythril/laser/ethereum/state/constraints.py
@@ -3,7 +3,7 @@ the call graph."""
 
 from mythril.laser.smt import Solver, Bool
 
-from typing import List, Optional
+from typing import Iterable, List, Optional
 from z3 import unsat
 
 
@@ -89,7 +89,7 @@ class Constraints(list):
         constraints_list = super(Constraints, self).__add__(constraints)
         return Constraints(constraint_list=constraints_list, is_possible=None)
 
-    def __iadd__(self, constraints: List[Bool]) -> "Constraints":
+    def __iadd__(self, constraints: Iterable[Bool]) -> "Constraints":
         """
 
         :param constraints: