Merge branch 'develop' into hzzhang/fix-bvmul-overflow-check

mythril/analysis/modules/integer.py

@@ -131,11 +131,8 @@ def _try_constraints(constraints, new_constraints):
     Tries new constraints
     :return Model if satisfiable otherwise None
     """
-    _constraints = copy.deepcopy(constraints)
-    for constraint in new_constraints:
-        _constraints.append(copy.deepcopy(constraint))
     try:
-        model = solver.get_model(_constraints)
+        model = solver.get_model(constraints + new_constraints)
         return model
     except UnsatError:
         return None

mythril/analysis/modules/transaction_order_dependence.py

@@ -1,5 +1,6 @@
 import logging
 import re
+import copy
 
 from mythril.analysis import solver
 from mythril.analysis.ops import *

mythril/laser/ethereum/instructions.py

@@ -18,7 +18,6 @@ from z3 import (
     URem,
     SRem,
     BitVec,
-    Solver,
     is_true,
     BitVecVal,
     If,
@@ -43,7 +42,6 @@ from mythril.laser.ethereum.transaction import (
     TransactionStartSignal,
     ContractCreationTransaction,
 )
-from mythril.analysis.solver import get_model
 
 TT256 = 2 ** 256
 TT256M1 = 2 ** 256 - 1
@@ -924,9 +922,6 @@ class Instruction:
             storage_keys = global_state.environment.active_account.storage.keys()
             keccak_keys = filter(keccak_function_manager.is_keccak, storage_keys)
 
-            solver = Solver()
-            solver.set(timeout=1000)
-
             results = []
             new = False
 
@@ -934,7 +929,7 @@ class Instruction:
                 key_argument = keccak_function_manager.get_argument(keccak_key)
                 index_argument = keccak_function_manager.get_argument(index)
 
-                if is_true(key_argument == index_argument):
+                if is_true(simplify(key_argument == index_argument)):
                     return self._sstore_helper(
                         copy(global_state),
                         keccak_key,