From 247648df7acb1cb6f888bd7e2ad71d2ffe553d70 Mon Sep 17 00:00:00 2001
From: Bernhard Mueller <bernhard.mueller11@gmail.com>
Date: Thu, 9 Nov 2017 18:54:06 +0700
Subject: [PATCH] Add solver timeout

---
 mythril/analysis/modules/unchecked_suicide.py | 2 +-
 mythril/analysis/solver.py                    | 3 ++-
 mythril/analysis/symbolic.py                  | 9 ++++++---
 3 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/mythril/analysis/modules/unchecked_suicide.py b/mythril/analysis/modules/unchecked_suicide.py
index b1f7e5ae..2777b9e5 100644
--- a/mythril/analysis/modules/unchecked_suicide.py
+++ b/mythril/analysis/modules/unchecked_suicide.py
@@ -57,7 +57,7 @@ def execute(statespace):
                             for s in statespace.sstors[index]:
 
                                 if s.tainted:
-                                    can_write = Trues
+                                    can_write = True
 
                                     issue.description += "\nThere is a check on storage index " + str(index) + ". This storage index can be written to by calling the function '" + s.node.function_name + "'."
                                     break
diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 89b616a5..868253c8 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -3,6 +3,7 @@ from mythril.exceptions import UnsatError
 
 def get_model(constraints):
     s = Solver()
+    s.set("timeout", 2000)
 
     for constraint in constraints:
         s.add(constraint)
@@ -12,5 +13,5 @@ def get_model(constraints):
         return s.model()
 
     else:
-            raise UnsatError
+        raise UnsatError
 
diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py
index 41382e11..0899bc57 100644
--- a/mythril/analysis/symbolic.py
+++ b/mythril/analysis/symbolic.py
@@ -69,19 +69,22 @@ class StateSpace:
 
     def sstor_analysis(self):
 
-        logging.debug("Analyzing storage operations...")
+        logging.info("Analyzing storage operations...")
 
         for index in self.sstors:
             for s in self.sstors[index]:
 
                 # For now we simply 'taint' every storage location that is reachable without any constraint on msg.sender
 
+                taint = True
+
                 for constraint in s.node.constraints:
-                    logging.debug("Constraint: " + str(constraint))
+                    # logging.debug("Constraint: " + str(constraint))
                     if ("caller" in str(constraint)):
-                        s.tainted = False
+                        taint = False
                         break
 
+                if taint:
                     try:
                         solver.get_model(s.node.constraints)
                         s.tainted = True