From 9485ee458798703409126a150f4d66410dee008e Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 23 Jul 2018 18:38:49 +0200
Subject: [PATCH] save

---
 mythril/analysis/modules/exceptions.py | 2 --
 mythril/analysis/modules/integer.py    | 4 +++-
 mythril/analysis/solver.py             | 4 ++--
 mythril/laser/ethereum/instructions.py | 7 +++----
 mythril/laser/ethereum/state.py        | 7 ++++++-
 mythril/laser/ethereum/svm.py          | 2 +-
 6 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/mythril/analysis/modules/exceptions.py b/mythril/analysis/modules/exceptions.py
index 507bbd49..fc287948 100644
--- a/mythril/analysis/modules/exceptions.py
+++ b/mythril/analysis/modules/exceptions.py
@@ -24,9 +24,7 @@ def execute(statespace):
         for state in node.states:
 
             instruction = state.get_current_instruction()
-
             if(instruction['opcode'] == "ASSERT_FAIL"):
-
                 try:
                     model = solver.get_model(node.constraints)
                     address = state.get_current_instruction()['address']
diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py
index e21dbb58..25282e2c 100644
--- a/mythril/analysis/modules/integer.py
+++ b/mythril/analysis/modules/integer.py
@@ -30,6 +30,7 @@ def execute(statespace):
         node = statespace.nodes[k]
 
         for state in node.states:
+            # pass
             issues += _check_integer_underflow(statespace, state, node)
             issues += _check_integer_overflow(statespace, state, node)
 
@@ -50,6 +51,8 @@ def _check_integer_overflow(statespace, state, node):
     instruction = state.get_current_instruction()
     if instruction['opcode'] not in ("ADD", "MUL"):
         return issues
+    if instruction['address'] != 755:
+        return issues
 
     # Formulate overflow constraints
     stack = state.mstate.stack
@@ -108,7 +111,6 @@ def _verify_integer_overflow(statespace, node, expr, state, model, constraint, o
 
     return _try_constraints(node.constraints, [Not(constraint)]) is not None
 
-
 def _try_constraints(constraints, new_constraints):
     """
     Tries new constraints
diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 0f6703e6..01633956 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -4,7 +4,7 @@ import logging
 
 def get_model(constraints):
     s = Solver()
-    s.set("timeout", 10000)
+    s.set("timeout", 100000)
 
     for constraint in constraints:
         s.add(constraint)
@@ -12,7 +12,7 @@ def get_model(constraints):
     if result == sat:
         return s.model()
     elif result == unknown:
-        logging.info("Timeout encountered while solving expression using z3")
+        logging.error("Timeout encountered while solving expression using z3")
     raise UnsatError
 
 
diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 2db3adf7..c97a5ebd 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -778,7 +778,7 @@ class Instruction:
                 new_state = copy(global_state)
                 new_state.mstate.pc = index
                 new_state.mstate.depth += 1
-                new_state.mstate.constraints.append(condi)
+                new_state.mstate.constraints.append(simplify(condi))
 
                 states.append(new_state)
             else:
@@ -786,12 +786,11 @@ class Instruction:
 
         # False case
         negated = Not(condition) if type(condition) == BoolRef else condition == 0
-        sat = not is_false(simplify(negated)) if type(condi) == BoolRef else not negated
 
-        if sat:
+        if (type(negated) == bool and negated) or (type(negated) == BoolRef and not is_false(simplify(negated))):
             new_state = copy(global_state)
             new_state.mstate.depth += 1
-            new_state.mstate.constraints.append(negated)
+            new_state.mstate.constraints.append(simplify(negated))
             states.append(new_state)
         else:
             logging.debug("Pruned unreachable states.")
diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py
index 7cb865b6..07951f6a 100644
--- a/mythril/laser/ethereum/state.py
+++ b/mythril/laser/ethereum/state.py
@@ -39,7 +39,12 @@ class Account:
         self.balance += balance
 
     def get_storage(self, index):
-        return self.storage[index] if index in self.storage.keys() else BitVec("storage_" + str(index), 256)
+        if index in self.storage.keys():
+            return self.storage[index]
+        else:
+            symbol = BitVec("storage_" + str(index), 256)
+            self.storage[index] = symbol
+            return symbol
 
     @property
     def as_dict(self):
diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index 1f54e6f2..98a0ba9d 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -70,7 +70,7 @@ class LaserEVM:
             try:
                 new_states, op_code = self.execute_state(global_state)
             except NotImplementedError:
-                logging.debug("Encountered unimplemented instruction")
+                logging.error("Encountered unimplemented instruction: {}".format(op_code))
                 continue
 
             if len(new_states) == 0: