From d0c00eef9c44ccb6714a8b620228ca5a9835f69d Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Sat, 29 Sep 2018 20:23:33 +0530
Subject: [PATCH] Support operators + and += for Constraints()

---
 mythril/analysis/solver.py      |  2 +-
 mythril/laser/ethereum/state.py | 16 ++++++----------
 2 files changed, 7 insertions(+), 11 deletions(-)

diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 721b5d91..317e1e0e 100644
--- a/mythril/analysis/solver.py
+++ b/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()
diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py
index 40acce37..86c72be1 100644
--- a/mythril/laser/ethereum/state.py
+++ b/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:
-            self.__possibility = (self.solver.check() != unsat)
-        return self.__possibility
+        if self.__possibility in (None, unknown):
+            self.__possibility = self.solver.check()
+        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 Constraints(constraint_list, self.solver, self.__possibility)
+        return self.__copy__()
 
     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):
-        """
-        Implement constraint concatenation if needed
-        """
-        raise NotImplementedError
+        return self.__add__(other)
 
 
 class MachineStack(list):