Fix some cases

mythril/analysis/modules/exceptions.py

@@ -43,7 +43,6 @@ class ReachableExceptionsModule(DetectionModule):
         :param state:
         :return:
         """
-        print("SHIT ASSERT")
         log.debug("ASSERT_FAIL in function " + state.environment.active_function_name)
 
         try:
@@ -74,7 +73,6 @@ class ReachableExceptionsModule(DetectionModule):
                 transaction_sequence=transaction_sequence,
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
             )
-            print(state.mstate.constraints)
             return [issue]
 
         except UnsatError:

mythril/analysis/solver.py

@@ -152,7 +152,6 @@ def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction):
         address = ""
         input_ = transaction.code.bytecode
     else:
-        print(transaction.call_data._calldata.raw)
         input_ = "".join(
             [
                 hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:]

mythril/laser/ethereum/instructions.py

@@ -1368,10 +1368,7 @@ class Instruction:
 
         state = global_state.mstate
         index = state.stack.pop()
-
         state.stack.append(global_state.environment.active_account.storage[index])
-        if global_state.get_current_instruction()['address'] == 357:
-            print(state.stack[-1])
         return [global_state]
 
     @StateTransition()

mythril/laser/ethereum/state/account.py

@@ -122,7 +122,6 @@ class ArrayStorageRegion(StorageRegion):
         storage, is_keccak_storage = self._get_corresponding_storage(key)
         if is_keccak_storage:
             key = self._sanitize(key.input_)
-
         storage[key] = value
 
     def __deepcopy__(self, memodict=dict()):
@@ -180,7 +179,6 @@ class Storage:
 
     @staticmethod
     def _array_condition(key: BitVec):
-
         return (
             not isinstance(key, BitVecFunc)
             or (
@@ -193,7 +191,6 @@ class Storage:
     def __getitem__(self, key: BitVec) -> BitVec:
         ite_get = self._ite_region[cast(BitVecFunc, key)]
         array_get = self._array_region[key]
-        print(If(ite_get, ite_get, array_get))
         return If(ite_get, ite_get, array_get)
 
     def __setitem__(self, key: BitVec, value: Any) -> None:

mythril/laser/ethereum/state/environment.py

@@ -5,6 +5,7 @@ from typing import Dict
 from z3 import ExprRef
 
 from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.constraints import Constraints
 from mythril.laser.ethereum.state.calldata import BaseCalldata
 from mythril.laser.smt import symbol_factory
 
@@ -22,6 +23,7 @@ class Environment:
         callvalue: ExprRef,
         origin: ExprRef,
         code=None,
+        constraints=None,
     ) -> None:
         """
 

mythril/laser/smt/bitvecfunc.py

@@ -67,12 +67,13 @@ def _comparison_helper(
         if operation == z3.ULT:
             operation = operator.lt
         return Bool(z3.BoolVal(operation(a.value, b.value)), annotations=union)
-    #if not isinstance(b, BitVecFunc) and a.potential_value:
-    #    condition = False
-    #    for value, cond in a.potential_value:
-    #        if value is not None:
-    #            condition = Or(condition, And(b == value, cond))
-    #    return And(condition, operation(a.raw, b.raw))
+
+    if not isinstance(b, BitVecFunc) and a.potential_value:
+        condition = False
+        for value, cond in a.potential_value:
+            if value is not None:
+                condition = Or(condition, And(b == value, cond))
+        return And(condition, operation(a.raw, b.raw))
     if (
         not isinstance(b, BitVecFunc)
         or not a.func_name