Support operators + and += for Constraints()

mythril/analysis/solver.py

@@ -5,7 +5,7 @@ import logging
 
 def get_model(constraints):
 
-    constraints.solver.set("timeout", 10000)
+    constraints.solver.set("timeout", 100000)
     result = constraints.solver.check()
     if result == sat:
         return constraints.solver.model()

mythril/laser/ethereum/state.py

@@ -1,4 +1,4 @@
-from z3 import BitVec, BitVecVal, Solver, ExprRef, sat, unsat
+from z3 import BitVec, BitVecVal, Solver, unsat, unknown
 from mythril.disassembler.disassembly import Disassembly
 from copy import copy, deepcopy
 from enum import Enum
@@ -140,9 +140,9 @@ class Constraints(list):
                 self.solver.add(constraint)
 
     def check_possibility(self):
-        if self.__possibility is None:
+        if self.__possibility in (None, unknown):
-            self.__possibility = (self.solver.check() != unsat)
+            self.__possibility = self.solver.check()
-        return self.__possibility
+        return self.__possibility != unsat
 
     def append(self, constraint):
         self.__possibility = None
@@ -158,8 +158,7 @@ class Constraints(list):
         return Constraints(constraint_list, self.solver, self.__possibility)
 
     def __deepcopy__(self, memodict={}):
-        constraint_list = super(Constraints, self).copy()
+        return self.__copy__()
-        return Constraints(constraint_list, self.solver, self.__possibility)
 
     def __add__(self, constraints):
         constraints_list = super(Constraints, self).__add__(constraints)
@@ -169,10 +168,7 @@ class Constraints(list):
         return Constraints(constraint_list=constraints_list, solver=new_solver)
 
     def __iadd__(self, other):
-        """
+        return self.__add__(other)
-        Implement constraint concatenation if needed
-        """
-        raise NotImplementedError
 
 
 class MachineStack(list):