From 4046047c512c11e92ea815d326f10a680e03ecac Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Mon, 16 Sep 2019 13:34:33 -0300
Subject: [PATCH 01/37] Unsound symbolication and asorted fixes

---
 examples/evm/minimal.py                    |   2 +-
 examples/script/concolic.py                |   2 +
 manticore/core/manticore.py                |  43 +-
 manticore/core/smtlib/constraints.py       |  27 +-
 manticore/core/smtlib/expression.py        |  43 +-
 manticore/core/smtlib/operators.py         |   9 +-
 manticore/core/smtlib/solver.py            | 107 ++--
 manticore/core/smtlib/visitors.py          | 225 ++++++--
 manticore/core/state.py                    |  27 +-
 manticore/ethereum/__init__.py             |   3 +-
 manticore/ethereum/abi.py                  |  34 +-
 manticore/ethereum/account.py              |   3 +
 manticore/ethereum/cli.py                  |   2 +-
 manticore/ethereum/detectors.py            |   6 +-
 manticore/ethereum/manticore.py            | 642 ++++++++++++---------
 manticore/ethereum/plugins.py              |   4 +-
 manticore/native/manticore.py              |   4 +-
 manticore/platforms/evm.py                 | 262 +++++----
 manticore/utils/event.py                   |   9 +-
 scripts/travis_test.sh                     |  14 +-
 tests/ethereum/test_consensys_benchmark.py |   6 +-
 tests/ethereum/test_detectors.py           |   8 +-
 tests/ethereum/test_general.py             |  95 +--
 23 files changed, 913 insertions(+), 664 deletions(-)

diff --git a/examples/evm/minimal.py b/examples/evm/minimal.py
index 6c7e456c3..df3fc3670 100644
--- a/examples/evm/minimal.py
+++ b/examples/evm/minimal.py
@@ -1,4 +1,4 @@
-from manticore.ethereum import ManticoreEVM
+from manticore import ManticoreEVM
 
 ################ Script #######################
 
diff --git a/examples/script/concolic.py b/examples/script/concolic.py
index a46afaef8..23043645e 100755
--- a/examples/script/concolic.py
+++ b/examples/script/concolic.py
@@ -72,6 +72,8 @@ def flip(constraint):
     assert len(equal.operands) == 2
     # assume they are the equal -> ite form that we produce on standard branches
     ite, forcepc = equal.operands
+    if not (isinstance(ite, BitVecITE) and isinstance(forcepc, BitVecConstant)):
+        return constraint
     assert isinstance(ite, BitVecITE) and isinstance(forcepc, BitVecConstant)
     assert len(ite.operands) == 3
     cond, iifpc, eelsepc = ite.operands
diff --git a/manticore/core/manticore.py b/manticore/core/manticore.py
index b20241d44..62c49dec0 100644
--- a/manticore/core/manticore.py
+++ b/manticore/core/manticore.py
@@ -549,6 +549,31 @@ def _kill_state(self, state_id, delete=False):
         # wake up everyone waiting for a change in the state lists
         self._lock.notify_all()
 
+    @sync
+    def kill_state(self, state, delete=False):
+        """ Kill a state.
+             A state is moved from any list to the kill list or fully
+             removed from secondary storage
+
+            :param state_id: a estate id
+            :type state_id: int
+            :param delete: if true remove the state from the secondary storage
+            :type delete: bool
+        """
+        state_id = state.id
+        if state_id in self._busy_states:
+            self._busy_states.remove(state_id)
+        if state_id in self._terminated_states:
+            self._terminated_states.remove(state_id)
+        if state_id in self._ready_states:
+            self._ready_states.remove(state_id)
+
+        if delete:
+            self._remove(state_id)
+        else:
+            # add the state_id to the terminated list
+            self._killed_states.append(state_id)
+
     @property
     @sync
     def ready_states(self):
@@ -561,7 +586,8 @@ def ready_states(self):
 
         This means it is not possible to change the state used by Manticore with `states = list(m.ready_states)`.
         """
-        for state_id in self._ready_states:
+        _ready_states = self._ready_states
+        for state_id in _ready_states:
             state = self._load(state_id)
             yield state
             # Re-save the state in case the user changed its data
@@ -610,9 +636,9 @@ def _all_states(self):
         """ Only allowed at not running.
             (At running we can have states at busy)
         """
-        return (
-            tuple(self._ready_states) + tuple(self._terminated_states) + tuple(self._killed_states)
-        )
+        return tuple(self._ready_states) + tuple(
+            self._terminated_states
+        )  # + tuple(self._killed_states)
 
     @property
     @sync
@@ -634,6 +660,11 @@ def count_states(self):
         """ Total states count """
         return len(self._all_states)
 
+    @sync
+    def count_all_states(self):
+        """ Total states count """
+        return len(self._all_states)
+
     @sync
     def count_ready_states(self):
         """ Ready states count """
@@ -866,11 +897,9 @@ def kill_timeout(self, timeout=None):
             timer.cancel()
 
     @at_not_running
-    def run(self, timeout=None):
+    def run(self):
         """
         Runs analysis.
-
-        :param timeout: Analysis timeout, in seconds
         """
         # Delete state cache
         # The cached version of a state may get out of sync if a worker in a
diff --git a/manticore/core/smtlib/constraints.py b/manticore/core/smtlib/constraints.py
index f46185b07..3cb4ed241 100644
--- a/manticore/core/smtlib/constraints.py
+++ b/manticore/core/smtlib/constraints.py
@@ -11,7 +11,7 @@
     BitVec,
     BoolConstant,
     ArrayProxy,
-    BoolEq,
+    BoolEqual,
     Variable,
     Constant,
 )
@@ -141,15 +141,16 @@ def __get_related(self, related_to=None):
         return related_variables, related_constraints
 
     def to_string(self, related_to=None, replace_constants=True):
+        replace_constants = False
         related_variables, related_constraints = self.__get_related(related_to)
 
         if replace_constants:
             constant_bindings = {}
-            for expression in self.constraints:
+            for expression in related_constraints:
                 if (
-                    isinstance(expression, BoolEq)
+                    isinstance(expression, BoolEqual)
                     and isinstance(expression.operands[0], Variable)
-                    and isinstance(expression.operands[1], Constant)
+                    and isinstance(expression.operands[1], (Variable, Constant))
                 ):
                     constant_bindings[expression.operands[0]] = expression.operands[1]
 
@@ -163,21 +164,19 @@ def to_string(self, related_to=None, replace_constants=True):
                 continue
             tmp.add(var.declaration)
             result += var.declaration + "\n"
-
         translator = TranslatorSmtlib(use_bindings=True)
         for constraint in related_constraints:
             if replace_constants:
-                if (
-                    isinstance(constraint, BoolEq)
-                    and isinstance(constraint.operands[0], Variable)
-                    and isinstance(constraint.operands[1], Constant)
-                ):
-                    var = constraint.operands[0]
-                    expression = constraint.operands[1]
-                    expression = simplify(replace(expression, constant_bindings))
-                    constraint = var == expression
+                constraint = simplify(replace(constraint, constant_bindings))
+                # if no variables then it is a constant
+                if isinstance(constraint, Constant) and constraint.value == True:
+                    continue
 
             translator.visit(constraint)
+        if replace_constants:
+            for k, v in constant_bindings.items():
+                translator.visit(k == v)
+
         for name, exp, smtlib in translator.bindings:
             if isinstance(exp, BitVec):
                 result += f"(declare-fun {name} () (_ BitVec {exp.size}))"
diff --git a/manticore/core/smtlib/expression.py b/manticore/core/smtlib/expression.py
index bca3b5f52..16bd0276f 100644
--- a/manticore/core/smtlib/expression.py
+++ b/manticore/core/smtlib/expression.py
@@ -178,7 +178,7 @@ def __invert__(self):
         return BoolNot(self)
 
     def __eq__(self, other):
-        return BoolEq(self, self.cast(other))
+        return BoolEqual(self, self.cast(other))
 
     def __hash__(self):
         return object.__hash__(self)
@@ -236,7 +236,7 @@ def __init__(self, value, **kwargs):
         super().__init__(value, **kwargs)
 
 
-class BoolEq(BoolOperation):
+class BoolEqual(BoolOperation):
     def __init__(self, a, b, **kwargs):
         super().__init__(a, b, **kwargs)
 
@@ -403,13 +403,13 @@ def __le__(self, other):
         return LessOrEqual(self, self.cast(other))
 
     def __eq__(self, other):
-        return Equal(self, self.cast(other))
+        return BoolEqual(self, self.cast(other))
 
     def __hash__(self):
         return object.__hash__(self)
 
     def __ne__(self, other):
-        return BoolNot(Equal(self, self.cast(other)))
+        return BoolNot(BoolEqual(self, self.cast(other)))
 
     def __gt__(self, other):
         return GreaterThan(self, self.cast(other))
@@ -591,9 +591,10 @@ def __init__(self, a, b, *args, **kwargs):
         super().__init__(a, b, *args, **kwargs)
 
 
-class Equal(BoolOperation):
+class BoolEqual(BoolOperation):
     def __init__(self, a, b, *args, **kwargs):
-        assert a.size == b.size
+        if isinstance(a, BitVec) or isinstance(b, BitVec):
+            assert a.size == b.size
         super().__init__(a, b, *args, **kwargs)
 
 
@@ -1001,16 +1002,7 @@ def taint(self):
         return self._array.taint
 
     def select(self, index):
-        index = self.cast_index(index)
-        if self.index_max is not None:
-            from .visitors import simplify
-
-            index = simplify(
-                BitVecITE(self.index_bits, index < 0, self.index_max + index + 1, index)
-            )
-        if isinstance(index, Constant) and index.value in self._concrete_cache:
-            return self._concrete_cache[index.value]
-        return self._array.select(index)
+        return self.get(index)
 
     def store(self, index, value):
         if not isinstance(index, Expression):
@@ -1040,6 +1032,9 @@ def __getitem__(self, index):
             for k, v in self._concrete_cache.items():
                 if k >= start and k < start + size:
                     array_proxy_slice._concrete_cache[k - start] = v
+
+            for i in self.written:
+                array_proxy_slice.written.add(i - start)
             return array_proxy_slice
         else:
             if self.index_max is not None:
@@ -1084,9 +1079,9 @@ def written(self):
             # take out Proxy sleve
             array = self._array
             offset = 0
-            if isinstance(array, ArraySlice):
+            while isinstance(array, ArraySlice):
                 # if it is a proxy over a slice take out the slice too
-                offset = array._slice_offset
+                offset += array._slice_offset
                 array = array._array
             while not isinstance(array, ArrayVariable):
                 # The index written to underlaying Array are displaced when sliced
@@ -1113,7 +1108,17 @@ def get(self, index, default=None):
         if default is None:
             default = self._default
         index = self.cast_index(index)
-        value = self.select(index)
+
+        if self.index_max is not None:
+            from .visitors import simplify
+
+            index = simplify(
+                BitVecITE(self.index_bits, index < 0, self.index_max + index + 1, index)
+            )
+        if isinstance(index, Constant) and index.value in self._concrete_cache:
+            return self._concrete_cache[index.value]
+
+        value = self._array.select(index)
         if default is None:
             return value
 
diff --git a/manticore/core/smtlib/operators.py b/manticore/core/smtlib/operators.py
index a6be5a66e..fbc8f5011 100644
--- a/manticore/core/smtlib/operators.py
+++ b/manticore/core/smtlib/operators.py
@@ -208,6 +208,9 @@ def ITEBV(size, cond, true_value, false_value):
     assert isinstance(false_value, (BitVec, int))
     assert isinstance(size, int)
 
+    if isinstance(cond, BoolConstant) and not cond.taint:
+        cond = cond.value
+
     if isinstance(cond, bool):
         if cond:
             return true_value
@@ -263,12 +266,6 @@ def UREM(a, b):
     return a % b
 
 
-def simplify(value):
-    if issymbolic(value):
-        return value.simplify()
-    return value
-
-
 def SAR(size, a, b):
     assert isinstance(size, int)
     if isinstance(b, BitVec) and b.size != size:
diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py
index 285eb6efa..bb77960c1 100644
--- a/manticore/core/smtlib/solver.py
+++ b/manticore/core/smtlib/solver.py
@@ -81,7 +81,7 @@ def check(self, constraints) -> bool:
         """Check if given constraints can be valid"""
         return self.can_be_true(constraints, True)
 
-    def can_be_true(self, constraints, expression) -> bool:
+    def can_be_true(self, constraints, expression=True) -> bool:
         """Check if given expression could be valid"""
         raise Exception("Abstract method not implemented")
 
@@ -386,7 +386,7 @@ def _pop(self):
         """Recall the last pushed constraint store and state."""
         self._send("(pop 1)")
 
-    def can_be_true(self, constraints, expression):
+    def can_be_true(self, constraints, expression=True):
         """Check if two potentially symbolic values can be equal"""
         if isinstance(expression, bool):
             if not expression:
@@ -429,9 +429,10 @@ def get_all_values(self, constraints, expression, maxcnt=None, silent=False):
                     f"get_all_values only implemented for {type(expression)} expression type."
                 )
 
+            from manticore.core.smtlib import translate_to_smtlib
+
             temp_cs.add(var == expression)
             self._reset(temp_cs.to_string(related_to=var))
-
             result = []
 
             start = time.time()
@@ -448,6 +449,7 @@ def get_all_values(self, constraints, expression, maxcnt=None, silent=False):
                         # of returned vals list (previous smtlib behavior)
                         break
                     else:
+                        print(result)
                         raise TooManySolutions(result)
                 if time.time() - start > consts.timeout:
                     raise SolverError("Timeout")
@@ -521,60 +523,71 @@ def optimize(self, constraints: ConstraintSet, x: BitVec, goal: str, M=10000):
                 return last_value
             raise SolverError("Optimizing error, unsat or unknown core")
 
-    def get_value(self, constraints, expression):
+    def get_value(self, constraints, *expressions):
         """
-        Ask the solver for one possible result of given expression using given set of constraints.
+        Ask the solver for one possible result of given expressions using
+        given set of constraints.
         """
-        if not issymbolic(expression):
-            return expression
-        assert isinstance(expression, (Bool, BitVec, Array))
+        values = []
         start = time.time()
         with constraints as temp_cs:
-            if isinstance(expression, Bool):
-                var = temp_cs.new_bool()
-            elif isinstance(expression, BitVec):
-                var = temp_cs.new_bitvec(expression.size)
-            elif isinstance(expression, Array):
-                var = []
-                result = []
-                for i in range(expression.index_max):
-                    subvar = temp_cs.new_bitvec(expression.value_bits)
-                    var.append(subvar)
-                    temp_cs.add(subvar == simplify(expression[i]))
+            for expression in expressions:
+                if not issymbolic(expression):
+                    values.append(expression)
+                    continue
+                assert isinstance(expression, (Bool, BitVec, Array))
+                if isinstance(expression, Bool):
+                    var = temp_cs.new_bool()
+                elif isinstance(expression, BitVec):
+                    var = temp_cs.new_bitvec(expression.size)
+                elif isinstance(expression, Array):
+                    var = []
+                    result = []
+                    for i in range(expression.index_max):
+                        subvar = temp_cs.new_bitvec(expression.value_bits)
+                        var.append(subvar)
+                        temp_cs.add(subvar == simplify(expression[i]))
 
-                self._reset(temp_cs)
-                if not self._is_sat():
-                    raise SolverError("Model is not available")
+                    self._reset(temp_cs)
+                    if not self._is_sat():
+                        raise SolverError("Model is not available")
 
-                for i in range(expression.index_max):
-                    self._send("(get-value (%s))" % var[i].name)
-                    ret = self._recv()
-                    assert ret.startswith("((") and ret.endswith("))")
-                    pattern, base = self._get_value_fmt
-                    m = pattern.match(ret)
-                    expr, value = m.group("expr"), m.group("value")
-                    result.append(int(value, base))
+                    for i in range(expression.index_max):
+                        self._send("(get-value (%s))" % var[i].name)
+                        ret = self._recv()
+                        assert ret.startswith("((") and ret.endswith("))")
+                        pattern, base = self._get_value_fmt
+                        m = pattern.match(ret)
+                        expr, value = m.group("expr"), m.group("value")
+                        result.append(int(value, base))
+                    values.append(bytes(result))
                     if time.time() - start > consts.timeout:
                         raise SolverError("Timeout")
-                return bytes(result)
+                    continue
 
-            temp_cs.add(var == expression)
+                temp_cs.add(var == expression)
+
+                self._reset(temp_cs)
 
-            self._reset(temp_cs)
+                if not self._is_sat():
+                    raise SolverError("Model is not available")
 
-        if not self._is_sat():
-            raise SolverError("Model is not available")
+                self._send("(get-value (%s))" % var.name)
+                ret = self._recv()
+                if not (ret.startswith("((") and ret.endswith("))")):
+                    raise SolverError("SMTLIB error parsing response: %s" % ret)
 
-        self._send("(get-value (%s))" % var.name)
-        ret = self._recv()
-        if not (ret.startswith("((") and ret.endswith("))")):
-            raise SolverError("SMTLIB error parsing response: %s" % ret)
+                if isinstance(expression, Bool):
+                    values.append({"true": True, "false": False}[ret[2:-2].split(" ")[1]])
+                if isinstance(expression, BitVec):
+                    pattern, base = self._get_value_fmt
+                    m = pattern.match(ret)
+                    expr, value = m.group("expr"), m.group("value")
+                    values.append(int(value, base))
+            if time.time() - start > consts.timeout:
+                raise SolverError("Timeout")
 
-        if isinstance(expression, Bool):
-            return {"true": True, "false": False}[ret[2:-2].split(" ")[1]]
-        if isinstance(expression, BitVec):
-            pattern, base = self._get_value_fmt
-            m = pattern.match(ret)
-            expr, value = m.group("expr"), m.group("value")
-            return int(value, base)
-        raise NotImplementedError("get_value only implemented for Bool and BitVec")
+        if len(expressions) == 1:
+            return values[0]
+        else:
+            return values
diff --git a/manticore/core/smtlib/visitors.py b/manticore/core/smtlib/visitors.py
index 486f5168b..d7579c32f 100644
--- a/manticore/core/smtlib/visitors.py
+++ b/manticore/core/smtlib/visitors.py
@@ -52,18 +52,16 @@ def result(self):
         return self._stack[-1]
 
     def _method(self, expression, *args):
-        assert expression.__class__.__mro__[-1] is object
         for cls in expression.__class__.__mro__:
             sort = cls.__name__
             methodname = "visit_%s" % sort
             if hasattr(self, methodname):
                 value = getattr(self, methodname)(expression, *args)
                 if value is not None:
-                    assert isinstance(value, Expression)
                     return value
         return self._rebuild(expression, args)
 
-    def visit(self, node, use_fixed_point=False):
+    def visit(self, node_arg, use_fixed_point=False):
         """
         The entry point of the visitor.
         The exploration algorithm is a DFS post-order traversal
@@ -75,6 +73,11 @@ def visit(self, node, use_fixed_point=False):
         :param use_fixed_point: if True, it runs _methods until a fixed point is found
         :type use_fixed_point: Bool
         """
+        if isinstance(node_arg, ArrayProxy):
+            node = node_arg.array
+        else:
+            node = node_arg
+
         cache = self._cache
         visited = set()
         stack = []
@@ -105,6 +108,13 @@ def visit(self, node, use_fixed_point=False):
                 self.visit(new_value)
                 old_value = new_value
                 new_value = self.pop()
+
+            if isinstance(node_arg, ArrayProxy):
+                new_value = ArrayProxy(new_value)
+                new_value._default = node_arg._default
+                new_value._written = set(node_arg.written)
+                new_value._concrete_cache = dict(node_arg._concrete_cache)
+
             self.push(new_value)
 
     @staticmethod
@@ -123,10 +133,10 @@ class Translator(Visitor):
     """ Simple visitor to translate an expression into something else
     """
 
-    def _method(self, expression, *args):
+    def _method(self, expression_arg, *args):
         # Special case. Need to get the unsleeved version of the array
-        if isinstance(expression, ArrayProxy):
-            expression = expression.array
+        expression = expression_arg
+
         assert expression.__class__.__mro__[-1] is object
         for cls in expression.__class__.__mro__:
             sort = cls.__name__
@@ -275,12 +285,17 @@ def __init__(self, **kw):
         BitVecNeg: operator.__invert__,
         LessThan: operator.__lt__,
         LessOrEqual: operator.__le__,
-        Equal: operator.__eq__,
+        BoolEqual: operator.__eq__,
         GreaterThan: operator.__gt__,
         GreaterOrEqual: operator.__ge__,
         BoolAnd: operator.__and__,
         BoolOr: operator.__or__,
         BoolNot: operator.__not__,
+        BitVecUnsignedDiv: lambda x, y: (x & (1 << 256) - 1) // (y & (1 << 256) - 1),
+        UnsignedLessThan: lambda x, y: x < y,
+        UnsignedLessOrEqual: lambda x, y: x <= y,
+        UnsignedGreaterThan: lambda x, y: x > y,
+        UnsignedGreaterOrEqual: lambda x, y: x >= y,
     }
 
     def visit_BitVecConcat(self, expression, *operands):
@@ -314,11 +329,7 @@ def visit_BoolAnd(self, expression, a, b):
             return b
         if isinstance(b, Constant) and b.value == True:
             return a
-
-    def visit_BoolOr(self, expression, a, b):
-        if isinstance(a, Constant) and a.value == False:
-            return b
-        if isinstance(b, Constant) and b.value == False:
+        if a is b:
             return a
 
     def visit_Operation(self, expression, *operands):
@@ -340,7 +351,7 @@ def visit_Operation(self, expression, *operands):
 constant_folder_simplifier_cache = CacheDict(max_size=150000, flush_perc=25)
 
 
-@lru_cache(maxsize=128)
+@lru_cache(maxsize=128, typed=True)
 def constant_folder(expression):
     global constant_folder_simplifier_cache
     simp = ConstantFolderSimplifier(cache=constant_folder_simplifier_cache)
@@ -377,13 +388,109 @@ def visit_BitVecZeroExtend(self, expression, *operands):
         else:
             return expression
 
+    def visit_BoolAnd(self, expression, *operands):
+        if isinstance(expression.operands[0], Constant) and expression.operands[0].value:
+            return expression.operands[1]
+        if isinstance(expression.operands[1], Constant) and expression.operands[1].value:
+            return expression.operands[0]
+
+        # AND ( EQ (EXTRACT(0,8, a), EXTRACT(0,8, b)),  EQ (EXTRACT(8,16, a), EXTRACT(8,16 b)) ->
+        # EQ(EXTRACT(0,16, a), EXTRACT(0,16, b))
+        if isinstance(expression.operands[0], BoolEqual) and isinstance(
+            expression.operands[1], BoolEqual
+        ):
+            # Eq operands
+            operanda = expression.operands[0]
+            operandb = expression.operands[1]
+            # Extract operands
+            operandaa = operanda.operands[0]
+            operandab = operanda.operands[1]
+            operandba = operandb.operands[0]
+            operandbb = operandb.operands[1]
+
+            if (
+                isinstance(operandaa, BitVecExtract)
+                and isinstance(operandab, BitVecExtract)
+                and isinstance(operandba, BitVecExtract)
+                and isinstance(operandbb, BitVecExtract)
+            ):
+
+                if (
+                    operandaa.value is operandba.value
+                    and operandab.value is operandbb.value
+                    and (operandaa.begining, operandaa.end) == (operandab.begining, operandab.end)
+                    and (operandba.begining, operandba.end) == (operandbb.begining, operandbb.end)
+                ):
+                    if ((operandaa.end + 1) == operandba.begining) or (
+                        operandaa.begining == (operandba.end + 1)
+                    ):
+
+                        value0 = operandaa.value  # := operandba.value
+                        value1 = operandab.value  # := operandbb.value
+                        beg = min(operandaa.begining, operandba.begining)
+                        end = max(operandaa.end, operandba.end)
+                        return BitVecExtract(value0, beg, end - beg + 1) == BitVecExtract(
+                            value1, beg, end - beg + 1
+                        )
+
+    def visit_BoolNot(self, expression, *operands):
+        if isinstance(expression.operands[0], BoolNot):
+            return expression.operands[0].operands[0]
+
+    def visit_BoolEqual(self, expression, *operands):
+        """ (EQ, ITE(cond, constant1, constant2), constant1) -> cond
+            (EQ, ITE(cond, constant1, constant2), constant2) -> NOT cond
+            (EQ (extract a, b, c) (extract a, b, c))
+        """
+        if isinstance(expression.operands[0], BitVecITE) and isinstance(
+            expression.operands[1], Constant
+        ):
+            if isinstance(expression.operands[0].operands[1], Constant) and isinstance(
+                expression.operands[0].operands[2], Constant
+            ):
+                value1, value2, value3 = (
+                    expression.operands[1].value,
+                    expression.operands[0].operands[1].value,
+                    expression.operands[0].operands[2].value,
+                )
+                if value1 == value2 and value1 != value3:
+                    return expression.operands[0].operands[0]  # FIXME:taint
+                elif value1 == value3 and value1 != value2:
+                    return BoolNot(expression.operands[0].operands[0], taint=expression.taint)
+
+        if operands[0] is operands[1]:
+            return BoolConstant(True, taint=expression.taint)
+
+        if isinstance(operands[0], BitVecExtract) and isinstance(operands[1], BitVecExtract):
+            if (
+                operands[0].value is operands[1].value
+                and operands[0].end == operands[1].end
+                and operands[0].begining == operands[1].begining
+            ):
+
+                return BoolConstant(True, taint=expression.taint)
+
+    def visit_BoolOr(self, expression, a, b):
+        if isinstance(a, Constant):
+            if a.value == False:
+                return b
+            if a.value == True:
+                return a
+        if isinstance(b, Constant):
+            if b.value == False:
+                return a
+            if b.value == True:
+                return b
+        if a is b:
+            return a
+
     def visit_BitVecITE(self, expression, *operands):
         # FIXME Enable some taint propagating optimization
-        if isinstance(expression.operands[0], Constant) and not expression.operands[0].taint:
-            if expression.operands[0].value:
-                result = expression.operands[1]
+        if isinstance(operands[0], Constant) and not expression.operands[0].taint:
+            if operands[0].value:
+                result = operands[1]
             else:
-                result = expression.operands[2]
+                result = operands[2]
             return result
 
         if self._changed(expression, operands):
@@ -392,16 +499,46 @@ def visit_BitVecITE(self, expression, *operands):
     def visit_BitVecConcat(self, expression, *operands):
         """ concat( extract(k1, 0, a), extract(sizeof(a)-k1, k1, a))  ==> a
             concat( extract(k1, beg, a), extract(end, k1, a))  ==> extract(beg, end, a)
+            concat( x , extract(k1, beg, a), extract(end, k1, a), z)  ==> concat( x , extract(k1, beg, a), extract(end, k1, a), z)
         """
-        op = expression.operands[0]
+        if len(operands) == 1:
+            return operands[0]
+
+        changed = False
+        last_o = None
+        new_operands = []
+        for o in operands:
+            if isinstance(o, BitVecExtract):
+                if last_o is None:
+                    last_o = o
+                else:
+                    if last_o.value is o.value and last_o.begining == o.end + 1:
+                        last_o = BitVecExtract(
+                            o.value, o.begining, last_o.end - o.begining + 1, taint=expression.taint
+                        )
+                        changed = True
+                    else:
+                        new_operands.append(last_o)
+                        last_o = o
+            else:
+                if last_o is not None:
+                    new_operands.append(last_o)
+                    last_o = None
+                new_operands.append(o)
+        if last_o is not None:
+            new_operands.append(last_o)
+        if changed:
+            return BitVecConcat(expression.size, *new_operands)
 
+        op = expression.operands[0]
         value = None
         end = None
         begining = None
         for o in operands:
             # If found a non BitVecExtract, do not apply
             if not isinstance(o, BitVecExtract):
-                return None
+                value = None
+                break
             # Set the value for the first item
             if value is None:
                 value = o.value
@@ -410,19 +547,21 @@ def visit_BitVecConcat(self, expression, *operands):
             else:
                 # If concat of extracts of different values do not apply
                 if value is not o.value:
-                    return None
+                    value = None
+                    break
                 # If concat of non contiguous extracs do not apply
                 if begining != o.end + 1:
-                    return None
+                    value = None
+                    break
                 # update begining variable
                 begining = o.begining
 
         if value is not None:
-            if end + 1 == value.size and begining == 0:
-                return value
-            else:
+            if end + 1 != value.size or begining != 0:
                 return BitVecExtract(value, begining, end - begining + 1, taint=expression.taint)
 
+        return value
+
     def visit_BitVecExtract(self, expression, *operands):
         """ extract(sizeof(a), 0)(a)  ==> a
             extract(16, 0)( concat(a,b,c,d) ) => concat(c, d)
@@ -432,7 +571,6 @@ def visit_BitVecExtract(self, expression, *operands):
         begining = expression.begining
         end = expression.end
         size = end - begining + 1
-
         # extract(sizeof(a), 0)(a)  ==> a
         if begining == 0 and end + 1 == op.size:
             return op
@@ -440,21 +578,29 @@ def visit_BitVecExtract(self, expression, *operands):
             return BitVecExtract(op.value, op.begining + begining, size, taint=expression.taint)
         elif isinstance(op, BitVecConcat):
             new_operands = []
-            bitcount = 0
             for item in reversed(op.operands):
+                if size == 0:
+                    assert expression.size == sum([x.size for x in new_operands])
+                    return BitVecConcat(
+                        expression.size, *reversed(new_operands), taint=expression.taint
+                    )
+
                 if begining >= item.size:
+                    # skip the item
                     begining -= item.size
                 else:
-                    if bitcount < expression.size:
+                    if begining == 0 and size == item.size:
                         new_operands.append(item)
-                    bitcount += item.size
-            if begining != expression.begining:
-                return BitVecExtract(
-                    BitVecConcat(sum([x.size for x in new_operands]), *reversed(new_operands)),
-                    begining,
-                    expression.size,
-                    taint=expression.taint,
-                )
+                        size = 0
+                    else:
+                        if size <= item.size - begining:
+                            new_operands.append(BitVecExtract(item, begining, size))
+                            size = 0
+                        else:
+                            new_operands.append(BitVecExtract(item, begining, item.size - begining))
+                            size -= item.size - begining
+                            begining = 0
+
         if isinstance(op, (BitVecAnd, BitVecOr, BitVecXor)):
             bitoperand_a, bitoperand_b = op.operands
             return op.__class__(
@@ -602,7 +748,7 @@ def visit_Expression(self, expression, *operands):
 arithmetic_simplifier_cache = CacheDict(max_size=150000, flush_perc=25)
 
 
-@lru_cache(maxsize=128)
+@lru_cache(maxsize=128, typed=True)
 def arithmetic_simplify(expression):
     global arithmetic_simplifier_cache
     simp = ArithmeticSimplifier(cache=arithmetic_simplifier_cache)
@@ -634,9 +780,9 @@ def to_constant(expression):
     return value
 
 
-@lru_cache(maxsize=128)
+@lru_cache(maxsize=128, typed=True)
 def simplify(expression):
-    expression = constant_folder(expression)
+    # expression = constant_folder(expression)
     expression = arithmetic_simplify(expression)
     return expression
 
@@ -675,7 +821,7 @@ def bindings(self):
 
     translation_table = {
         BoolNot: "not",
-        BoolEq: "=",
+        BoolEqual: "=",
         BoolAnd: "and",
         BoolOr: "or",
         BoolXor: "xor",
@@ -699,7 +845,6 @@ def bindings(self):
         BitVecNeg: "bvneg",
         LessThan: "bvslt",
         LessOrEqual: "bvsle",
-        Equal: "=",
         GreaterThan: "bvsgt",
         GreaterOrEqual: "bvsge",
         UnsignedLessThan: "bvult",
diff --git a/manticore/core/state.py b/manticore/core/state.py
index 5b03105f0..cee21abfb 100644
--- a/manticore/core/state.py
+++ b/manticore/core/state.py
@@ -309,7 +309,7 @@ def must_be_true(self, expr):
             self._constraints, expr == False
         )
 
-    def solve_one(self, expr, constrain=False):
+    def solve_one(self, *exprs, constrain=False):
         """
         Concretize a symbolic :class:`~manticore.core.smtlib.expression.Expression` into
         one solution.
@@ -319,14 +319,23 @@ def solve_one(self, expr, constrain=False):
         :return: Concrete value
         :rtype: int
         """
-        expr = self.migrate_expression(expr)
-        value = self._solver.get_value(self._constraints, expr)
-        if constrain:
-            self.constrain(expr == value)
-        # Include forgiveness here
-        if isinstance(value, bytearray):
-            value = bytes(value)
-        return value
+        # if len(exprs)>1:
+        values = []
+        for expr in exprs:
+            if not issymbolic(expr):
+                values.append(expr)
+            else:
+                expr = self.migrate_expression(expr)
+                value = self._solver.get_value(self._constraints, expr)
+                if constrain:
+                    self.constrain(expr == value)
+                # Include forgiveness here
+                if isinstance(value, bytearray):
+                    value = bytes(value)
+                values.append(value)
+        if len(exprs) == 1:
+            values = values[0]
+        return values
 
     def solve_n(self, expr, nsolves):
         """
diff --git a/manticore/ethereum/__init__.py b/manticore/ethereum/__init__.py
index 9e3d23d63..068a7c8be 100644
--- a/manticore/ethereum/__init__.py
+++ b/manticore/ethereum/__init__.py
@@ -1,6 +1,6 @@
 # Exports (for `from manticore.ethereum import ...`)
 from .abi import ABI
-from .manticore import ManticoreEVM
+from .manticore import ManticoreEVM, config
 from .state import State
 from .detectors import (
     Detector,
@@ -19,7 +19,6 @@
     DetectManipulableBalance,
 )
 from .account import EVMAccount, EVMContract
-from .abi import ABI
 from .solidity import SolidityMetadata
 
 from ..exceptions import NoAliveStates, EthereumError
diff --git a/manticore/ethereum/abi.py b/manticore/ethereum/abi.py
index 161d4dd3b..0c6aff913 100644
--- a/manticore/ethereum/abi.py
+++ b/manticore/ethereum/abi.py
@@ -5,7 +5,15 @@
 import sha3
 
 from . import abitypes
-from ..core.smtlib import Array, Operators, BitVec, ArrayVariable, ArrayProxy, issymbolic
+from ..core.smtlib import (
+    Array,
+    Operators,
+    BitVec,
+    ArrayVariable,
+    ArrayProxy,
+    to_constant,
+    issymbolic,
+)
 from ..exceptions import EthereumError
 
 logger = logging.getLogger(__name__)
@@ -220,7 +228,7 @@ def deserialize(type_spec, data):
 
     @staticmethod
     def _deserialize(ty, buf, offset=0):
-        assert isinstance(buf, (bytearray, Array))
+        assert isinstance(buf, (bytearray, bytes, Array))
         result = None
         if ty[0] == "int":
             result = ABI._deserialize_int(buf[offset : offset + 32], nbytes=ty[1] // 8)
@@ -234,11 +242,11 @@ def _deserialize(ty, buf, offset=0):
             result = (address, func_id)
         elif ty[0] in ("bytes", "string"):
             dyn_offset = ABI._deserialize_int(buf[offset : offset + 32])
+            dyn_offset = to_constant(dyn_offset)
             size = ABI._deserialize_int(buf[dyn_offset : dyn_offset + 32])
             result = buf[dyn_offset + 32 : dyn_offset + 32 + size]
         elif ty[0] in ("tuple"):
             result = ()
-            current_off = 0
             for ty_i in ty[1]:
                 result += (ABI._deserialize(ty_i, buf, offset),)
                 offset += ABI._type_size(ty_i)
@@ -272,7 +280,7 @@ def _serialize_uint(value, size=32, padding=0):
             raise ValueError
         if issymbolic(value):
             # FIXME This temporary array variable should be obtained from a specific constraint store
-            bytes = ArrayVariable(
+            buffer = ArrayVariable(
                 index_bits=256, index_max=32, value_bits=8, name="temp{}".format(uuid.uuid1())
             )
             if value.size <= size * 8:
@@ -280,16 +288,17 @@ def _serialize_uint(value, size=32, padding=0):
             else:
                 # automatically truncate, e.g. if they passed a BitVec(256) for an `address` argument (160 bits)
                 value = Operators.EXTRACT(value, 0, size * 8)
-            bytes = ArrayProxy(bytes.write_BE(padding, value, size))
+            buffer = buffer.write_BE(padding, value, size)
         else:
             value = int(value)
-            bytes = bytearray()
+            buffer = bytearray()
             for _ in range(padding):
-                bytes.append(0)
+                buffer.append(0)
             for position in reversed(range(size)):
-                bytes.append(Operators.EXTRACT(value, position * 8, 8))
-        assert len(bytes) == size + padding
-        return bytes
+                buffer.append(Operators.EXTRACT(value, position * 8, 8))
+            buffer = bytes(buffer)
+        assert len(buffer) == size + padding
+        return buffer
 
     @staticmethod
     def _serialize_int(value, size=32, padding=0):
@@ -314,6 +323,7 @@ def _serialize_int(value, size=32, padding=0):
 
             for position in reversed(range(size)):
                 buf.append(Operators.EXTRACT(value, position * 8, 8))
+            buf = bytes(buf)
         return buf
 
     @staticmethod
@@ -352,7 +362,7 @@ def _deserialize_uint(data, nbytes=32, padding=0, offset=0):
         :param nbytes: number of bytes to read starting from least significant byte
         :rtype: int or Expression
         """
-        assert isinstance(data, (bytearray, Array))
+        assert isinstance(data, (bytearray, bytes, Array))
         value = ABI._readBE(data, nbytes, padding=True, offset=offset)
         value = Operators.ZEXTEND(value, (nbytes + padding) * 8)
         return value
@@ -366,7 +376,7 @@ def _deserialize_int(data, nbytes=32, padding=0):
         :param nbytes: number of bytes to read starting from least significant byte
         :rtype: int or Expression
         """
-        assert isinstance(data, (bytearray, Array))
+        assert isinstance(data, (bytearray, bytes, Array))
         value = ABI._readBE(data, nbytes, padding=True)
         value = Operators.SEXTEND(value, nbytes * 8, (nbytes + padding) * 8)
         if not issymbolic(value):
diff --git a/manticore/ethereum/account.py b/manticore/ethereum/account.py
index a9fc16779..dd63bfdc9 100644
--- a/manticore/ethereum/account.py
+++ b/manticore/ethereum/account.py
@@ -28,6 +28,9 @@ def __eq__(self, other):
             return self._address == other._address
         return super().__eq__(other)
 
+    def __hash__(self):
+        return self._address
+
     @property
     def name_(self):
         """
diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py
index d175dfb13..0c56ec209 100644
--- a/manticore/ethereum/cli.py
+++ b/manticore/ethereum/cli.py
@@ -108,7 +108,7 @@ def ethereum_main(args, logger):
                 tx_send_ether=not args.txnoether,
                 tx_account=args.txaccount,
                 tx_preconstrain=args.txpreconstrain,
-                crytic_compile_args=vars(args),
+                compile_args=vars(args),  # FIXME
             )
 
         if not args.no_testcases:
diff --git a/manticore/ethereum/detectors.py b/manticore/ethereum/detectors.py
index 5c851a271..fc5f27cc3 100644
--- a/manticore/ethereum/detectors.py
+++ b/manticore/ethereum/detectors.py
@@ -496,12 +496,12 @@ def _check_finding(self, state, what):
             for taint in get_taints(what, "IOS_.*"):
                 address, pc, finding, at_init, condition = self._get_location(state, taint[4:])
                 if state.can_be_true(condition):
-                    self.add_finding(state, address, pc, finding, at_init)
+                    self.add_finding(state, address, pc, finding, at_init, condition)
         else:
             for taint in get_taints(what, "IOU_.*"):
                 address, pc, finding, at_init, condition = self._get_location(state, taint[4:])
                 if state.can_be_true(condition):
-                    self.add_finding(state, address, pc, finding, at_init)
+                    self.add_finding(state, address, pc, finding, at_init, condition)
 
     def did_evm_execute_instruction_callback(self, state, instruction, arguments, result):
         vm = state.platform.current_vm
@@ -700,7 +700,7 @@ def did_evm_read_storage_callback(self, state, address, offset, value):
             cbu = Operators.AND(cbu, Operators.OR(address != known_address, offset != known_offset))
 
         if state.can_be_true(cbu):
-            self.add_finding_here(state, "Potentially reading uninitialized storage")
+            self.add_finding_here(state, "Potentially reading uninitialized storage", cbu)
 
     def did_evm_write_storage_callback(self, state, address, offset, value):
         # concrete or symbolic write
diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index 267abaa67..4465a07f7 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -1,17 +1,16 @@
+import copy
+import itertools
 import binascii
 import json
 import logging
 import string
 from multiprocessing import Queue, Process
 from queue import Empty as EmptyQueue
-from subprocess import check_output, Popen, PIPE
 from typing import Dict, Optional, Union
-
+from enum import Enum
 import io
-import os
 import pyevmasm as EVMAsm
 import random
-import re
 import sha3
 import tempfile
 
@@ -28,6 +27,7 @@
     BoolOperation,
     Expression,
     issymbolic,
+    simplify,
 )
 from ..core.state import TerminateState, AbandonState
 from .account import EVMContract, EVMAccount, ABI
@@ -43,8 +43,30 @@
 logger = logging.getLogger(__name__)
 logging.getLogger("CryticCompile").setLevel(logging.ERROR)
 
-cfg = config.get_group("evm")
-cfg.add("defaultgas", 3000000, "Default gas value for ethereum transactions.")
+
+class Sha3Type(Enum):
+    """Used as configuration constant for choosing sha3 flavor"""
+
+    concretize = "concretize"
+    symbolicate = "symbolicate"
+    timetravel = "timetravel"
+    functions = "functions"
+
+    def title(self):
+        return self._name_.title()
+
+    @classmethod
+    def from_string(cls, name):
+        return cls.__members__[name]
+
+
+consts = config.get_group("evm")
+consts.add("defaultgas", 3000000, "Default gas value for ethereum transactions.")
+consts.add(
+    "sha3",
+    default=Sha3Type.concretize,
+    description="concretize(*): sound simple concretization\nsymbolicate: unsound symbolication with gout of cycle FP killing\ntimetravel: best effort is done on the spot using current and future information :-O\nfunctions: sha3 is replaced by a uninstantiated function, requires solver support",
+)
 
 
 def flagged(flag):
@@ -155,11 +177,11 @@ def make_symbolic_value(self, nbits=256, name=None):
         """
         avoid_collisions = False
         if name is None:
-            name = "TXVALUE"
+            name = "SVALUE"
             avoid_collisions = True
         return self.constraints.new_bitvec(nbits, name=name, avoid_collisions=avoid_collisions)
 
-    def make_symbolic_address(self, name=None, select="both"):
+    def make_symbolic_address(self, *accounts, name=None, select="both"):
         """
         Creates a symbolic address and constrains it to pre-existing addresses or the 0 address.
 
@@ -169,10 +191,11 @@ def make_symbolic_address(self, name=None, select="both"):
         """
         if select not in ("both", "normal", "contract"):
             raise EthereumError("Wrong selection type")
-        if select in ("normal", "contract"):
-            # FIXME need to select contracts or normal accounts
-            raise NotImplemented
-
+        # if select in ("normal", "contract"):
+        # FIXME need to select contracts or normal accounts
+        #    raise NotImplemented
+        if not accounts:
+            accounts = self._accounts.values()
         avoid_collisions = False
         if name is None:
             name = "TXADDR"
@@ -183,7 +206,11 @@ def make_symbolic_address(self, name=None, select="both"):
         )
 
         constraint = symbolic_address == 0
-        for account in self._accounts.values():
+        for account in accounts:
+            if select == "contract" and not self.get_code(account):
+                continue
+            if select == "normal" and self.get_code(account):
+                continue
             constraint = Operators.OR(symbolic_address == int(account), constraint)
         self.constrain(constraint)
 
@@ -196,18 +223,6 @@ def constrain(self, constraint):
             for state in self.all_states:
                 state.constrain(constraint)
 
-    @staticmethod
-    def compile(
-        source_code, contract_name=None, libraries=None, runtime=False, crytic_compile_args=dict()
-    ):
-        """ Get initialization bytecode from a Solidity source code """
-        name, source_code, init_bytecode, runtime_bytecode, srcmap, srcmap_runtime, hashes, abi, warnings = ManticoreEVM._compile(
-            source_code, contract_name, libraries, crytic_compile_args
-        )
-        if runtime:
-            return runtime_bytecode
-        return init_bytecode
-
     @staticmethod
     def _link(bytecode, libraries=None):
         has_dependencies = "_" in bytecode
@@ -246,90 +261,6 @@ def _link(bytecode, libraries=None):
             hex_contract = "".join(hex_contract_lst)
         return bytearray(binascii.unhexlify(hex_contract))
 
-    @staticmethod
-    def _run_solc(source_file, solc_bin=None, solc_remaps=[], working_dir=None):
-        """ Compile a source file with the Solidity compiler
-
-            :param source_file: a file object for the source file
-            :param solc_bin: path to solc binary
-            :param solc_remaps: solc import remaps
-            :return: output, warnings
-        """
-        if solc_bin is not None:
-            solc = solc_bin
-        else:
-            solc = "solc"
-
-        # check solc version
-        supported_versions = ("0.4.18", "0.4.21")
-
-        try:
-            installed_version_output = check_output([solc, "--version"])
-        except OSError:
-            raise EthereumError("Solidity compiler not installed.")
-
-        m = re.match(
-            r".*Version: (?P<version>(?P<major>\d+)\.(?P<minor>\d+)\.(?P<build>\d+)).*\+(?P<commit>[^\s]+).*",
-            installed_version_output.decode(),
-            re.DOTALL | re.IGNORECASE,
-        )
-
-        if not m or m.groupdict()["version"] not in supported_versions:
-            # Fixme https://github.com/trailofbits/manticore/issues/847
-            # logger.warning("Unsupported solc version %s", installed_version)
-            pass
-
-        # solc path search is a mess
-        # https://solidity.readthedocs.io/en/latest/layout-of-source-files.html
-
-        relative_filepath = source_file.name
-
-        if not working_dir:
-            working_dir = os.getcwd()
-
-        if relative_filepath.startswith(working_dir):
-            relative_filepath = relative_filepath[len(working_dir) + 1 :]
-
-        # If someone pass an absolute path to the file, we don't have to put cwd
-        additional_kwargs = {"cwd": working_dir} if working_dir else {}
-
-        solc_invocation = (
-            [solc]
-            + list(solc_remaps)
-            + [
-                "--combined-json",
-                "abi,srcmap,srcmap-runtime,bin,hashes,bin-runtime",
-                "--allow-paths",
-                ".",
-                relative_filepath,
-            ]
-        )
-        logger.debug(f"Running: {' '.join(solc_invocation)}")
-        p = Popen(solc_invocation, stdout=PIPE, stderr=PIPE, **additional_kwargs)
-        stdout, stderr = p.communicate()
-
-        stdout, stderr = stdout.decode(), stderr.decode()
-
-        # See #1123 - solc fails when run within snap
-        # and https://forum.snapcraft.io/t/interfaces-allow-access-tmp-directory/5129
-        if stdout == "" and f'""{relative_filepath}"" is not found' in stderr:
-            raise EthereumError(
-                "Solidity compilation failed with error: {}\n"
-                "Did you install solc from snap Linux universal packages?\n"
-                "If so, the problem is likely due to snap's sandbox restricting access to /tmp\n"
-                "\n"
-                "Here are some potential solutions:\n"
-                " 1) Remove solc from snap and install it different way\n"
-                " 2) Reinstall solc from snap in developer mode, so there is no sandbox\n"
-                " 3) Find a way to add /tmp to the solc's sandbox. If you do, "
-                "send us a PR so we could add it here!".format(stderr)
-            )
-
-        try:
-            return json.loads(stdout), stderr
-        except ValueError:
-            raise EthereumError("Solidity compilation error:\n\n{}".format(stderr))
-
     @staticmethod
     def _compile_through_crytic_compile(filename, contract_name, libraries, crytic_compile_args):
         """
@@ -376,7 +307,7 @@ def _compile_through_crytic_compile(filename, contract_name, libraries, crytic_c
             with open(filename) as f:
                 source_code = f.read()
 
-            return (name, source_code, bytecode, runtime, srcmap, srcmap_runtime, hashes, abi)
+            return name, source_code, bytecode, runtime, srcmap, srcmap_runtime, hashes, abi
 
         except InvalidCompilation as e:
             raise EthereumError(
@@ -464,9 +395,16 @@ def __init__(self, workspace_url: str = None, policy: str = "random"):
         super().__init__(initial_state, workspace_url=workspace_url, policy=policy)
         self.subscribe("will_terminate_state", self._terminate_state_callback)
         self.subscribe("did_evm_execute_instruction", self._did_evm_execute_instruction_callback)
-        self.subscribe("did_read_code", self._did_evm_read_code)
-        self.subscribe("on_symbolic_sha3", self._on_symbolic_sha3_callback)
-        self.subscribe("on_concrete_sha3", self._on_concrete_sha3_callback)
+        consts.sha3 = consts.sha3.symbolicate
+        if consts.sha3 is consts.sha3.timetravel:
+            self.subscribe("on_symbolic_function", self._on_timetravel)
+        elif consts.sha3 is consts.sha3.concretize:
+            self.subscribe("on_symbolic_function", self._on_concretize)
+        elif consts.sha3 is consts.sha3.symbolicate:
+            self.subscribe("on_symbolic_function", self.on_unsound_symbolication)
+        else:
+            # if consts.sha3 is consts.sha3.function:
+            raise NotImplemented
 
         self._accounts = dict()
         self._serializer = PickleSerializer()
@@ -475,11 +413,6 @@ def __init__(self, workspace_url: str = None, policy: str = "random"):
         self.detectors = {}
         self.metadata: Dict[int, SolidityMetadata] = {}
 
-        # The following should go to manticore.context so we can use multiprocessing
-        with self.locked_context("ethereum", dict) as context:
-            context["_sha3_states"] = dict()
-            context["_known_sha3"] = set()
-
     @property
     def world(self):
         """ The world instance or None if there is more than one state """
@@ -585,109 +518,6 @@ def _make_symbolic_arguments(self, ty):
 
         return result
 
-    def json_create_contract(
-        self,
-        jfile,
-        owner=None,
-        name=None,
-        contract_name=None,
-        balance=0,
-        gas=None,
-        network_id=None,
-        args=(),
-    ):
-        """ Creates a solidity contract based on a truffle json artifact.
-            https://github.com/trufflesuite/truffle/tree/develop/packages/truffle-contract-schema
-
-            :param jfile: truffle json artifact
-            :type jfile: str or IOBase
-            :param owner: owner account (will be default caller in any transactions)
-            :type owner: int or EVMAccount
-            :param contract_name: Name of the contract to analyze (optional if there is a single one in the source code)
-            :type contract_name: str
-            :param balance: balance to be transferred on creation
-            :type balance: int or BitVecVariable
-            :param gas: gas budget for each contract creation needed (may be more than one if several related contracts defined in the solidity source)
-            :type gas: int
-            :param network_id: Truffle network id to instantiate
-            :param tuple args: constructor arguments
-            :rtype: EVMAccount
-        """
-
-        if isinstance(jfile, io.IOBase):
-            jfile = jfile.read()
-        elif isinstance(jfile, bytes):
-            jfile = str(jfile, "utf-8")
-        elif not isinstance(jfile, str):
-            raise TypeError(f"source code bad type: {type(jfile).__name__}")
-
-        truffle = json.loads(jfile)
-        hashes = {}
-        for item in truffle["abi"]:
-            item_type = item["type"]
-            if item_type in ("function"):
-                signature = SolidityMetadata.function_signature_for_name_and_inputs(
-                    item["name"], item["inputs"]
-                )
-                hashes[signature] = int(
-                    "0x" + sha3.keccak_256(signature.encode()).hexdigest()[:8], 16
-                )
-                if "signature" in item:
-                    if item["signature"] != f"0x{hashes[signature]}":
-                        raise Exception(
-                            f"Something wrong with the sha3 of the method {signature} signature (a.k.a. the hash)"
-                        )
-
-        if contract_name is None:
-            contract_name = truffle["contractName"]
-
-        if network_id is None:
-            if len(truffle["networks"]) > 1:
-                raise Exception("Network id not specified")
-            if len(truffle["networks"]) == 1:
-                network_id = list(truffle["networks"].keys())[0]
-        if network_id in truffle["networks"]:
-            temp_dict = truffle["networks"][network_id]["links"]
-            links = dict((k, int(v["address"], 0)) for k, v in temp_dict.items())
-        else:
-            links = ()
-
-        source_code = truffle["source"]
-        bytecode = self._link(truffle["bytecode"][2:], links)
-        runtime = self._link(truffle["deployedBytecode"][2:], links)
-        if "sourceMap" in truffle:
-            srcmap = truffle["sourceMap"].split(";")
-        else:
-            srcmap_runtime = []
-        if "deployedSourceMap" in truffle:
-            srcmap_runtime = truffle["deployedSourceMap"].split(";")
-        else:
-            srcmap_runtime = []
-        abi = truffle["abi"]
-        md = SolidityMetadata(
-            contract_name, source_code, bytecode, runtime, srcmap, srcmap_runtime, hashes, abi, b""
-        )
-        constructor_types = md.get_constructor_arguments()
-        if constructor_types != "()":
-            if args is None:
-                args = self.make_symbolic_arguments(constructor_types)
-
-            constructor_data = ABI.serialize(constructor_types, *args)
-        else:
-            constructor_data = b""
-
-        contract_account = self.create_contract(
-            owner=owner, balance=balance, init=md._init_bytecode + constructor_data, gas=gas
-        )
-
-        if contract_account is None:
-            raise EthereumError(f"Failed to build contract {contract_name}")
-        self.metadata[int(contract_account)] = md
-
-        if not self.count_ready_states() or len(self.get_code(contract_account)) == 0:
-            return None
-        return contract_account
-
     def solidity_create_contract(
         self,
         source_code,
@@ -699,7 +529,7 @@ def solidity_create_contract(
         address=None,
         args=(),
         gas=None,
-        crytic_compile_args=None,
+        compile_args=None,
     ):
         """ Creates a solidity contract and library dependencies
 
@@ -714,14 +544,15 @@ def solidity_create_contract(
             :param address: the address for the new contract (optional)
             :type address: int or EVMAccount
             :param tuple args: constructor arguments
-            :param crytic_compile_args: crytic compile options (https://github.com/crytic/crytic-compile/wiki/Configuration)
-            :type crytic_compile_args: dict
+            :param compile_args: crytic compile options #FIXME(https://github.com/crytic/crytic-compile/wiki/Configuration)
+            :type compile_args: dict
             :param gas: gas budget for each contract creation needed (may be more than one if several related contracts defined in the solidity source)
             :type gas: int
             :rtype: EVMAccount
         """
 
-        crytic_compile_args = dict() if crytic_compile_args is None else crytic_compile_args
+        if compile_args is None:
+            compile_args = dict()
 
         if libraries is None:
             deps = {}
@@ -733,10 +564,7 @@ def solidity_create_contract(
             contract_name_i = contract_names.pop()
             try:
                 compile_results = self._compile(
-                    source_code,
-                    contract_name_i,
-                    libraries=deps,
-                    crytic_compile_args=crytic_compile_args,
+                    source_code, contract_name_i, libraries=deps, crytic_compile_args=compile_args
                 )
                 md = SolidityMetadata(*compile_results)
                 if contract_name_i == contract_name:
@@ -1015,7 +843,7 @@ def _transaction(self, sort, caller, value=0, address=None, data=None, gaslimit=
             :rtype: EVMAccount
         """
         if gaslimit is None:
-            gaslimit = cfg.defaultgas
+            gaslimit = consts.defaultgas
         # Type Forgiveness
         if isinstance(address, EVMAccount):
             address = int(address)
@@ -1166,7 +994,7 @@ def multi_tx_analysis(
         tx_account="attacker",
         tx_preconstrain=False,
         args=None,
-        crytic_compile_args=dict(),
+        compile_args=None,
     ):
         owner_account = self.create_account(balance=1000, name="owner")
         attacker_account = self.create_account(balance=1000, name="attacker")
@@ -1178,7 +1006,7 @@ def multi_tx_analysis(
             contract_name=contract_name,
             owner=owner_account,
             args=args,
-            crytic_compile_args=crytic_compile_args,
+            compile_args=compile_args,
         )
 
         if tx_account == "attacker":
@@ -1276,18 +1104,62 @@ def run(self, **kwargs):
         assert not self._busy_states
         assert not self.is_running()
 
-        # ManticoreEthereum decided at terminate_state_callback wich state is
+        # ManticoreEthereum decided at terminate_state_callback which state is
         # ready for next run and saved them at the context item
         # 'ethereum.saved_states'
         # Move successfully terminated states to ready states
         with self.locked_context("ethereum.saved_states", list) as saved_states:
             while saved_states:
                 state_id = saved_states.pop()
-                self._terminated_states.remove(state_id)
-                self._ready_states.append(state_id)
+                if state_id in self._terminated_states:
+                    self._terminated_states.remove(state_id)
+                    self._ready_states.append(state_id)
 
     # Callbacks
-    def _on_symbolic_sha3_callback(self, state, data, known_hashes):
+    def _on_concretize(self, state, func, data, result):
+        if not issymbolic(data):
+            y_concrete = func(data)
+        else:
+            with self.locked_context("ethereum") as context:
+                # adding a single random example so we can explore further
+                x_concrete = state.solve_one(data)
+                y_concrete = func(x_concrete)
+
+                # Lets contraint the data to the single sound concretization
+                state.constrain(x_concrete == data)
+
+        result.append(y_concrete)
+
+    def _on_timetravel(self, state, func, data, result):
+        if issymbolic(data):
+            # will be updated with the buf->hash pairs to use
+            known_hashes = {}
+            # This updates the local copy of sha3 with the pairs we need to explore
+            self._on_symbolic_sha3_callback_tt(state, data, known_hashes)
+
+            # This builds a symbol in `value` that represents all the known sha3
+            # as reported by ManticoreEVM
+            value = None  # never used
+            known_hashes_cond = False
+            for key, hsh in known_hashes.items():
+                # Ignore the key if the size wont match
+                if len(key) == len(data):
+                    cond = key == data
+                    if known_hashes_cond is False:
+                        value = hsh
+                        known_hashes_cond = cond
+                    else:
+                        value = Operators.ITEBV(256, cond, hsh, value)
+                        known_hashes_cond = Operators.OR(cond, known_hashes_cond)
+        else:
+            value = func(data)
+            self._on_concrete_sha3_callback_tt(state, data, value)
+            logger.info("Found a concrete SHA3 example %r -> %x", data, value)
+
+        result.append(value)
+
+    # Callbacks
+    def _on_symbolic_sha3_callback_tt(self, state, data, known_hashes):
         """ INTERNAL USE """
         assert issymbolic(data), "Data should be symbolic here!"
         with self.locked_context("ethereum") as context:
@@ -1295,7 +1167,9 @@ def _on_symbolic_sha3_callback(self, state, data, known_hashes):
             if known_sha3 is None:
                 known_sha3 = set()
 
-            sha3_states = context.get("_sha3_states", [])
+            sha3_states = context.get("_sha3_states", None)
+            if sha3_states is None:
+                sha3_states = dict()
             results = []
             # If know_hashes is true then there is a _known_ solution for the hash
             known_hashes_cond = False
@@ -1313,7 +1187,6 @@ def _on_symbolic_sha3_callback(self, state, data, known_hashes):
                 with state as temp:
                     temp.constrain(known_hashes_cond == False)
                     data_concrete = temp.solve_one(data)
-                # data_concrete = state.solve_one(data)
                 data_hash = int(sha3.keccak_256(data_concrete).hexdigest(), 16)
                 results.append((data_concrete, data_hash))
                 known_hashes_cond = Operators.OR(data_concrete == data, known_hashes_cond)
@@ -1329,7 +1202,10 @@ def _on_symbolic_sha3_callback(self, state, data, known_hashes):
                 if temp_state.can_be_true(not_known_hashes_cond):
                     temp_state.constrain(not_known_hashes_cond)
                     state_id = self._workspace.save_state(temp_state)
-                    sha3_states[state_id] = [hsh for buf, hsh in known_sha3]
+                    # Save the size of the input buffer and all known hashes so
+                    # we awake this state only when a _new_ sha3 pair for _this_
+                    # size is found
+                    sha3_states[state_id] = (len(data), [hsh for buf, hsh in known_sha3])
             context["_sha3_states"] = sha3_states
             context["_known_sha3"] = known_sha3
 
@@ -1340,14 +1216,209 @@ def _on_symbolic_sha3_callback(self, state, data, known_hashes):
             # send known hashes to evm
             known_hashes.update(results)
 
-    def _on_concrete_sha3_callback(self, state, buf, value):
+    def _on_concrete_sha3_callback_tt(self, state, buf, value):
         """ INTERNAL USE """
         with self.locked_context("ethereum", dict) as ethereum_context:
             known_sha3 = ethereum_context.get("_known_sha3", None)
             if known_sha3 is None:
                 known_sha3 = set()
+
+            sha3_states = ethereum_context.get("_sha3_states", None)
+            if sha3_states is None:
+                sha3_states = dict()
+
+            for sha3_state_id, (size, hashes) in sha3_states.items():
+                if size == len(buf) and value not in hashes:
+                    sha3_states.remove(sha3_state_id)
+
+                    # locked at locked_context()
+                    # Enqueue it in the ready state list for processing
+                    self._ready_states.append(sha3_state_id)
+                    self._lock.notify_all()
+
             known_sha3.add((buf, value))
             ethereum_context["_known_sha3"] = known_sha3
+            ethereum_context["_sha3_states"] = sha3_states
+
+    # Callbacks for generic SYMB TABLE
+    def on_unsound_symbolication(self, state, func, data, result):
+        """Apply the function func to data
+        state: a manticore state
+        func: a concrete normal python function like `sha3()`
+        data: a concrete or symbolic value of the domain of func
+        result: an empty list where to put the result
+
+
+        If data is concrete this method simply return func(data) in result.
+        In the case of a symbolic data this method returns a fresh free symbol Y
+        representing all the potential results of applying func to data.
+        The relations between the data and Y is saved in an internal table.
+
+
+                        result func(data)                     data is concrete
+                      / concrete_pairs.append((data, result))
+        func(data)   |
+                     \ result = constraints.new_bitvec()     data is symbolic
+                       symbolic_pairs.append((data, result))
+                       constraints.add(func_table is bijective)
+
+        """
+
+        name = func.__name__
+        # Save concrete unction
+        with self.locked_context("ethereum", dict) as ethereum_context:
+            functions = ethereum_context.get("symbolic_func", dict())
+            functions[name] = func
+            ethereum_context["symbolic_func"] = functions
+
+        if issymbolic(data):
+            """table: is a string used internally to identify the symbolic function
+                data: is the symbolic value of the function domain
+                known_pairs: in/out is a dictionary containing known pairs from {domain, range}"""
+            # We are adding a new pair to the symbolic pairs
+            # Reset the soundcheck if True
+            if state.context.get("soundcheck", None) == True:
+                state.context["soundcheck"] = None
+
+            data_var = state.new_symbolic_buffer(len(data))  # FIXME: generalize to bitvec
+            state.constrain(data_var == data)
+            data = data_var
+            # symbolic_pairs is the pairs known locally for this symbolic function
+            symbolic_pairs = state.context.get(f"symbolic_func_sym_{name}", [])
+            # lets make a fresh 256 bit symbol representing any potential hash
+            value = state.new_symbolic_value(256)
+
+            # bijectiveness
+            for i in range(len(symbolic_pairs)):
+                xa, ya = symbolic_pairs[i]
+                if len(xa) == len(data):
+                    constraint = simplify((xa == data) == (ya == value))
+                else:
+                    constraint = ya != value
+                state.constrain(constraint)  # bijective
+
+            symbolic_pairs.append((data, value))
+            state.context[f"symbolic_func_sym_{name}"] = symbolic_pairs
+            # let it return just new_hash
+        else:
+            value = func(data)
+            with self.locked_context("ethereum", dict) as ethereum_context:
+                global_known_pairs = ethereum_context.get(f"symbolic_func_conc_{name}", set())
+                global_known_pairs.add((data, value))
+                ethereum_context[f"symbolic_func_conc_{name}"] = global_known_pairs
+            concrete_pairs = state.context.get(f"symbolic_func_conc_{name}", set())
+            concrete_pairs.add((data, value))
+            state.context[f"symbolic_func_conc_{name}"] = concrete_pairs
+            logger.info(f"Found a concrete {name} {data} -> {value}")
+
+        result.append(value)
+
+    def fix_unsound_symbolication(self, state):
+        """ This method goes through all the applied symbolic functions and tries
+            to find a concrete matching set of pairs
+        """
+
+        def concretize_known_pairs(state, symbolic_pairs, known_pairs):
+            # Each symbolic pair must match at least one of the concrete
+            # pairs we know
+
+            for xa, ya in symbolic_pairs:
+                cond = False
+                for xc, yc in known_pairs:
+                    if len(xa) == len(xc):
+                        cond = Operators.OR(Operators.AND(xa == xc, ya == yc), cond)
+                state.constrain(cond)
+                if cond is False:
+                    return
+
+        def match(state, func, symbolic_pairs, concrete_pairs, depth=0):
+            """ Tries to find a concrete match for the symbolic pairs. It uses
+            concrete_pairs (and potentially extends it with solved pairs) until
+            a matching set of concrete pairs is found, or fail.
+
+            state: the current state
+            func: the relation between domain and range in symbolic_pairs/concrete_pairs
+            symbolic_pairs: related symbolic values that need a set of solutions
+            concrete_pairs: Known of concrete pairs that may match some of the symbolic pairs
+
+            """
+
+            # The base case. No symbolic pairs. Just check if the state is feasible.
+            if not symbolic_pairs:
+                return state.can_be_true(True)
+
+            if not state.can_be_true(True):
+                return False
+
+            for i in range(len(symbolic_pairs)):
+                # shuffle and if it failed X times at some depth bail configurable
+                x, y = symbolic_pairs[i]
+                new_symbolic_pairs = symbolic_pairs[:i] + symbolic_pairs[i + 1 :]
+                new_concrete_pairs = set(concrete_pairs)
+                unseen = True  # Is added only unseen pairs could make it sat
+                for x_concrete, y_concrete in concrete_pairs:
+                    if len(x) == len(x_concrete):  # If the size of the buffer wont
+                        # match it does not matter
+                        unseen = Operators.AND(
+                            Operators.AND(x != x_concrete, y != y_concrete), unseen
+                        )
+
+                with state as temp_state:
+                    temp_state.constrain(unseen)
+                    new_x_concretes = temp_state.solve_n(x, nsolves=1)
+                    new_y_concretes = map(func, new_x_concretes)
+                    new_concrete_pairs.update(zip(new_x_concretes, new_y_concretes))
+
+                seen = False
+                for x_concrete, y_concrete in new_concrete_pairs:
+                    if len(x) == len(x_concrete):  # If the size of the buffer wont
+                        # match it does not matter
+                        seen = Operators.OR(Operators.AND(x == x_concrete, y == y_concrete), seen)
+                with state as temp_state:
+                    temp_state.constrain(seen)
+                    if match(temp_state, func, new_symbolic_pairs, new_concrete_pairs, depth + 1):
+                        concrete_pairs.update(new_concrete_pairs)
+                        return True
+            return False
+
+        # Save concrete unction
+        with self.locked_context("ethereum", dict) as ethereum_context:
+            soundcheck = state.context.get("soundcheck", None)
+            if soundcheck is not None:
+                return soundcheck
+            functions = ethereum_context.get("symbolic_func", dict())
+            for table in functions:
+                symbolic_pairs = state.context.get(f"symbolic_func_sym_{table}", ())
+                # if not constrain_bijectivity(state, symbolic_pairs):
+                #    # If UF does not comply with bijectiveness bail
+                #    return False
+
+                # symbolic_pairs = graph_sort(state, symbolic_pairs)
+                known_pairs = ethereum_context.get(f"symbolic_func_conc_{table}", set())
+                new_known_pairs = set(known_pairs)
+                if not match(state, functions[table], symbolic_pairs, new_known_pairs):
+                    ethereum_context["soundcheck"] = False
+                    return False
+
+                # Now paste the known pairs in the state constraints
+                concretize_known_pairs(state, symbolic_pairs, new_known_pairs)
+                ethereum_context[f"symbolic_func_conc_{table}"] = new_known_pairs
+                state.context[f"symbolic_func_sym_{table}_done"] = symbolic_pairs
+
+            # Ok all functions had a match for current state
+            state.context["soundcheck"] = state.can_be_true(True)
+        return state.context["soundcheck"]
+
+    def concretize_unsound_symbolication(self):
+        self._on_did_run_unsound_symbolication()
+
+    def _on_did_run_unsound_symbolication(self):
+        # Called at the end of a run(). Need to filter out the unreproducible/
+        # unfeasible states
+        # Caveat: It will add redundant constraints from previous run()
+        for state in self.all_states:
+            if not self.fix_unsound_symbolication(state):
+                self.kill_state(state)
 
     def _terminate_state_callback(self, state, e):
         """ INTERNAL USE
@@ -1410,17 +1481,11 @@ def _did_evm_execute_instruction_callback(self, state, instruction, arguments, r
             (state.platform.current_vm.address, instruction.pc, at_init)
         )
 
-    def _did_evm_read_code(self, state, offset, size):
-        """ INTERNAL USE """
-        with self.locked_context("code_data", set) as code_data:
-            for i in range(offset, offset + size):
-                code_data.add((state.platform.current_vm.address, i))
-
     def get_metadata(self, address) -> Optional[SolidityMetadata]:
         """ Gets the solidity metadata for address.
             This is available only if address is a contract created from solidity
         """
-        return self.metadata.get(int(address))
+        return self.metadata.get(address)
 
     def register_detector(self, d):
         """
@@ -1455,6 +1520,13 @@ def unregister_detector(self, d):
     def workspace(self):
         return self._workspace._store.uri
 
+    @property
+    def global_findings(self):
+        try:
+            return self._global_findings
+        except AttributeError:
+            return set()
+
     def current_location(self, state):
         world = state.platform
         address = world.current_vm.address
@@ -1524,7 +1596,8 @@ def generate_testcase(self, state, message="", only_if=None, name="user"):
         for detector in self.detectors.values():
             for address, pc, finding, at_init, constraint in detector.get_findings(state):
                 if (address, pc, finding, at_init) not in local_findings:
-                    local_findings.add((address, pc, finding, at_init, constraint))
+                    if state.can_be_true(constraint):
+                        local_findings.add((address, pc, finding, at_init, constraint))
 
         if len(local_findings):
             with testcase.open_stream("findings") as findings:
@@ -1541,12 +1614,15 @@ def generate_testcase(self, state, message="", only_if=None, name="user"):
         with testcase.open_stream("summary") as stream:
             is_something_symbolic = state.platform.dump(stream, state, self, message)
 
-            with self.locked_context("ethereum") as context:
-                known_sha3 = context.get("_known_sha3", None)
-                if known_sha3:
-                    stream.write("Known hashes:\n")
-                    for key, value in known_sha3:
-                        stream.write("%s::%x\n" % (binascii.hexlify(key), value))
+            with self.locked_context("ethereum", dict) as ethereum_context:
+                functions = ethereum_context.get("symbolic_func", dict())
+
+                for table in functions:
+                    concrete_pairs = state.context.get(f"symbolic_func_conc_{table}", ())
+                    if concrete_pairs:
+                        stream.write(f"Known for {table}:\n")
+                        for key, value in concrete_pairs:
+                            stream.write("%s::%x\n" % (binascii.hexlify(key), value))
 
             if is_something_symbolic:
                 stream.write(
@@ -1554,7 +1630,6 @@ def generate_testcase(self, state, message="", only_if=None, name="user"):
                 )
 
         # Transactions
-
         with testcase.open_stream("tx") as tx_summary:
             with testcase.open_stream("tx.json") as txjson:
                 txlist = []
@@ -1625,17 +1700,8 @@ def _emit_trace_file(filestream, trace):
             ln = "0x{:x}:0x{:x} {}\n".format(contract, pc, "*" if at_init else "")
             filestream.write(ln)
 
-    @property
-    def global_findings(self):
-        global_findings = set()
-        for detector in self.detectors.values():
-            for address, pc, finding, at_init in detector.global_findings:
-                if (address, pc, finding, at_init) not in global_findings:
-                    global_findings.add((address, pc, finding, at_init))
-        return global_findings
-
     @ManticoreBase.at_not_running
-    def finalize(self, procs=10):
+    def finalize(self, procs=45):
         """
         Terminate and generate testcases for all currently alive states (contract
         states that cleanly executed to a STOP or RETURN in the last symbolic
@@ -1648,13 +1714,11 @@ def finalize(self, procs=10):
 
         def finalizer(state_id):
             st = self._load(state_id)
-            logger.debug("Generating testcase for state_id %d", state_id)
-            last_tx = st.platform.last_transaction
-            message = last_tx.result if last_tx else "NO STATE RESULT (?)"
-            try:
+            if self.fix_unsound_symbolication(st):
+                logger.debug("Generating testcase for state_id %d", state_id)
+                last_tx = st.platform.last_transaction
+                message = last_tx.result if last_tx else "NO STATE RESULT (?)"
                 self.generate_testcase(st, message=message)
-            except Exception as e:
-                print(e)
 
         def worker_finalize(q):
             try:
@@ -1663,6 +1727,7 @@ def worker_finalize(q):
             except EmptyQueue:
                 pass
 
+        # Generate testcases for all but killed states
         q = Queue()
         for state_id in self._all_states:
             # we need to remove -1 state before forking because it may be in memory
@@ -1675,6 +1740,17 @@ def worker_finalize(q):
         for proc in report_workers:
             proc.join()
 
+        global_findings = set()
+        for state in self.all_states:
+            if not self.fix_unsound_symbolication(state):
+                continue
+            for detector in self.detectors.values():
+                for address, pc, finding, at_init, constraint in detector.get_findings(state):
+                    if (address, pc, finding, at_init) not in global_findings:
+                        if state.can_be_true(constraint):
+                            global_findings.add((address, pc, finding, at_init))
+        self._global_findings = global_findings
+
         # global summary
         with self._output.save_stream("global.findings") as global_findings_stream:
             for address, pc, finding, at_init in self.global_findings:
@@ -1696,23 +1772,19 @@ def worker_finalize(q):
                 global_summary.write(
                     "{:x}: {:2.2f}%\n".format(int(address), self.global_coverage(address))
                 )
+            with self.locked_context("ethereum", dict) as ethereum_context:
+                functions = ethereum_context.get("symbolic_func", dict())
+                for table in functions:
+                    concrete_pairs = ethereum_context.get(f"symbolic_func_conc_{table}", ())
+                    if concrete_pairs:
+                        global_summary.write(f"Known for {table}:\n")
+                        for key, value in concrete_pairs:
+                            global_summary.write("%s::%x\n" % (binascii.hexlify(key), value))
 
-                md = self.get_metadata(address)
-                if md is not None and len(md.warnings) > 0:
-                    global_summary.write("\n\nCompiler warnings for %s:\n" % md.name)
-                    global_summary.write(md.warnings)
-
+        md = self.get_metadata(address)
         for address, md in self.metadata.items():
             with self._output.save_stream("global_%s.sol" % md.name) as global_src:
                 global_src.write(md.source_code)
-            with self._output.save_stream(
-                "global_%s_runtime.bytecode" % md.name, binary=True
-            ) as global_runtime_bytecode:
-                global_runtime_bytecode.write(md.runtime_bytecode)
-            with self._output.save_stream(
-                "global_%s_init.bytecode" % md.name, binary=True
-            ) as global_init_bytecode:
-                global_init_bytecode.write(md.init_bytecode)
 
             with self._output.save_stream(
                 "global_%s.runtime_asm" % md.name
@@ -1723,7 +1795,7 @@ def worker_finalize(q):
                 for i in EVMAsm.disassemble_all(runtime_bytecode):
                     if (address, i.pc) in seen:
                         count += 1
-                        global_runtime_asm.write("*")
+                        globalmanticore / ethereum / manticore.py_runtime_asm.write("*")
                     else:
                         global_runtime_asm.write(" ")
 
diff --git a/manticore/ethereum/plugins.py b/manticore/ethereum/plugins.py
index f27bd8613..f956147e8 100644
--- a/manticore/ethereum/plugins.py
+++ b/manticore/ethereum/plugins.py
@@ -207,7 +207,9 @@ def did_run_callback(self):
             for state_id in list(saved_states):
                 st = self.manticore._load(state_id)
                 if not st.context["written"][-1]:
-                    self.manticore._terminated_states.append(st.id)
+                    if st.id in self.manticore._ready_states:
+                        self.manticore._ready_states.remove(st.id)
+                        self.manticore._terminated_states.append(st.id)
                     saved_states.remove(st.id)
 
     def generate_testcase(self, state, testcase, message):
diff --git a/manticore/native/manticore.py b/manticore/native/manticore.py
index 1cc2dbf94..7572139d4 100644
--- a/manticore/native/manticore.py
+++ b/manticore/native/manticore.py
@@ -307,8 +307,8 @@ def resolve(self, symbol):
     def run(self, timeout=None):
         with self.locked_context() as context:
             context["time_started"] = time.time()
-
-        super().run(timeout=timeout)
+        with self.kill_timeout(timeout):
+            super().run()
 
     def finalize(self):
         super().finalize()
diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index 71a394942..16ad10771 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -1,4 +1,5 @@
 """Symbolic EVM implementation based on the yellow paper: http://gavwood.com/paper.pdf"""
+import uuid
 import binascii
 import random
 import io
@@ -20,6 +21,7 @@
     translate_to_smtlib,
     to_constant,
     simplify,
+    get_depth,
     issymbolic,
     get_taints,
     istainted,
@@ -35,7 +37,6 @@
 from collections import namedtuple
 import sha3
 import rlp
-import time
 
 logger = logging.getLogger(__name__)
 
@@ -53,9 +54,14 @@
 # ignore: Ignore gas. Do not account for it. Do not OOG.
 consts = config.get_group("evm")
 
+
+def globalsha3(data):
+    return int(sha3.keccak_256(data).hexdigest(), 16)
+
+
 consts.add(
     "oog",
-    default="pedantic",
+    default="complete",
     description=(
         "Default behavior for symbolic gas."
         "pedantic: Fully faithful. Test at every instruction. Forks."
@@ -251,7 +257,7 @@ def dump(self, stream, state, mevm, conc_tx=None):
                 calldata = conc_tx.data
                 is_calldata_symbolic = issymbolic(self.data)
 
-                function_id = calldata[:4]  # hope there is enough data
+                function_id = bytes(calldata[:4])  # hope there is enough data
                 signature = metadata.get_func_signature(function_id)
                 function_name = metadata.get_func_name(function_id)
                 if signature:
@@ -547,7 +553,7 @@ def wrapper(*args, **kwargs):
                     # TODO / FIXME: The taint should persist!
                     logger.warning(
                         f"Concretizing {func.__name__}'s {index} argument and dropping its taints: "
-                        "the value might not be tracked properly (in case of using detectors)"
+                        "the value might not be tracked properly (This may affect detectors)"
                     )
                 logger.info(
                     f"Concretizing instruction {args[0].world.current_vm.instruction} argument {arg} by {policy}"
@@ -578,9 +584,9 @@ class EVM(Eventful):
         "evm_read_memory",
         "evm_write_memory",
         "evm_read_code",
+        "evm_write_code",
         "decode_instruction",
-        "concrete_sha3",
-        "symbolic_sha3",
+        "on_unsound_symbolication",
     }
 
     class transact:
@@ -732,10 +738,7 @@ def extend_with_zeroes(b):
         self._published_pre_instruction_events = False
 
         # Used calldata size
-        min_size = 0
-        max_size = len(self.data)
         self._used_calldata_size = 0
-        self._calldata_size = len(self.data)
         self._valid_jmpdests = set()
 
     @property
@@ -775,7 +778,6 @@ def __getstate__(self):
         state["_checkpoint_data"] = self._checkpoint_data
         state["_published_pre_instruction_events"] = self._published_pre_instruction_events
         state["_used_calldata_size"] = self._used_calldata_size
-        state["_calldata_size"] = self._calldata_size
         state["_valid_jumpdests"] = self._valid_jumpdests
         state["_check_jumpdest"] = self._check_jumpdest
         return state
@@ -799,7 +801,6 @@ def __setstate__(self, state):
         self._allocated = state["allocated"]
         self.suicides = state["suicides"]
         self._used_calldata_size = state["_used_calldata_size"]
-        self._calldata_size = state["_calldata_size"]
         self._valid_jumpdests = state["_valid_jumpdests"]
         self._check_jumpdest = state["_check_jumpdest"]
         super().__setstate__(state)
@@ -952,7 +953,7 @@ def _consume(self, fee):
         # pesimistic: OOG soon. If it may NOT be enough gas we ignore the normal case. A constraint is added to assert the gas is NOT enough and the other state is ignored.
         # ignore: Ignore gas. Do not account for it. Do not OOG.
 
-        # optimization that speed up concrete fees sometimes
+        # optimization that speed up concrete fees over symbolic gas sometimes
         if not issymbolic(fee) and issymbolic(self._gas):
             reps, m = getattr(self, "_mgas", (0, None))
             reps += 1
@@ -969,13 +970,15 @@ def _consume(self, fee):
             # gas is faithfully accounted and ogg checked at instruction/BB level.
             if consts.oog == "pedantic" or self.instruction.is_terminator:
                 # explore both options / fork
+                constraint = simplify(Operators.UGT(self._gas, fee))
 
                 # FIXME if gas can be both enough and insufficient this will
                 #  reenter here and generate redundant queries
-                if not issymbolic(self._gas) and not issymbolic(fee):
-                    enough_gas_solutions = (self._gas - fee >= 0,)
+                if isinstance(constraint, Constant):
+                    enough_gas_solutions = (constraint.value,)  # (self._gas - fee >= 0,)
+                elif isinstance(constraint, bool):
+                    enough_gas_solutions = (constraint,)  # (self._gas - fee >= 0,)
                 else:
-                    constraint = simplify(Operators.UGT(self._gas, fee))
                     enough_gas_solutions = Z3Solver.instance().get_all_values(
                         self.constraints, constraint
                     )
@@ -983,10 +986,7 @@ def _consume(self, fee):
                 if len(enough_gas_solutions) == 2:
                     # if gas can be both enough and insufficient, fork
                     raise Concretize(
-                        "Concretize gas fee",
-                        expression=Operators.UGT(self._gas, fee),
-                        setstate=None,
-                        policy="ALL",
+                        "Concretize gas fee", expression=constraint, setstate=None, policy="ALL"
                     )
                 elif enough_gas_solutions[0] is False:
                     # if gas if only insuficient OOG!
@@ -997,6 +997,7 @@ def _consume(self, fee):
                 else:
                     assert enough_gas_solutions[0] is True
                     # if there is enough gas keep going
+
         elif consts.oog == "concrete":
             # Keep gas concrete. Concretize symbolic fees to some values.
             # this can happen only if symbolic gas is provided for the TX
@@ -1028,6 +1029,8 @@ def _consume(self, fee):
             # do nothing. gas is not even changed
             return
         self._gas = simplify(self._gas - fee)
+        if isinstance(self._gas, Constant) and not self._gas.taint:
+            self._gas = self._gas.value
 
         # If everything is concrete lets just check at every instruction
         if not issymbolic(self._gas) and self._gas < 0:
@@ -1134,7 +1137,7 @@ def _set_check_jmpdest(self, flag=True):
         Note that at this point `flag` can be the conditional from a JUMPI
         instruction hence potentially a symbolic value.
         """
-        self._check_jumpdest = flag
+        self._check_jumpdest = simplify(flag)
 
     def _check_jmpdest(self):
         """
@@ -1145,7 +1148,9 @@ def _check_jmpdest(self):
         already constrained to a single concrete value.
         """
         should_check_jumpdest = self._check_jumpdest
-        if issymbolic(should_check_jumpdest):
+        if isinstance(should_check_jumpdest, Constant):
+            should_check_jumpdest = should_check_jumpdest.value
+        elif issymbolic(should_check_jumpdest):
             should_check_jumpdest_solutions = Z3Solver().get_all_values(
                 self.constraints, should_check_jumpdest
             )
@@ -1208,7 +1213,7 @@ def setstate(state, value):
             raise Concretize(
                 "Concretize PC", expression=expression, setstate=setstate, policy="ALL"
             )
-        # print(self.instruction)
+        # print(self)
         try:
             # import time
             # limbo = 0.0
@@ -1253,7 +1258,7 @@ def setstate(state, value):
 
             raise Concretize(
                 "Concretize current instruction fee",
-                expression=fee,
+                expression=self._checkpoint_data[4],
                 setstate=setstate,
                 policy=ex.policy,
             )
@@ -1549,36 +1554,20 @@ def try_simplify_to_constant(self, data):
 
     def SHA3_gas(self, start, size):
         GSHA3WORD = 6  # Cost of SHA3 per word
+        sha3fee = self.safe_mul(GSHA3WORD, ceil32(size) // 32)
         memfee = self._get_memfee(start, size)
-        return GSHA3WORD * (ceil32(size) // 32) + memfee
+        return self.safe_add(sha3fee, memfee)
 
-    @concretized_args(size="SAMPLED")
+    @concretized_args(size="ALL")
     def SHA3(self, start, size):
-        """Compute Keccak-256 hash"""
-        # read memory from start to end
-        # http://gavwood.com/paper.pdf
-        data = self.try_simplify_to_constant(self.read_buffer(start, size))
-
-        if issymbolic(data):
-            known_sha3 = {}
-            # Broadcast the signal
-            self._publish(
-                "on_symbolic_sha3", data, known_sha3
-            )  # This updates the local copy of sha3 with the pairs we need to explore
-            value = 0  # never used
-            known_hashes_cond = False
-            for key, hsh in known_sha3.items():
-                assert not issymbolic(key), "Saved sha3 data,hash pairs should be concrete"
-                cond = key == data
-                known_hashes_cond = Operators.OR(cond, known_hashes_cond)
-                value = Operators.ITEBV(256, cond, hsh, value)
-            return value
+        """Compute Keccak-256 hash
+            If the size is symbolic the potential solutions will be sampled as
+            defined by the default policy and the analysis will be forked.
+            The `size` can be considered concrete in this handler.
 
-        value = sha3.keccak_256(data).hexdigest()
-        value = int(value, 16)
-        self._publish("on_concrete_sha3", data, value)
-        logger.info("Found a concrete SHA3 example %r -> %x", data, value)
-        return value
+        """
+        data = self.read_buffer(start, size)
+        return self.world.symbolic_function(globalsha3, data)
 
     ############################################################################
     # Environmental Information
@@ -1607,95 +1596,105 @@ def CALLVALUE(self):
 
     def CALLDATALOAD(self, offset):
         """Get input data of current environment"""
-
-        if issymbolic(offset):
-            if Z3Solver().can_be_true(self._constraints, offset == self._used_calldata_size):
-                self.constraints.add(offset == self._used_calldata_size)
-                offset = self._used_calldata_size
-            else:
-                raise ConcretizeArgument(1, policy="SAMPLED")
+        # calldata_overflow = const.calldata_overflow
+        # calldata_underflow = const.calldata_underflow
+        calldata_overflow = None  # 32
+        calldata_underflow = None  # 32
+        # if const.calldata_overlap:
+        if calldata_overflow is not None:
+            self.constraints.add(offset + 32 <= len(self.data) + calldata_overflow)
+        if calldata_underflow is not None:
+            self.constraints.add(offset >= -calldata_underflow)
 
         self._use_calldata(offset, 32)
 
         data_length = len(self.data)
-
         bytes = []
         for i in range(32):
             try:
-                c = Operators.ITEBV(8, offset + i < data_length, self.data[offset + i], 0)
+                c = simplify(Operators.ITEBV(8, offset + i < data_length, self.data[offset + i], 0))
             except IndexError:
                 # offset + i is concrete and outside data
                 c = 0
-
             bytes.append(c)
         return Operators.CONCAT(256, *bytes)
 
-    def _use_calldata(self, n, size):
-        assert not issymbolic(n)
-        max_size = len(self.data)
-        min_size = self._used_calldata_size
+    def _use_calldata(self, offset, size):
+        """ To improve reporting we maintain how much of the calldata is actually
+        used. CALLDATACOPY and CALLDATA LOAD update this limit accordingly """
         self._used_calldata_size = Operators.ITEBV(
-            256,
-            size != 0,
-            Operators.ITEBV(256, min_size + n > max_size, max_size, min_size + n),
-            self._used_calldata_size,
+            256, size != 0, self._used_calldata_size + offset + size, self._used_calldata_size
         )
 
     def CALLDATASIZE(self):
         """Get size of input data in current environment"""
-        return self._calldata_size
+        return len(self.data)
 
     def CALLDATACOPY_gas(self, mem_offset, data_offset, size):
         GCOPY = 3  # cost to copy one 32 byte word
         copyfee = self.safe_mul(GCOPY, self.safe_add(size, 31) // 32)
         memfee = self._get_memfee(mem_offset, size)
-        return copyfee + memfee
+        return self.safe_add(copyfee, memfee)
 
+    @concretized_args(size="SAMPLED")
     def CALLDATACOPY(self, mem_offset, data_offset, size):
         """Copy input data in current environment to memory"""
-        if issymbolic(size):
-            if not Z3Solver().can_be_true(
-                self._constraints, Operators.ULE(size, len(self.data) + data_offset + 32)
-            ):
-                print("omg it can not be small")
-                import pdb
-
-                pdb.set_trace()
-                raise ConcretizeArgument(3, policy="MIN")
-            self.constraints.add(Operators.ULE(size, len(self.data) + data_offset + 32))
-            raise ConcretizeArgument(3, policy="SAMPLED")
-
-        if issymbolic(data_offset):
-            if Z3Solver().can_be_true(self._constraints, data_offset == self._used_calldata_size):
-                self.constraints.add(data_offset == self._used_calldata_size)
-                data_offset = self._used_calldata_size
-                print("symbolic data_offset", data_offset, "choosing", self._used_calldata_size)
-            else:
-                logger.debug("symbolic data_offset MIN")
-                raise ConcretizeArgument(2, policy="MIN")
+        # calldata_overflow = const.calldata_overflow
+        # calldata_underflow = const.calldata_underflow
+        calldata_overflow = None  # 32
+        calldata_underflow = None  # 32
+        # if const.calldata_overlap:
+        if calldata_underflow is not None:
+            self.constraints.add(data_offset + size <= len(self.data) + calldata_overflow)
+            self.constraints.add(data_offset >= -calldata_underflow)
 
-        # account for calldata usage
         self._use_calldata(data_offset, size)
         self._allocate(mem_offset, size)
-        if size > consts.calldata_max_offset:
-            logger.info("CALLDATACOPY absurd size %d. OOG policy used: %r", size, consts.oog)
-            raise TerminateState(
-                "CALLDATACOPY absurd size %d. OOG policy used: %r" % (size, consts.oog),
-                testcase=True,
-            )
 
-        for i in range(size):
+        if consts.oog == "complete":
+            # gas reduced
+            cond = Operators.ULT(self.gas, self._checkpoint_data[1])
+            if not Z3Solver.instance().can_be_true(self.constraints, cond):
+                raise NotEnoughGas()
+            self.constraints.add(cond)
+
+        max_size = size
+        if issymbolic(max_size):
+            max_size = Z3Solver.instance().max(self.constraints, size)
+
+        if calldata_overflow is not None:
+            cap = len(self.data) + calldata_overflow
+            if max_size > cap:
+                logger.info(f"Constraining CALLDATACOPY size to {cap}")
+                max_size = cap
+                self.constraints.add(Operators.ULE(size, cap))
+                # cond = Operators.OR(size == 0, size==4)
+                # for conc_size in range(8,max_size, 32):
+                #   cond = Operators.OR(size==conc_size, cond)
+                # self.constraints.add(cond)
+
+        for i in range(max_size):
             try:
-                c = Operators.ITEBV(
+                c1 = Operators.ITEBV(
                     8,
                     data_offset + i < len(self.data),
                     Operators.ORD(self.data[data_offset + i]),
                     0,
                 )
+
             except IndexError:
                 # data_offset + i is concrete and outside data
-                c = 0
-            self._store(mem_offset + i, c)
+                c1 = 0
+
+            c = simplify(Operators.ITEBV(8, i < size, c1, self.memory[mem_offset + i]))
+            if not issymbolic(c) or get_depth(c) < 3:
+                x = c
+            else:
+                # if te expression is deep enough lets replace it by a binding
+                x = self.constraints.new_bitvec(8, name="temp{}".format(uuid.uuid1()))
+                self.constraints.add(x == c)
+            self._store(mem_offset + i, x)
+            # print (str(self.constraints))
 
     def CODESIZE(self):
         """Get size of code running in current environment"""
@@ -1742,7 +1741,7 @@ def CODECOPY(self, mem_offset, code_offset, size):
                 else:
                     value = self.bytecode[code_offset + i]
             self._store(mem_offset + i, value)
-        self._publish("did_evm_read_code", code_offset, size)
+        self._publish("did_evm_read_code", self.address, code_offset, size)
 
     def GASPRICE(self):
         """Get price of gas in current environment"""
@@ -1770,6 +1769,7 @@ def EXTCODECOPY(self, account, address, offset, size):
                 self._store(address + i, extbytecode[offset + i])
             else:
                 self._store(address + i, 0)
+            self._publish("did_evm_read_code", address, offset, size)
 
     def RETURNDATACOPY_gas(self, mem_offset, return_offset, size):
         return self._get_memfee(mem_offset, size)
@@ -1948,7 +1948,7 @@ def LOG_gas(self, address, size, *topics):
     @concretized_args(size="ONE")
     def LOG(self, address, size, *topics):
         GLOGBYTE = 8
-        self._consume(size * GLOGBYTE)
+        self._consume(self.safe_mul(size, GLOGBYTE))
         memlog = self.read_buffer(address, size)
         self.world.log(self.address, topics, memlog)
 
@@ -2221,12 +2221,11 @@ class EVMWorld(Platform):
         "evm_read_storage",
         "evm_write_storage",
         "evm_read_code",
-        "decode_instruction",
+        "evm_write_code" "decode_instruction",
         "execute_instruction",
-        "concrete_sha3",
-        "symbolic_sha3",
         "open_transaction",
         "close_transaction",
+        "symbolic_function",
     }
 
     def __init__(
@@ -2299,6 +2298,42 @@ def __setstate__(self, state):
         for _, _, _, _, vm in self._callstack:
             self.forward_events_from(vm)
 
+    def try_simplify_to_constant(self, data):
+        concrete_data = bytearray()
+        for c in data:
+            simplified = simplify(c)
+            if isinstance(simplified, Constant):
+                concrete_data.append(simplified.value)
+            else:
+                # simplify by solving. probably means that we need to improve simplification
+                solutions = Z3Solver.instance().get_all_values(
+                    self.constraints, simplified, 2, silent=True
+                )
+                if len(solutions) != 1:
+                    break
+                concrete_data.append(solutions[0])
+        else:
+            data = bytes(concrete_data)
+        return data
+
+    def symbolic_function(self, func, data):
+        """
+        Get an unsound symbolication for function `func`
+
+        """
+        data = self.try_simplify_to_constant(data)
+        try:
+            result = []
+            self._publish(
+                "on_symbolic_function", func, data, result
+            )  # This updates the local copy of result
+
+            return result[0]
+        except Exception as e:
+            logger.info("Error! %r", e)
+            data_c = Z3Solver.instance().get_value(self.constraints, data)
+            return int(sha3.keccak_256(data_c).hexdigest(), 16)
+
     @property
     def PC(self):
         return (self.current_vm.address, self.current_vm.pc)
@@ -2312,7 +2347,13 @@ def __contains__(self, key):
         return key in self.accounts
 
     def __str__(self):
-        return "WORLD:" + str(self._world_state)
+        return (
+            "WORLD:"
+            + str(self._world_state)
+            + "\n"
+            + str(list((map(str, self.transactions))))
+            + str(self.logs)
+        )
 
     @property
     def logs(self):
@@ -2945,7 +2986,9 @@ def _process_pending_transaction(self):
         if not failed:
             src_balance = self.get_balance(caller)
             enough_balance = Operators.UGE(src_balance, value)
-            enough_balance_solutions = Z3Solver().get_all_values(self._constraints, enough_balance)
+            enough_balance_solutions = Z3Solver.instance().get_all_values(
+                self._constraints, enough_balance
+            )
 
             if set(enough_balance_solutions) == {True, False}:
                 raise Concretize(
@@ -3012,7 +3055,7 @@ def dump(self, stream, state, mevm, message):
             stream.write("Balance: %d %s\n" % (balance, flagged(is_balance_symbolic)))
 
             storage = blockchain.get_storage(account_address)
-            stream.write("Storage: %s\n" % translate_to_smtlib(storage, use_bindings=True))
+            stream.write("Storage: %s\n" % translate_to_smtlib(storage, use_bindings=False))
 
             all_used_indexes = []
             with state.constraints as temp_cs:
@@ -3021,8 +3064,9 @@ def dump(self, stream, state, mevm, message):
                 temp_cs.add(storage.get(index) != 0)
 
                 try:
+                    # FIXME do this only if it has symbolic writes?
                     while True:
-                        a_index = Z3Solver().get_value(temp_cs, index)
+                        a_index = Z3Solver.instance().get_value(temp_cs, index)
                         all_used_indexes.append(a_index)
 
                         temp_cs.add(storage.get(a_index) != 0)
diff --git a/manticore/utils/event.py b/manticore/utils/event.py
index d3374a96e..5a5d75440 100644
--- a/manticore/utils/event.py
+++ b/manticore/utils/event.py
@@ -150,7 +150,14 @@ def _publish_impl(self, _name, *args, **kwargs):
         bucket = self._get_signal_bucket(_name)
         for robj, methods in bucket.items():
             for callback in methods:
-                callback(robj(), *args, **kwargs)
+                try:
+                    callback(robj(), *args, **kwargs)
+                except Exception as e:
+                    import traceback
+
+                    # traceback.print_stack()
+                    traceback.print_last()
+                    print("Exception", e, callback)
 
         # The include_source flag indicates to prepend the source of the event in
         # the callback signature. This is set on forward_events_from/to
diff --git a/scripts/travis_test.sh b/scripts/travis_test.sh
index 8bacfbfc5..0af57f63f 100755
--- a/scripts/travis_test.sh
+++ b/scripts/travis_test.sh
@@ -95,8 +95,8 @@ run_truffle_tests(){
     # but Manticore fails to explore the paths due to the lack of the 0x1f opcode support
     # see https://github.com/trailofbits/manticore/issues/1166
     # if [ "$(ls output/*tx -l | wc -l)" != "41" ]; then
-    if [ "$(ls output/*tx -l | wc -l)" != "19" ]; then
-        echo "Truffle test failed" `ls output/*tx -l | wc -l` "!= 19"
+    if [ "$(ls output/*tx -l | wc -l)" != "13" ]; then
+        echo "Truffle test failed" `ls output/*tx -l | wc -l` "!= 13"
         return 1
     fi
     echo "Truffle test succeded"
@@ -107,7 +107,7 @@ run_truffle_tests(){
 run_tests_from_dir() {
     DIR=$1
     coverage erase
-    coverage run -m unittest discover -c -v "tests/$DIR" 2>&1 >/dev/null | tee travis_tests.log
+    coverage run -m unittest discover "tests/$DIR" 2>&1 >/dev/null | tee travis_tests.log
     DID_OK=$(tail -n1 travis_tests.log)
     if [[ "${DID_OK}" != OK* ]]; then
         echo "Some tests failed :("
@@ -138,11 +138,13 @@ run_examples() {
 case $1 in
     ethereum_vm)
         make_vmtests
-        install_truffle
-        run_truffle_tests
-        RV=$?
         echo "Running only the tests from 'tests/$1' directory"
         run_tests_from_dir $1
+        RV=$?
+
+	echo "Running truffle test"
+        install_truffle
+        run_truffle_tests
         RV=$(($RV + $?))
         ;;
 
diff --git a/tests/ethereum/test_consensys_benchmark.py b/tests/ethereum/test_consensys_benchmark.py
index 029bac95c..7bcac10c1 100644
--- a/tests/ethereum/test_consensys_benchmark.py
+++ b/tests/ethereum/test_consensys_benchmark.py
@@ -3,7 +3,7 @@
 import os
 import shutil
 from manticore.ethereum.plugins import LoopDepthLimiter, KeepOnlyIfStorageChanges
-
+from manticore.utils import log
 
 from manticore.ethereum import (
     ManticoreEVM,
@@ -20,8 +20,7 @@ class EthBenchmark(unittest.TestCase):
 
     def setUp(self):
         self.mevm = ManticoreEVM()
-        self.mevm.register_plugin(KeepOnlyIfStorageChanges())
-        self.mevm.verbosity(0)
+        log.set_verbosity(0)
         self.worksp = self.mevm.workspace
 
     def tearDown(self):
@@ -45,6 +44,7 @@ def _test(self, name, should_find, use_ctor_sym_arg=False):
             ctor_arg = ()
 
         mevm.multi_tx_analysis(filename, contract_name="Benchmark", args=ctor_arg)
+        mevm.finalize()
 
         expected_findings = set(((c, d) for b, c, d in should_find))
         actual_findings = set(((c, d) for a, b, c, d in mevm.global_findings))
diff --git a/tests/ethereum/test_detectors.py b/tests/ethereum/test_detectors.py
index 4056faab1..9e0f60b70 100644
--- a/tests/ethereum/test_detectors.py
+++ b/tests/ethereum/test_detectors.py
@@ -24,7 +24,7 @@
 )
 from manticore.ethereum.plugins import LoopDepthLimiter, KeepOnlyIfStorageChanges
 
-from manticore.utils import config
+from manticore.utils import config, log
 
 consts = config.get_group("core")
 consts.mprocessing = consts.mprocessing.single
@@ -48,7 +48,7 @@ class EthDetectorTest(unittest.TestCase):
     def setUp(self):
         self.mevm = ManticoreEVM()
         self.mevm.register_plugin(KeepOnlyIfStorageChanges())
-        self.mevm.verbosity(0)
+        log.set_verbosity(0)
         self.worksp = self.mevm.workspace
 
     def tearDown(self):
@@ -76,9 +76,9 @@ def _test(self, name, should_find, use_ctor_sym_arg=False):
                 filepath,
                 contract_name="DetectThis",
                 args=ctor_arg,
-                crytic_compile_args={"solc_working_dir": dir},
+                compile_args={"solc_working_dir": dir},
             )
-
+        mevm.finalize()
         expected_findings = set(((finding, at_init) for finding, at_init in should_find))
         actual_findings = set(
             ((finding, at_init) for _addr, _pc, finding, at_init in mevm.global_findings)
diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py
index 357abdadd..ebf604ef2 100644
--- a/tests/ethereum/test_general.py
+++ b/tests/ethereum/test_general.py
@@ -53,6 +53,7 @@ def test_int_ovf(self):
         mevm.register_detector(DetectIntegerOverflow())
         filename = os.path.join(THIS_DIR, "contracts/int_overflow.sol")
         mevm.multi_tx_analysis(filename, tx_limit=1)
+        mevm.finalize()
         self.assertEqual(len(mevm.global_findings), 3)
         all_findings = "".join([x[2] for x in mevm.global_findings])
         self.assertIn("Unsigned integer overflow at SUB instruction", all_findings)
@@ -1001,6 +1002,7 @@ def did_evm_execute_instruction_callback(self, state, instruction, arguments, re
                         with self.locked_context(name) as d:
                             d.append(instruction.pc)
                 except Exception as e:
+                    print(e)
                     raise
 
         mevm = self.mevm
@@ -1105,6 +1107,7 @@ def test_event_forwarding_after_state_fork_during_message_call(self):
         attacker = m.create_account(name="attacker", balance=0)
 
         wallet.luckyNumber(m.make_symbolic_value(), caller=attacker)
+        m.finalize()
 
         self.assertListEqual([x[2] for x in m.global_findings], ["Reachable ether leak to sender"])
 
@@ -1361,74 +1364,6 @@ def inner_func(self, a, b):
         inner_func(None, self.bv, 123)
 
 
-class EthSolidityCompilerTest(unittest.TestCase):
-    def test_run_solc(self):
-        source_a = """
-        import "./B.sol";
-        contract A {
-            function callB(B _b) public { _b.fromA(); }
-            function fromB() public { revert(); }
-        }
-        """
-        source_b = """
-        import "./A.sol";
-        contract B {
-            function callA(A _a) public { _a.fromB(); }
-            function fromA() public { revert(); }
-        }
-        """
-        tmp_dir = tempfile.mkdtemp()
-        try:
-            with open(os.path.join(tmp_dir, "A.sol"), "w") as a, open(
-                os.path.join(tmp_dir, "B.sol"), "w"
-            ) as b:
-                a.write(source_a)
-                a.flush()
-                b.write(source_b)
-                b.flush()
-                output, warnings = ManticoreEVM._run_solc(a, working_dir=tmp_dir)
-                source_list = output.get("sourceList", [])
-                self.assertIn(os.path.split(a.name)[-1], source_list)
-                self.assertIn(os.path.split(b.name)[-1], source_list)
-        finally:
-            shutil.rmtree(tmp_dir)
-
-    def test_run_solc_with_remappings(self):
-        source_a = """
-        import "test/B.sol";
-        contract A {
-            function callB(B _b) public { _b.fromA(); }
-            function fromB() public { revert(); }
-        }
-        """
-        source_b = """
-        import "../A.sol";
-        contract B {
-            function callA(A _a) public { _a.fromB(); }
-            function fromA() public { revert(); }
-        }
-        """
-        tmp_dir = tempfile.mkdtemp()
-        lib_dir = os.path.join(tmp_dir, "lib")
-        os.makedirs(lib_dir)
-        try:
-            with open(os.path.join(tmp_dir, "A.sol"), "w") as a, open(
-                os.path.join(lib_dir, "B.sol"), "w"
-            ) as b:
-                a.write(source_a)
-                a.flush()
-                b.write(source_b)
-                b.flush()
-                output, warnings = ManticoreEVM._run_solc(
-                    a, solc_remaps=["test=lib"], working_dir=tmp_dir
-                )
-                source_list = output.get("sourceList", [])
-                self.assertIn("A.sol", source_list)
-                self.assertIn("lib/B.sol", source_list)
-        finally:
-            shutil.rmtree(tmp_dir)
-
-
 class EthSolidityMetadataTests(unittest.TestCase):
     def test_tuple_signature_for_components(self):
         self.assertEqual(SolidityMetadata.tuple_signature_for_components([]), "()")
@@ -1599,30 +1534,6 @@ def test_overloaded_functions_and_events(self):
             )
 
 
-class TruffleTests(unittest.TestCase):
-    def test_truffle_contract_schema(self):
-        filename = os.path.join(THIS_DIR, "data/MetaCoin.json")
-        with open(filename, "rb") as f:
-            truffle_json = f.read()
-        m = ManticoreEVM()
-        user_account = m.create_account(balance=1000, name="user_account")
-        contract_account = m.json_create_contract(
-            truffle_json, owner=user_account, name="contract_account"
-        )
-        md: SolidityMetadata = m.get_metadata(contract_account)
-        self.assertEqual(
-            md.runtime_bytecode,
-            b"```@Rc\xff\xff\xff\xff`\xe0`\x02\n`\x005\x04\x16c{\xd7\x03\xe8\x81\x14a\x007W\x80c\x90\xb9\x8a\x11\x14a\x00eW\x80c\xf8\xb2\xcbO\x14a\x00\x98W[\xfe[4\x15a\x00?W\xfe[a\x00S`\x01`\xa0`\x02\n\x03`\x045\x16a\x00\xc6V[`@\x80Q\x91\x82RQ\x90\x81\x90\x03` \x01\x90\xf3[4\x15a\x00mW\xfe[a\x00\x84`\x01`\xa0`\x02\n\x03`\x045\x16`$5a\x01MV[`@\x80Q\x91\x15\x15\x82RQ\x90\x81\x90\x03` \x01\x90\xf3[4\x15a\x00\xa0W\xfe[a\x00S`\x01`\xa0`\x02\n\x03`\x045\x16a\x01\xe5V[`@\x80Q\x91\x82RQ\x90\x81\x90\x03` \x01\x90\xf3[`\x00s{\xccc\xd4W\x90\xe2?n\x9b\xc3QN\x1a\xb5\xafd\x93\x02\xd0c\x96\xe4\xee=a\x00\xeb\x84a\x01\xe5V[`\x02`\x00`@Q` \x01R`@Q\x83c\xff\xff\xff\xff\x16`\xe0`\x02\n\x02\x81R`\x04\x01\x80\x83\x81R` \x01\x82\x81R` \x01\x92PPP` `@Q\x80\x83\x03\x81\x86\x80;\x15\x15a\x010W\xfe[a\x02\xc6Z\x03\xf4\x15\x15a\x01>W\xfe[PP`@QQ\x91PP[\x91\x90PV[`\x01`\xa0`\x02\n\x033\x16`\x00\x90\x81R` \x81\x90R`@\x81 T\x82\x90\x10\x15a\x01vWP`\x00a\x01\xdfV[`\x01`\xa0`\x02\n\x033\x81\x16`\x00\x81\x81R` \x81\x81R`@\x80\x83 \x80T\x88\x90\x03\x90U\x93\x87\x16\x80\x83R\x91\x84\x90 \x80T\x87\x01\x90U\x83Q\x86\x81R\x93Q\x91\x93\x7f\xdd\xf2R\xad\x1b\xe2\xc8\x9bi\xc2\xb0h\xfc7\x8d\xaa\x95+\xa7\xf1c\xc4\xa1\x16(\xf5ZM\xf5#\xb3\xef\x92\x90\x81\x90\x03\x90\x91\x01\x90\xa3P`\x01[\x92\x91PPV[`\x01`\xa0`\x02\n\x03\x81\x16`\x00\x90\x81R` \x81\x90R`@\x90 T[\x91\x90PV\x00",
-        )
-        self.assertEqual(
-            md.init_bytecode,
-            b"```@R4\x15a\x00\x0cW\xfe[[`\x01`\xa0`\x02\n\x032\x16`\x00\x90\x81R` \x81\x90R`@\x90 a'\x10\x90U[[a\x020\x80a\x00;`\x009`\x00\xf3\x00```@Rc\xff\xff\xff\xff`\xe0`\x02\n`\x005\x04\x16c{\xd7\x03\xe8\x81\x14a\x007W\x80c\x90\xb9\x8a\x11\x14a\x00eW\x80c\xf8\xb2\xcbO\x14a\x00\x98W[\xfe[4\x15a\x00?W\xfe[a\x00S`\x01`\xa0`\x02\n\x03`\x045\x16a\x00\xc6V[`@\x80Q\x91\x82RQ\x90\x81\x90\x03` \x01\x90\xf3[4\x15a\x00mW\xfe[a\x00\x84`\x01`\xa0`\x02\n\x03`\x045\x16`$5a\x01MV[`@\x80Q\x91\x15\x15\x82RQ\x90\x81\x90\x03` \x01\x90\xf3[4\x15a\x00\xa0W\xfe[a\x00S`\x01`\xa0`\x02\n\x03`\x045\x16a\x01\xe5V[`@\x80Q\x91\x82RQ\x90\x81\x90\x03` \x01\x90\xf3[`\x00s{\xccc\xd4W\x90\xe2?n\x9b\xc3QN\x1a\xb5\xafd\x93\x02\xd0c\x96\xe4\xee=a\x00\xeb\x84a\x01\xe5V[`\x02`\x00`@Q` \x01R`@Q\x83c\xff\xff\xff\xff\x16`\xe0`\x02\n\x02\x81R`\x04\x01\x80\x83\x81R` \x01\x82\x81R` \x01\x92PPP` `@Q\x80\x83\x03\x81\x86\x80;\x15\x15a\x010W\xfe[a\x02\xc6Z\x03\xf4\x15\x15a\x01>W\xfe[PP`@QQ\x91PP[\x91\x90PV[`\x01`\xa0`\x02\n\x033\x16`\x00\x90\x81R` \x81\x90R`@\x81 T\x82\x90\x10\x15a\x01vWP`\x00a\x01\xdfV[`\x01`\xa0`\x02\n\x033\x81\x16`\x00\x81\x81R` \x81\x81R`@\x80\x83 \x80T\x88\x90\x03\x90U\x93\x87\x16\x80\x83R\x91\x84\x90 \x80T\x87\x01\x90U\x83Q\x86\x81R\x93Q\x91\x93\x7f\xdd\xf2R\xad\x1b\xe2\xc8\x9bi\xc2\xb0h\xfc7\x8d\xaa\x95+\xa7\xf1c\xc4\xa1\x16(\xf5ZM\xf5#\xb3\xef\x92\x90\x81\x90\x03\x90\x91\x01\x90\xa3P`\x01[\x92\x91PPV[`\x01`\xa0`\x02\n\x03\x81\x16`\x00\x90\x81R` \x81\x90R`@\x90 T[\x91\x90PV\x00",
-        )
-        self.assertSequenceEqual(
-            md.function_selectors, (b"{\xd7\x03\xe8", b"\x90\xb9\x8a\x11", b"\xf8\xb2\xcbO")
-        )
-
-
 class EthSpecificTxIntructionTests(unittest.TestCase):
     def test_jmpdest_check(self):
         """

From b667b983887b6ac4bdd1fd022b23184e87b07e7b Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Mon, 16 Sep 2019 14:56:10 -0300
Subject: [PATCH 02/37] Add test for ULE

---
 manticore/platforms/evm.py   |  1 -
 tests/other/test_smtlibv2.py | 17 +++++++++++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index 16ad10771..0aaa6e3ba 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -1694,7 +1694,6 @@ def CALLDATACOPY(self, mem_offset, data_offset, size):
                 x = self.constraints.new_bitvec(8, name="temp{}".format(uuid.uuid1()))
                 self.constraints.add(x == c)
             self._store(mem_offset + i, x)
-            # print (str(self.constraints))
 
     def CODESIZE(self):
         """Get size of code running in current environment"""
diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py
index 2de08ee01..8a07b1adc 100644
--- a/tests/other/test_smtlibv2.py
+++ b/tests/other/test_smtlibv2.py
@@ -835,6 +835,23 @@ def test_SDIV(self):
         self.assertTrue(solver.check(cs))
         self.assertEqual(solver.get_value(cs, a), -7 & 0xFF)
 
+    def test_ULE(self):
+        solver = Z3Solver.instance()
+        cs = ConstraintSet()
+        a = cs.new_bitvec(8)
+        b = cs.new_bitvec(8)
+        c = cs.new_bitvec(8)
+
+        cs.add(a == 0x1)  # 1
+        cs.add(b == 0x86)  # -122
+        cs.add(c == 0x11)  # 17
+        self.assertTrue(solver.must_be_true(cs, Operators.ULE(a, b)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULE(a, c)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULE(c, b)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULE(a, 0xF2)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULE(b, 0xF9)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULE(c, 0xF2)))
+
     def test_check_solver_min(self):
         self.solver._received_version = '(:version "4.4.1")'
         self.assertTrue(self.solver._solver_version() == Version(major=4, minor=4, patch=1))

From 9665aa124c37f33afc3cd09615c7f231ad38ee98 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Mon, 16 Sep 2019 16:20:44 -0300
Subject: [PATCH 03/37] More operators tests

---
 manticore/core/smtlib/operators.py |  7 -----
 manticore/native/cpu/x86.py        |  2 +-
 tests/other/test_smtlibv2.py       | 44 ++++++++++++++++++++++++++++--
 3 files changed, 43 insertions(+), 10 deletions(-)

diff --git a/manticore/core/smtlib/operators.py b/manticore/core/smtlib/operators.py
index fbc8f5011..2db6b3304 100644
--- a/manticore/core/smtlib/operators.py
+++ b/manticore/core/smtlib/operators.py
@@ -71,13 +71,6 @@ def OR(a, b, *others):
     return result
 
 
-def XOR(a, b):
-    result = a ^ b
-    if isinstance(result, (BitVec, int)):
-        result = ITE(result != 0, True, False)
-    return result
-
-
 def UGT(a, b):
     if isinstance(a, BitVec):
         return a.ugt(b)
diff --git a/manticore/native/cpu/x86.py b/manticore/native/cpu/x86.py
index 0f13766ee..f3f79147d 100644
--- a/manticore/native/cpu/x86.py
+++ b/manticore/native/cpu/x86.py
@@ -1077,7 +1077,7 @@ def XOR(cpu, dest, src):
         """
         Logical exclusive OR.
 
-        Performs a bitwise exclusive Operators.OR(XOR) operation on the destination (first)
+        Performs a bitwise exclusive-OR(XOR) operation on the destination (first)
         and source (second) operands and stores the result in the destination
         operand location.
 
diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py
index 8a07b1adc..8e8902177 100644
--- a/tests/other/test_smtlibv2.py
+++ b/tests/other/test_smtlibv2.py
@@ -111,6 +111,8 @@ def testBool(self):
         bf = BoolConstant(False)
         bt = BoolConstant(True)
         cs.add(Operators.AND(bf, bt))
+        cs.add(Operators.AND(bf, bt, bt, bt))
+        cs.add(Operators.OR(True, bf))
         self.assertFalse(self.solver.check(cs))
 
     def testBasicArray(self):
@@ -849,8 +851,46 @@ def test_ULE(self):
         self.assertTrue(solver.must_be_true(cs, Operators.ULE(a, c)))
         self.assertTrue(solver.must_be_true(cs, Operators.ULE(c, b)))
         self.assertTrue(solver.must_be_true(cs, Operators.ULE(a, 0xF2)))
-        self.assertTrue(solver.must_be_true(cs, Operators.ULE(b, 0xF9)))
-        self.assertTrue(solver.must_be_true(cs, Operators.ULE(c, 0xF2)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULE(b, 0x99)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULE(c, 0x12)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULE(3, 0xF2)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULE(3, 3)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULE(1, a)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULE(0x85, b)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULE(0x10, c)))
+
+    def test_ULT(self):
+        solver = Z3Solver.instance()
+        cs = ConstraintSet()
+        a = cs.new_bitvec(8)
+        b = cs.new_bitvec(8)
+        c = cs.new_bitvec(8)
+
+        cs.add(a == 0x1)  # 1
+        cs.add(b == 0x86)  # -122
+        cs.add(c == 0x11)  # 17
+        self.assertTrue(solver.must_be_true(cs, Operators.ULT(a, b)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULT(a, c)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULT(c, b)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULT(a, 0xF2)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULT(b, 0x99)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULT(c, 0x12)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULT(3, 0xF2)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULT(3, 4)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULT(0, a)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULT(0x85, b)))
+        self.assertTrue(solver.must_be_true(cs, Operators.ULT(0x10, c)))
+
+    def test_NOT(self):
+        solver = Z3Solver.instance()
+        cs = ConstraintSet()
+        a = cs.new_bitvec(8)
+        b = cs.new_bitvec(8)
+
+        cs.add(a == 0x1)  # 1
+        cs.add(b == 0x86)  # -122
+        self.assertTrue(solver.must_be_true(cs, Operators.NOT(False)))
+        self.assertTrue(solver.must_be_true(cs, Operators.NOT(a == b)))
 
     def test_check_solver_min(self):
         self.solver._received_version = '(:version "4.4.1")'

From d02125781e4d798b7c630021daf5c10dd8454e19 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Mon, 16 Sep 2019 17:38:31 -0300
Subject: [PATCH 04/37] remove TT

---
 manticore/ethereum/manticore.py | 63 ++++++++++-----------------------
 1 file changed, 18 insertions(+), 45 deletions(-)

diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index 4465a07f7..a6ec40d3a 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -49,8 +49,6 @@ class Sha3Type(Enum):
 
     concretize = "concretize"
     symbolicate = "symbolicate"
-    timetravel = "timetravel"
-    functions = "functions"
 
     def title(self):
         return self._name_.title()
@@ -65,7 +63,7 @@ def from_string(cls, name):
 consts.add(
     "sha3",
     default=Sha3Type.concretize,
-    description="concretize(*): sound simple concretization\nsymbolicate: unsound symbolication with gout of cycle FP killing\ntimetravel: best effort is done on the spot using current and future information :-O\nfunctions: sha3 is replaced by a uninstantiated function, requires solver support",
+    description="concretize(*): sound simple concretization\nsymbolicate: unsound symbolication with gout of cycle FP killing",
 )
 
 
@@ -396,8 +394,6 @@ def __init__(self, workspace_url: str = None, policy: str = "random"):
         self.subscribe("will_terminate_state", self._terminate_state_callback)
         self.subscribe("did_evm_execute_instruction", self._did_evm_execute_instruction_callback)
         consts.sha3 = consts.sha3.symbolicate
-        if consts.sha3 is consts.sha3.timetravel:
-            self.subscribe("on_symbolic_function", self._on_timetravel)
         elif consts.sha3 is consts.sha3.concretize:
             self.subscribe("on_symbolic_function", self._on_concretize)
         elif consts.sha3 is consts.sha3.symbolicate:
@@ -1130,34 +1126,6 @@ def _on_concretize(self, state, func, data, result):
 
         result.append(y_concrete)
 
-    def _on_timetravel(self, state, func, data, result):
-        if issymbolic(data):
-            # will be updated with the buf->hash pairs to use
-            known_hashes = {}
-            # This updates the local copy of sha3 with the pairs we need to explore
-            self._on_symbolic_sha3_callback_tt(state, data, known_hashes)
-
-            # This builds a symbol in `value` that represents all the known sha3
-            # as reported by ManticoreEVM
-            value = None  # never used
-            known_hashes_cond = False
-            for key, hsh in known_hashes.items():
-                # Ignore the key if the size wont match
-                if len(key) == len(data):
-                    cond = key == data
-                    if known_hashes_cond is False:
-                        value = hsh
-                        known_hashes_cond = cond
-                    else:
-                        value = Operators.ITEBV(256, cond, hsh, value)
-                        known_hashes_cond = Operators.OR(cond, known_hashes_cond)
-        else:
-            value = func(data)
-            self._on_concrete_sha3_callback_tt(state, data, value)
-            logger.info("Found a concrete SHA3 example %r -> %x", data, value)
-
-        result.append(value)
-
     # Callbacks
     def _on_symbolic_sha3_callback_tt(self, state, data, known_hashes):
         """ INTERNAL USE """
@@ -1288,18 +1256,22 @@ def on_unsound_symbolication(self, state, func, data, result):
             # lets make a fresh 256 bit symbol representing any potential hash
             value = state.new_symbolic_value(256)
 
-            # bijectiveness
-            for i in range(len(symbolic_pairs)):
-                xa, ya = symbolic_pairs[i]
-                if len(xa) == len(data):
-                    constraint = simplify((xa == data) == (ya == value))
-                else:
-                    constraint = ya != value
-                state.constrain(constraint)  # bijective
-
-            symbolic_pairs.append((data, value))
-            state.context[f"symbolic_func_sym_{name}"] = symbolic_pairs
-            # let it return just new_hash
+            for x,y in symbolic_pairs:
+                if state.must_be_true(Operators.OR(x==data, y==value)):
+                    constraint = simplify((x == data) == (y == value))
+                    state.constrain(constraint)
+                    data, value = x, y
+                    break
+            else:
+                # bijectiveness
+                for xa, ya in symbolic_pairs:
+                    if len(xa) == len(data):
+                        constraint = simplify((xa == data) == (ya == value))
+                    else:
+                        constraint = ya != value
+                    state.constrain(constraint)  # bijective
+                symbolic_pairs.append((data, value))
+                state.context[f"symbolic_func_sym_{name}"] = symbolic_pairs
         else:
             value = func(data)
             with self.locked_context("ethereum", dict) as ethereum_context:
@@ -1311,6 +1283,7 @@ def on_unsound_symbolication(self, state, func, data, result):
             state.context[f"symbolic_func_conc_{name}"] = concrete_pairs
             logger.info(f"Found a concrete {name} {data} -> {value}")
 
+        # let it return just new_hash
         result.append(value)
 
     def fix_unsound_symbolication(self, state):

From 87df083c578cbaf148ab7273fc739db0f2a35206 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Mon, 16 Sep 2019 17:41:04 -0300
Subject: [PATCH 05/37] remove TT

---
 manticore/ethereum/manticore.py | 82 ---------------------------------
 1 file changed, 82 deletions(-)

diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index a6ec40d3a..e91b1db27 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -1126,88 +1126,6 @@ def _on_concretize(self, state, func, data, result):
 
         result.append(y_concrete)
 
-    # Callbacks
-    def _on_symbolic_sha3_callback_tt(self, state, data, known_hashes):
-        """ INTERNAL USE """
-        assert issymbolic(data), "Data should be symbolic here!"
-        with self.locked_context("ethereum") as context:
-            known_sha3 = context.get("_known_sha3", None)
-            if known_sha3 is None:
-                known_sha3 = set()
-
-            sha3_states = context.get("_sha3_states", None)
-            if sha3_states is None:
-                sha3_states = dict()
-            results = []
-            # If know_hashes is true then there is a _known_ solution for the hash
-            known_hashes_cond = False
-            for key, value in known_sha3:
-                assert not issymbolic(key), "Saved sha3 data,hash pairs should be concrete"
-                cond = key == data
-                # TODO consider disabling this solver query.
-                if not state.can_be_true(cond):
-                    continue
-                results.append((key, value))
-                known_hashes_cond = Operators.OR(cond, known_hashes_cond)
-
-            # adding a single random example so we can explore further
-            if not results or state.can_be_true(known_hashes_cond == False):
-                with state as temp:
-                    temp.constrain(known_hashes_cond == False)
-                    data_concrete = temp.solve_one(data)
-                data_hash = int(sha3.keccak_256(data_concrete).hexdigest(), 16)
-                results.append((data_concrete, data_hash))
-                known_hashes_cond = Operators.OR(data_concrete == data, known_hashes_cond)
-                known_sha3.add((data_concrete, data_hash))
-
-            not_known_hashes_cond = Operators.NOT(known_hashes_cond)
-
-            # We need to fork/save the state
-            #################################
-            # save the state to secondary storage
-            # Build and enqueue a state for each solution
-            with state as temp_state:
-                if temp_state.can_be_true(not_known_hashes_cond):
-                    temp_state.constrain(not_known_hashes_cond)
-                    state_id = self._workspace.save_state(temp_state)
-                    # Save the size of the input buffer and all known hashes so
-                    # we awake this state only when a _new_ sha3 pair for _this_
-                    # size is found
-                    sha3_states[state_id] = (len(data), [hsh for buf, hsh in known_sha3])
-            context["_sha3_states"] = sha3_states
-            context["_known_sha3"] = known_sha3
-
-            if not state.can_be_true(known_hashes_cond):
-                raise TerminateState("There is no matching sha3 pair, bailing out")
-            state.constrain(known_hashes_cond)
-
-            # send known hashes to evm
-            known_hashes.update(results)
-
-    def _on_concrete_sha3_callback_tt(self, state, buf, value):
-        """ INTERNAL USE """
-        with self.locked_context("ethereum", dict) as ethereum_context:
-            known_sha3 = ethereum_context.get("_known_sha3", None)
-            if known_sha3 is None:
-                known_sha3 = set()
-
-            sha3_states = ethereum_context.get("_sha3_states", None)
-            if sha3_states is None:
-                sha3_states = dict()
-
-            for sha3_state_id, (size, hashes) in sha3_states.items():
-                if size == len(buf) and value not in hashes:
-                    sha3_states.remove(sha3_state_id)
-
-                    # locked at locked_context()
-                    # Enqueue it in the ready state list for processing
-                    self._ready_states.append(sha3_state_id)
-                    self._lock.notify_all()
-
-            known_sha3.add((buf, value))
-            ethereum_context["_known_sha3"] = known_sha3
-            ethereum_context["_sha3_states"] = sha3_states
-
     # Callbacks for generic SYMB TABLE
     def on_unsound_symbolication(self, state, func, data, result):
         """Apply the function func to data

From ee2dea14edaa650738ef14fe9c4af563699b9cde Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Mon, 16 Sep 2019 17:45:00 -0300
Subject: [PATCH 06/37] remove TT

---
 manticore/ethereum/manticore.py | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index e91b1db27..f65da766d 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -394,7 +394,7 @@ def __init__(self, workspace_url: str = None, policy: str = "random"):
         self.subscribe("will_terminate_state", self._terminate_state_callback)
         self.subscribe("did_evm_execute_instruction", self._did_evm_execute_instruction_callback)
         consts.sha3 = consts.sha3.symbolicate
-        elif consts.sha3 is consts.sha3.concretize:
+        if consts.sha3 is consts.sha3.concretize:
             self.subscribe("on_symbolic_function", self._on_concretize)
         elif consts.sha3 is consts.sha3.symbolicate:
             self.subscribe("on_symbolic_function", self.on_unsound_symbolication)
@@ -1174,8 +1174,8 @@ def on_unsound_symbolication(self, state, func, data, result):
             # lets make a fresh 256 bit symbol representing any potential hash
             value = state.new_symbolic_value(256)
 
-            for x,y in symbolic_pairs:
-                if state.must_be_true(Operators.OR(x==data, y==value)):
+            for x, y in symbolic_pairs:
+                if state.must_be_true(Operators.OR(x == data, y == value)):
                     constraint = simplify((x == data) == (y == value))
                     state.constrain(constraint)
                     data, value = x, y

From fd55973cba8e453000a6044ed74ac042ccc7dff6 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Mon, 16 Sep 2019 20:15:54 -0300
Subject: [PATCH 07/37] Add test for simple sha3 concretization

---
 manticore/ethereum/manticore.py |   1 -
 tests/ethereum/test_sha3.py     | 484 ++++++++++++++++++++++++++++++++
 2 files changed, 484 insertions(+), 1 deletion(-)
 create mode 100644 tests/ethereum/test_sha3.py

diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index f65da766d..7222bcd44 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -399,7 +399,6 @@ def __init__(self, workspace_url: str = None, policy: str = "random"):
         elif consts.sha3 is consts.sha3.symbolicate:
             self.subscribe("on_symbolic_function", self.on_unsound_symbolication)
         else:
-            # if consts.sha3 is consts.sha3.function:
             raise NotImplemented
 
         self._accounts = dict()
diff --git a/tests/ethereum/test_sha3.py b/tests/ethereum/test_sha3.py
new file mode 100644
index 000000000..b2f4a05ce
--- /dev/null
+++ b/tests/ethereum/test_sha3.py
@@ -0,0 +1,484 @@
+"""
+File name is purposefully not test_* to run this test separately.
+"""
+
+import inspect
+import unittest
+
+import os
+import shutil
+from manticore.platforms.evm import EVMWorld
+from manticore.core.smtlib import operators, ConstraintSet
+from manticore.ethereum import ManticoreEVM
+from manticore.ethereum.plugins import KeepOnlyIfStorageChanges
+from manticore.utils import config
+
+consts = config.get_group("core")
+consts.mprocessing = consts.mprocessing.single
+
+THIS_DIR = os.path.dirname(os.path.abspath(__file__))
+
+
+class EthSha3Test(unittest.TestCase):
+    """
+    Subclasses must assign this class variable to the class for the detector
+    """
+
+    DETECTOR_CLASS = None
+
+    def setUp(self):
+        evm_consts = config.get_group("evm")
+        evm_consts.sha3 = evm_consts.sha3.symbolicate
+
+        self.mevm = ManticoreEVM()
+        self.worksp = self.mevm.workspace
+
+    def tearDown(self):
+        self.mevm = None
+        shutil.rmtree(self.worksp)
+
+    def ManticoreEVM(self):
+        return self.mevm
+
+    def test_example1(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint input) payable public{
+                if (sha3(input) == 0x12341234){
+                    emit Log("Found a bug");
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=1000, name="owner")
+        attacker = m.create_account(balance=1000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        symbolic_input = m.make_symbolic_value()
+        contract.foo(symbolic_input)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 0)  # log is not reachable
+        self.assertEqual(m.count_all_states(), 1)
+
+    def test_example2(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint x, uint y) payable public{
+                if (x == uint256(sha3(y))){
+                    emit Log("Found a bug");
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=1000, name="owner")
+        attacker = m.create_account(balance=1000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        x = m.make_symbolic_value()
+        y = m.make_symbolic_value()
+        contract.foo(x, y)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)  # log is reachable
+        self.assertEqual(m.count_all_states(), 2)
+
+    def test_example3(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint x, uint y) payable public{
+                if (sha3(x) == sha3(y)){
+                    emit Log("Found a bug");
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=1000, name="owner")
+        attacker = m.create_account(balance=1000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        x = m.make_symbolic_value()
+        y = m.make_symbolic_value()
+        contract.foo(x, y)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)
+        # x == y #log
+        # x != y
+        self.assertEqual(m.count_all_states(), 2)
+
+    def test_example4(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint x, uint y) payable public{
+                if (sha3(x) == sha3(y)){
+                    if (x != 10) {
+                        emit Log("Found a bug"); //Reachable 
+                    }
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=1000, name="owner")
+        attacker = m.create_account(balance=1000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        x = m.make_symbolic_value()
+        y = m.make_symbolic_value()
+        contract.foo(x, y)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)  # log is reachable
+
+        # x==10 && y == 10
+        # x==C  && y == C && C != 10   #log
+        # x != y
+        self.assertEqual(m.count_all_states(), 3)
+
+    def test_example5(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint x, uint y) payable public{
+                if (sha3(x) == sha3(y)){
+                    if (x != 10 && y != 10) {
+                        emit Log("Found a bug"); //Reachable 
+                    }
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=1000, name="owner")
+        attacker = m.create_account(balance=1000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        x = m.make_symbolic_value()
+        y = m.make_symbolic_value()
+        contract.foo(x, y)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)  # log is reachable
+        # x==10 && y == 10
+        # x==C  && y == C && C != 10 #log
+        # x != y
+        self.assertEqual(m.count_all_states(), 3)
+
+    def test_example6(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint x, uint y) payable public{
+                if (x == uint256(sha3(y))){
+                    if(y == 10){
+                        emit Log("Found a bug");
+                    }
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=1000, name="owner")
+        attacker = m.create_account(balance=1000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        x = m.make_symbolic_value()
+        y = m.make_symbolic_value()
+        contract.foo(x, y)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)  # log is reachable
+
+        # x==sha3(10) && y == 10
+        # x==sha3(C) && y == C  && C!=10
+        # x==sha3(C)  && y != C
+        self.assertEqual(m.count_all_states(), 3)
+
+    def test_example7(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint x, uint y) payable public{
+                if (sha3(x) == sha3(y)){
+                    if (x == 10) {
+                        emit Log("Found a bug"); //Reachable 
+                    }
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=1000, name="owner")
+        attacker = m.create_account(balance=1000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        x = m.make_symbolic_value()
+        y = m.make_symbolic_value()
+        contract.foo(x, y)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)  # log is reachable
+
+        # x==y && x == 10
+        # x==y && x != 10
+        # x!=y
+        self.assertEqual(m.count_all_states(), 3)
+
+    def test_example8(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint x, uint y) payable public{
+                if (sha3(x) == sha3(y)){
+                    if (x == 10) {
+                        emit Log("Found a bug"); //Reachable 
+                    }
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=1000, name="owner")
+        attacker = m.create_account(balance=1000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        x = m.make_symbolic_value()
+        y = m.make_symbolic_value()
+        contract.foo(x, y)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)  # log is reachable
+
+        # x==y && x == 10
+        # x==y && x != 10
+        # x!=y
+        self.assertEqual(m.count_all_states(), 3)
+
+    def test_essence1(self):
+        source_code = """
+        contract I_Choose_Not_To_Run {
+            event Log(string);
+            function foo(bytes x) public {
+                // x1 keccak
+                if (keccak256("tob") == keccak256(abi.encodePacked(x))){
+                    emit Log("bug");
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=1000, name="owner")
+        attacker = m.create_account(balance=1000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        x = m.make_symbolic_buffer(3)
+        contract.foo(x)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                print("killed", st.id)
+                continue
+            m.generate_testcase(st)
+            found += len(st.platform.logs)
+        self.assertEqual(found, 1)  # log is reachable
+        self.assertEqual(m.count_all_states(), 2)
+
+    def test_essence2(self):
+        source_code = """
+        contract I_Choose_Not_To_Run {
+            event Log(string);
+            function foo(bytes x) public {
+                //# x10 keccak
+                if (keccak256(keccak256(keccak256(keccak256(keccak256(keccak256(keccak256(keccak256(keccak256(keccak256("tob")))))))))) == 
+                    keccak256(keccak256(keccak256(keccak256(keccak256(keccak256(keccak256(keccak256(keccak256(keccak256(abi.encodePacked(x)))))))))))){
+                    emit Log("bug");
+                }
+            }
+        }
+        """
+
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=1000, name="owner")
+        attacker = m.create_account(balance=1000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        x = m.make_symbolic_buffer(3)
+        contract.foo(x)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            m.generate_testcase(st)
+            found += len(st.platform.logs)
+        self.assertEqual(found, 1)  # log is reachable
+        self.assertEqual(m.count_all_states(), 2)
+
+    def test_essence3(self):
+        source_code = """contract Sha3_Multiple_tx{
+            event Log(string);
+            bytes32 val;
+            function foo(uint x) public {
+                if (x == 12345){
+                    val = keccak256(keccak256(uint(6789)));
+                }
+                else{
+                    if (keccak256(val) == keccak256(keccak256(keccak256(x)))){
+                        emit Log("bug");
+                    }
+                }
+            }
+        }
+
+        """
+
+        m = self.ManticoreEVM()
+        m.register_plugin(KeepOnlyIfStorageChanges())
+        owner = m.create_account(balance=1000, name="owner")
+        attacker = m.create_account(balance=1000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        x1 = m.make_symbolic_value()
+        contract.foo(x1)
+        x2 = m.make_symbolic_value()
+        contract.foo(x2)
+
+        self.assertEqual(m.count_all_states(), 5)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            m.generate_testcase(st)
+            found += len(st.platform.logs)
+        self.assertEqual(found, 1)  # log is reachable
+
+class EthSha3TestConcrete(unittest.TestCase):
+    """
+    Subclasses must assign this class variable to the class for the detector
+    """
+
+    DETECTOR_CLASS = None
+
+    def setUp(self):
+        evm_consts = config.get_group("evm")
+        evm_consts.sha3 = evm_consts.sha3.concretize
+
+        self.mevm = ManticoreEVM()
+        self.worksp = self.mevm.workspace
+
+    def tearDown(self):
+        self.mevm = None
+        shutil.rmtree(self.worksp)
+
+    def ManticoreEVM(self):
+        return self.mevm
+
+
+    def test_example_concrete_1(self):
+        source_code = """
+        contract IsThisVulnerable {
+            event Log(string);
+            function foo(uint x, uint y) payable public{
+                if (sha3(x) == sha3(y)){
+                    if (x != 10 && y != 10) {
+                        emit Log("Found a bug"); //Reachable 
+                    }
+                }
+            }
+        }
+        """
+        m = self.ManticoreEVM()
+        owner = m.create_account(balance=1000, name="owner")
+        attacker = m.create_account(balance=1000, name="attacker")
+        contract = m.solidity_create_contract(source_code, owner=owner, name="contract")
+
+        x = m.make_symbolic_value()
+        y = m.make_symbolic_value()
+        contract.foo(x, y)
+
+        found = 0
+        for st in m.all_states:
+            if not m.fix_unsound_symbolication(st):
+                m.kill_state(st)
+                continue
+            found += len(st.platform.logs)
+
+        self.assertEqual(found, 1)  # log is reachable
+        # x==10 && y == 10
+        # x==C  && y == C && C != 10 #log
+        # x != y
+        self.assertEqual(m.count_all_states(), 3)
+
+
+if __name__ == "__main__":
+    unittest.main()

From c8653b47e000ce12cfd5f7dec7041ce3a406d287 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Mon, 16 Sep 2019 20:16:30 -0300
Subject: [PATCH 08/37] Add test for simple sha3 concretization

---
 tests/ethereum/test_sha3.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/ethereum/test_sha3.py b/tests/ethereum/test_sha3.py
index b2f4a05ce..3bb0936d2 100644
--- a/tests/ethereum/test_sha3.py
+++ b/tests/ethereum/test_sha3.py
@@ -422,6 +422,7 @@ def test_essence3(self):
             found += len(st.platform.logs)
         self.assertEqual(found, 1)  # log is reachable
 
+
 class EthSha3TestConcrete(unittest.TestCase):
     """
     Subclasses must assign this class variable to the class for the detector
@@ -443,7 +444,6 @@ def tearDown(self):
     def ManticoreEVM(self):
         return self.mevm
 
-
     def test_example_concrete_1(self):
         source_code = """
         contract IsThisVulnerable {

From 482ed119ed5f6dfbf20639b038cde46c914698ed Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Tue, 17 Sep 2019 11:10:47 -0300
Subject: [PATCH 09/37] Add coverage to integration tests

---
 tests/native/test_integration_native.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/native/test_integration_native.py b/tests/native/test_integration_native.py
index d709656b5..79971c5d1 100644
--- a/tests/native/test_integration_native.py
+++ b/tests/native/test_integration_native.py
@@ -61,7 +61,7 @@ def test_timeout(self):
         with open(os.path.join(os.pardir, self.test_dir, "output.log"), "w") as output:
             subprocess.check_call(
                 [
-                    PYTHON_BIN,
+                    "coverage", "run", #PYTHON_BIN,
                     "-m",
                     "manticore",
                     "--workspace",

From e2ecac1f7a24c804b12d5b3409c95b3f2562e3d9 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Tue, 17 Sep 2019 11:11:05 -0300
Subject: [PATCH 10/37] Add coverage to integration tests

---
 tests/native/test_integration_native.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tests/native/test_integration_native.py b/tests/native/test_integration_native.py
index 79971c5d1..487ae59cd 100644
--- a/tests/native/test_integration_native.py
+++ b/tests/native/test_integration_native.py
@@ -61,7 +61,8 @@ def test_timeout(self):
         with open(os.path.join(os.pardir, self.test_dir, "output.log"), "w") as output:
             subprocess.check_call(
                 [
-                    "coverage", "run", #PYTHON_BIN,
+                    "coverage",
+                    "run",  # PYTHON_BIN,
                     "-m",
                     "manticore",
                     "--workspace",

From c8f3f2532873b33ed758afc54e4822f5c43650d8 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Mon, 23 Sep 2019 17:09:21 -0300
Subject: [PATCH 11/37] Added timeout to sha3 matching

---
 manticore/ethereum/manticore.py | 12 ++++++++----
 manticore/platforms/evm.py      |  2 +-
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index 7222bcd44..1b8bc446f 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -13,6 +13,7 @@
 import random
 import sha3
 import tempfile
+import time
 
 from crytic_compile import CryticCompile, InvalidCompilation, is_supported
 
@@ -65,6 +66,7 @@ def from_string(cls, name):
     default=Sha3Type.concretize,
     description="concretize(*): sound simple concretization\nsymbolicate: unsound symbolication with gout of cycle FP killing",
 )
+consts.add("sha3timeout", 60*20, "Default timeout for matching sha3 for unsound states (see unsound symbolication).")
 
 
 def flagged(flag):
@@ -1175,7 +1177,7 @@ def on_unsound_symbolication(self, state, func, data, result):
 
             for x, y in symbolic_pairs:
                 if state.must_be_true(Operators.OR(x == data, y == value)):
-                    constraint = simplify((x == data) == (y == value))
+                    constraint = simplify(Operators.AND(x == data, y == value))
                     state.constrain(constraint)
                     data, value = x, y
                     break
@@ -1221,7 +1223,7 @@ def concretize_known_pairs(state, symbolic_pairs, known_pairs):
                 if cond is False:
                     return
 
-        def match(state, func, symbolic_pairs, concrete_pairs, depth=0):
+        def match(state, func, symbolic_pairs, concrete_pairs, depth=0, start=None):
             """ Tries to find a concrete match for the symbolic pairs. It uses
             concrete_pairs (and potentially extends it with solved pairs) until
             a matching set of concrete pairs is found, or fail.
@@ -1232,6 +1234,8 @@ def match(state, func, symbolic_pairs, concrete_pairs, depth=0):
             concrete_pairs: Known of concrete pairs that may match some of the symbolic pairs
 
             """
+            if time.time() - start > consts.sha3timeout:
+                return False
 
             # The base case. No symbolic pairs. Just check if the state is feasible.
             if not symbolic_pairs:
@@ -1266,7 +1270,7 @@ def match(state, func, symbolic_pairs, concrete_pairs, depth=0):
                         seen = Operators.OR(Operators.AND(x == x_concrete, y == y_concrete), seen)
                 with state as temp_state:
                     temp_state.constrain(seen)
-                    if match(temp_state, func, new_symbolic_pairs, new_concrete_pairs, depth + 1):
+                    if match(temp_state, func, new_symbolic_pairs, new_concrete_pairs, depth + 1, start=start):
                         concrete_pairs.update(new_concrete_pairs)
                         return True
             return False
@@ -1286,7 +1290,7 @@ def match(state, func, symbolic_pairs, concrete_pairs, depth=0):
                 # symbolic_pairs = graph_sort(state, symbolic_pairs)
                 known_pairs = ethereum_context.get(f"symbolic_func_conc_{table}", set())
                 new_known_pairs = set(known_pairs)
-                if not match(state, functions[table], symbolic_pairs, new_known_pairs):
+                if not match(state, functions[table], symbolic_pairs, new_known_pairs, start=time.time()):
                     ethereum_context["soundcheck"] = False
                     return False
 
diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index 0aaa6e3ba..4c58a2603 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -1213,7 +1213,7 @@ def setstate(state, value):
             raise Concretize(
                 "Concretize PC", expression=expression, setstate=setstate, policy="ALL"
             )
-        # print(self)
+        #print(self)
         try:
             # import time
             # limbo = 0.0

From 7422bc059e0de1d052cdda5bf52249c80bf1bf84 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Mon, 23 Sep 2019 17:18:25 -0300
Subject: [PATCH 12/37] 2 files reformatted

---
 manticore/ethereum/manticore.py | 19 ++++++++++++++++---
 manticore/platforms/evm.py      |  2 +-
 2 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index 1b8bc446f..25cb24f46 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -66,7 +66,11 @@ def from_string(cls, name):
     default=Sha3Type.concretize,
     description="concretize(*): sound simple concretization\nsymbolicate: unsound symbolication with gout of cycle FP killing",
 )
-consts.add("sha3timeout", 60*20, "Default timeout for matching sha3 for unsound states (see unsound symbolication).")
+consts.add(
+    "sha3timeout",
+    60 * 20,
+    "Default timeout for matching sha3 for unsound states (see unsound symbolication).",
+)
 
 
 def flagged(flag):
@@ -1270,7 +1274,14 @@ def match(state, func, symbolic_pairs, concrete_pairs, depth=0, start=None):
                         seen = Operators.OR(Operators.AND(x == x_concrete, y == y_concrete), seen)
                 with state as temp_state:
                     temp_state.constrain(seen)
-                    if match(temp_state, func, new_symbolic_pairs, new_concrete_pairs, depth + 1, start=start):
+                    if match(
+                        temp_state,
+                        func,
+                        new_symbolic_pairs,
+                        new_concrete_pairs,
+                        depth + 1,
+                        start=start,
+                    ):
                         concrete_pairs.update(new_concrete_pairs)
                         return True
             return False
@@ -1290,7 +1301,9 @@ def match(state, func, symbolic_pairs, concrete_pairs, depth=0, start=None):
                 # symbolic_pairs = graph_sort(state, symbolic_pairs)
                 known_pairs = ethereum_context.get(f"symbolic_func_conc_{table}", set())
                 new_known_pairs = set(known_pairs)
-                if not match(state, functions[table], symbolic_pairs, new_known_pairs, start=time.time()):
+                if not match(
+                    state, functions[table], symbolic_pairs, new_known_pairs, start=time.time()
+                ):
                     ethereum_context["soundcheck"] = False
                     return False
 
diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index 4c58a2603..0aaa6e3ba 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -1213,7 +1213,7 @@ def setstate(state, value):
             raise Concretize(
                 "Concretize PC", expression=expression, setstate=setstate, policy="ALL"
             )
-        #print(self)
+        # print(self)
         try:
             # import time
             # limbo = 0.0

From 401e06ce9ac55a5aa3b4459572ad4c1d4a2819e5 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Tue, 24 Sep 2019 10:23:05 -0300
Subject: [PATCH 13/37] Review fixes

---
 manticore/core/smtlib/solver.py   |  1 -
 manticore/core/smtlib/visitors.py | 42 +++++++++++++++----------------
 manticore/ethereum/manticore.py   |  7 ++++--
 manticore/platforms/evm.py        | 19 ++++++--------
 manticore/utils/event.py          |  9 +------
 5 files changed, 34 insertions(+), 44 deletions(-)

diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py
index bb77960c1..bed3954ab 100644
--- a/manticore/core/smtlib/solver.py
+++ b/manticore/core/smtlib/solver.py
@@ -449,7 +449,6 @@ def get_all_values(self, constraints, expression, maxcnt=None, silent=False):
                         # of returned vals list (previous smtlib behavior)
                         break
                     else:
-                        print(result)
                         raise TooManySolutions(result)
                 if time.time() - start > consts.timeout:
                     raise SolverError("Timeout")
diff --git a/manticore/core/smtlib/visitors.py b/manticore/core/smtlib/visitors.py
index d7579c32f..a629b718b 100644
--- a/manticore/core/smtlib/visitors.py
+++ b/manticore/core/smtlib/visitors.py
@@ -400,35 +400,35 @@ def visit_BoolAnd(self, expression, *operands):
             expression.operands[1], BoolEqual
         ):
             # Eq operands
-            operanda = expression.operands[0]
-            operandb = expression.operands[1]
+            operand_0 = expression.operands[0]
+            operand_1 = expression.operands[1]
             # Extract operands
-            operandaa = operanda.operands[0]
-            operandab = operanda.operands[1]
-            operandba = operandb.operands[0]
-            operandbb = operandb.operands[1]
+            operand_0_0 = operand_0.operands[0]
+            operand_0_1 = operand_0.operands[1]
+            operand_1_0 = operand_1.operands[0]
+            operand_1_1 = operand_1.operands[1]
 
             if (
-                isinstance(operandaa, BitVecExtract)
-                and isinstance(operandab, BitVecExtract)
-                and isinstance(operandba, BitVecExtract)
-                and isinstance(operandbb, BitVecExtract)
+                isinstance(operand_0_0, BitVecExtract)
+                and isinstance(operand_0_1, BitVecExtract)
+                and isinstance(operand_1_0, BitVecExtract)
+                and isinstance(operand_1_1, BitVecExtract)
             ):
 
                 if (
-                    operandaa.value is operandba.value
-                    and operandab.value is operandbb.value
-                    and (operandaa.begining, operandaa.end) == (operandab.begining, operandab.end)
-                    and (operandba.begining, operandba.end) == (operandbb.begining, operandbb.end)
+                    operand_0_0.value is operand_1_0.value
+                    and operand_0_1.value is operand_1_1.value
+                    and (operand_0_0.begining, operand_0_0.end) == (operand_0_1.begining, operand_0_1.end)
+                    and (operand_1_0.begining, operand_1_0.end) == (operand_1_1.begining, operand_1_1.end)
                 ):
-                    if ((operandaa.end + 1) == operandba.begining) or (
-                        operandaa.begining == (operandba.end + 1)
+                    if ((operand_0_0.end + 1) == operand_1_0.begining) or (
+                        operand_0_0.begining == (operand_1_0.end + 1)
                     ):
 
-                        value0 = operandaa.value  # := operandba.value
-                        value1 = operandab.value  # := operandbb.value
-                        beg = min(operandaa.begining, operandba.begining)
-                        end = max(operandaa.end, operandba.end)
+                        value0 = operand_0_0.value
+                        value1 = operand_0_1.value
+                        beg = min(operand_0_0.begining, operand_1_0.begining)
+                        end = max(operand_0_0.end, operand_1_0.end)
                         return BitVecExtract(value0, beg, end - beg + 1) == BitVecExtract(
                             value1, beg, end - beg + 1
                         )
@@ -454,7 +454,7 @@ def visit_BoolEqual(self, expression, *operands):
                     expression.operands[0].operands[2].value,
                 )
                 if value1 == value2 and value1 != value3:
-                    return expression.operands[0].operands[0]  # FIXME:taint
+                    return expression.operands[0].operands[0]  # FIXME: this may break taint propagation
                 elif value1 == value3 and value1 != value2:
                     return BoolNot(expression.operands[0].operands[0], taint=expression.taint)
 
diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index 25cb24f46..a37bdb2e9 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -1608,14 +1608,17 @@ def _emit_trace_file(filestream, trace):
             filestream.write(ln)
 
     @ManticoreBase.at_not_running
-    def finalize(self, procs=45):
+    def finalize(self, procs=None):
         """
         Terminate and generate testcases for all currently alive states (contract
         states that cleanly executed to a STOP or RETURN in the last symbolic
         transaction).
 
-        :param procs: nomber of local processes to use in the reporting generation
+        :param procs: force the number of local processes to use in the reporting
+        generation. Uses global configuration constant by default
         """
+        if procs is None:
+            procs = config.get_group("core").procs
 
         logger.debug("Finalizing %d states.", self.count_states())
 
diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index 0aaa6e3ba..c805a85a0 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -2220,7 +2220,8 @@ class EVMWorld(Platform):
         "evm_read_storage",
         "evm_write_storage",
         "evm_read_code",
-        "evm_write_code" "decode_instruction",
+        "evm_write_code",
+        "decode_instruction",
         "execute_instruction",
         "open_transaction",
         "close_transaction",
@@ -3058,20 +3059,14 @@ def dump(self, stream, state, mevm, message):
 
             all_used_indexes = []
             with state.constraints as temp_cs:
+                # make a free symbolic idex that could address any storage slot
                 index = temp_cs.new_bitvec(256)
+                #get the storage for accounbt_address
                 storage = blockchain.get_storage(account_address)
+                #we are interested only in used slots
                 temp_cs.add(storage.get(index) != 0)
-
-                try:
-                    # FIXME do this only if it has symbolic writes?
-                    while True:
-                        a_index = Z3Solver.instance().get_value(temp_cs, index)
-                        all_used_indexes.append(a_index)
-
-                        temp_cs.add(storage.get(a_index) != 0)
-                        temp_cs.add(index != a_index)
-                except Exception:
-                    pass
+                #Query the solver to get all storage indexes with used slots
+                all_used_indexes = Z3Solver.instance().get_all_values(temp_cs, index)
 
             if all_used_indexes:
                 stream.write("Storage:\n")
diff --git a/manticore/utils/event.py b/manticore/utils/event.py
index 5a5d75440..d3374a96e 100644
--- a/manticore/utils/event.py
+++ b/manticore/utils/event.py
@@ -150,14 +150,7 @@ def _publish_impl(self, _name, *args, **kwargs):
         bucket = self._get_signal_bucket(_name)
         for robj, methods in bucket.items():
             for callback in methods:
-                try:
-                    callback(robj(), *args, **kwargs)
-                except Exception as e:
-                    import traceback
-
-                    # traceback.print_stack()
-                    traceback.print_last()
-                    print("Exception", e, callback)
+                callback(robj(), *args, **kwargs)
 
         # The include_source flag indicates to prepend the source of the event in
         # the callback signature. This is set on forward_events_from/to

From 31aa8ebb56e6c8206a6f16a8bfdf0b849b12e476 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Tue, 24 Sep 2019 10:23:27 -0300
Subject: [PATCH 14/37] black

---
 manticore/core/smtlib/visitors.py | 10 +++++++---
 manticore/platforms/evm.py        |  6 +++---
 2 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/manticore/core/smtlib/visitors.py b/manticore/core/smtlib/visitors.py
index a629b718b..8b74845ad 100644
--- a/manticore/core/smtlib/visitors.py
+++ b/manticore/core/smtlib/visitors.py
@@ -418,8 +418,10 @@ def visit_BoolAnd(self, expression, *operands):
                 if (
                     operand_0_0.value is operand_1_0.value
                     and operand_0_1.value is operand_1_1.value
-                    and (operand_0_0.begining, operand_0_0.end) == (operand_0_1.begining, operand_0_1.end)
-                    and (operand_1_0.begining, operand_1_0.end) == (operand_1_1.begining, operand_1_1.end)
+                    and (operand_0_0.begining, operand_0_0.end)
+                    == (operand_0_1.begining, operand_0_1.end)
+                    and (operand_1_0.begining, operand_1_0.end)
+                    == (operand_1_1.begining, operand_1_1.end)
                 ):
                     if ((operand_0_0.end + 1) == operand_1_0.begining) or (
                         operand_0_0.begining == (operand_1_0.end + 1)
@@ -454,7 +456,9 @@ def visit_BoolEqual(self, expression, *operands):
                     expression.operands[0].operands[2].value,
                 )
                 if value1 == value2 and value1 != value3:
-                    return expression.operands[0].operands[0]  # FIXME: this may break taint propagation
+                    return expression.operands[0].operands[
+                        0
+                    ]  # FIXME: this may break taint propagation
                 elif value1 == value3 and value1 != value2:
                     return BoolNot(expression.operands[0].operands[0], taint=expression.taint)
 
diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index c805a85a0..879a9afa9 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -3061,11 +3061,11 @@ def dump(self, stream, state, mevm, message):
             with state.constraints as temp_cs:
                 # make a free symbolic idex that could address any storage slot
                 index = temp_cs.new_bitvec(256)
-                #get the storage for accounbt_address
+                # get the storage for accounbt_address
                 storage = blockchain.get_storage(account_address)
-                #we are interested only in used slots
+                # we are interested only in used slots
                 temp_cs.add(storage.get(index) != 0)
-                #Query the solver to get all storage indexes with used slots
+                # Query the solver to get all storage indexes with used slots
                 all_used_indexes = Z3Solver.instance().get_all_values(temp_cs, index)
 
             if all_used_indexes:

From a958d718ce1f89cc367b0618d3e0345c683098e1 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Tue, 24 Sep 2019 11:00:19 -0300
Subject: [PATCH 15/37] Fix KeepOnlyIfStorageChanges test

---
 manticore/ethereum/manticore.py            | 2 +-
 tests/ethereum/test_consensys_benchmark.py | 1 +
 tests/ethereum/test_plugins.py             | 2 +-
 3 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index a37bdb2e9..b4f57760c 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -1432,7 +1432,7 @@ def global_findings(self):
         try:
             return self._global_findings
         except AttributeError:
-            return set()
+            raise Exception("You need to call finalize() first")
 
     def current_location(self, state):
         world = state.platform
diff --git a/tests/ethereum/test_consensys_benchmark.py b/tests/ethereum/test_consensys_benchmark.py
index 7bcac10c1..60466c5a3 100644
--- a/tests/ethereum/test_consensys_benchmark.py
+++ b/tests/ethereum/test_consensys_benchmark.py
@@ -20,6 +20,7 @@ class EthBenchmark(unittest.TestCase):
 
     def setUp(self):
         self.mevm = ManticoreEVM()
+        self.mevm.register_plugin(KeepOnlyIfStorageChanges())
         log.set_verbosity(0)
         self.worksp = self.mevm.workspace
 
diff --git a/tests/ethereum/test_plugins.py b/tests/ethereum/test_plugins.py
index 7d1de8222..ad9e10f06 100644
--- a/tests/ethereum/test_plugins.py
+++ b/tests/ethereum/test_plugins.py
@@ -31,7 +31,7 @@ def test_ignore_states(self):
         for st in m.all_states:
             if st.platform.logs:
                 return
-        self.assertEqual(0, 1)
+        self.fail("We did not reach any state with logs")
 
     @unittest.skip("failing")
     def test_verbose_trace(self):

From d0099cdd19b769ab0dfd8d8c1f18f6db49387b64 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Tue, 24 Sep 2019 15:10:00 -0300
Subject: [PATCH 16/37] remove dead code

---
 manticore/ethereum/manticore.py | 13 +------------
 1 file changed, 1 insertion(+), 12 deletions(-)

diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index b4f57760c..74ba76f68 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -64,7 +64,7 @@ def from_string(cls, name):
 consts.add(
     "sha3",
     default=Sha3Type.concretize,
-    description="concretize(*): sound simple concretization\nsymbolicate: unsound symbolication with gout of cycle FP killing",
+    description="concretize(*): sound simple concretization\nsymbolicate: unsound symbolication with out of cycle false positive killing",
 )
 consts.add(
     "sha3timeout",
@@ -1316,17 +1316,6 @@ def match(state, func, symbolic_pairs, concrete_pairs, depth=0, start=None):
             state.context["soundcheck"] = state.can_be_true(True)
         return state.context["soundcheck"]
 
-    def concretize_unsound_symbolication(self):
-        self._on_did_run_unsound_symbolication()
-
-    def _on_did_run_unsound_symbolication(self):
-        # Called at the end of a run(). Need to filter out the unreproducible/
-        # unfeasible states
-        # Caveat: It will add redundant constraints from previous run()
-        for state in self.all_states:
-            if not self.fix_unsound_symbolication(state):
-                self.kill_state(state)
-
     def _terminate_state_callback(self, state, e):
         """ INTERNAL USE
             Every time a state finishes executing the last transaction, we save it in

From 0b0c193408d194cae0155ac93ec07f327d3690f6 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Thu, 26 Sep 2019 12:38:09 -0300
Subject: [PATCH 17/37] cleanups

---
 manticore/ethereum/manticore.py | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index 74ba76f68..298e47a63 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -1227,7 +1227,7 @@ def concretize_known_pairs(state, symbolic_pairs, known_pairs):
                 if cond is False:
                     return
 
-        def match(state, func, symbolic_pairs, concrete_pairs, depth=0, start=None):
+        def match(state, func, symbolic_pairs, concrete_pairs, start=None):
             """ Tries to find a concrete match for the symbolic pairs. It uses
             concrete_pairs (and potentially extends it with solved pairs) until
             a matching set of concrete pairs is found, or fail.
@@ -1235,7 +1235,8 @@ def match(state, func, symbolic_pairs, concrete_pairs, depth=0, start=None):
             state: the current state
             func: the relation between domain and range in symbolic_pairs/concrete_pairs
             symbolic_pairs: related symbolic values that need a set of solutions
-            concrete_pairs: Known of concrete pairs that may match some of the symbolic pairs
+            concrete_pairs: known of concrete pairs that may match some of the symbolic pairs
+
 
             """
             if time.time() - start > consts.sha3timeout:
@@ -1260,18 +1261,22 @@ def match(state, func, symbolic_pairs, concrete_pairs, depth=0, start=None):
                         unseen = Operators.AND(
                             Operators.AND(x != x_concrete, y != y_concrete), unseen
                         )
-
+                #Search for a new unseen sha3 pair
                 with state as temp_state:
                     temp_state.constrain(unseen)
                     new_x_concretes = temp_state.solve_n(x, nsolves=1)
                     new_y_concretes = map(func, new_x_concretes)
                     new_concrete_pairs.update(zip(new_x_concretes, new_y_concretes))
 
+                #Consider all the new set of sha3 pairs and rebuild the seen condition
                 seen = False
                 for x_concrete, y_concrete in new_concrete_pairs:
                     if len(x) == len(x_concrete):  # If the size of the buffer wont
                         # match it does not matter
                         seen = Operators.OR(Operators.AND(x == x_concrete, y == y_concrete), seen)
+
+                # With the current x,y pair being one of the known sha3 pairs try
+                # to match the following symbolic pairs
                 with state as temp_state:
                     temp_state.constrain(seen)
                     if match(
@@ -1279,7 +1284,6 @@ def match(state, func, symbolic_pairs, concrete_pairs, depth=0, start=None):
                         func,
                         new_symbolic_pairs,
                         new_concrete_pairs,
-                        depth + 1,
                         start=start,
                     ):
                         concrete_pairs.update(new_concrete_pairs)

From f7d94f384fd02ce66750abe0f20fcde6c3e405fb Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Fri, 27 Sep 2019 15:59:11 -0300
Subject: [PATCH 18/37] remove unused code

---
 manticore/core/smtlib/solver.py | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py
index bed3954ab..fc636382d 100644
--- a/manticore/core/smtlib/solver.py
+++ b/manticore/core/smtlib/solver.py
@@ -20,14 +20,12 @@
 import time
 from subprocess import PIPE, Popen
 import re
-
 from . import operators as Operators
 from .constraints import *
 from .visitors import *
 from ...exceptions import Z3NotFoundError, SolverError, SolverUnknown, TooManySolutions
 from ...utils import config
 from . import issymbolic
-import time
 
 logger = logging.getLogger(__name__)
 consts = config.get_group("smt")
@@ -429,8 +427,6 @@ def get_all_values(self, constraints, expression, maxcnt=None, silent=False):
                     f"get_all_values only implemented for {type(expression)} expression type."
                 )
 
-            from manticore.core.smtlib import translate_to_smtlib
-
             temp_cs.add(var == expression)
             self._reset(temp_cs.to_string(related_to=var))
             result = []

From 4098ee5d4ccb529e20f2650552b6b9dd23469643 Mon Sep 17 00:00:00 2001
From: Eric Hennenfent <eric.hennenfent@trailofbits.com>
Date: Tue, 1 Oct 2019 07:57:00 -0700
Subject: [PATCH 19/37] Blacken

---
 manticore/ethereum/manticore.py | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index 298e47a63..3007cb2d9 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -1261,14 +1261,14 @@ def match(state, func, symbolic_pairs, concrete_pairs, start=None):
                         unseen = Operators.AND(
                             Operators.AND(x != x_concrete, y != y_concrete), unseen
                         )
-                #Search for a new unseen sha3 pair
+                # Search for a new unseen sha3 pair
                 with state as temp_state:
                     temp_state.constrain(unseen)
                     new_x_concretes = temp_state.solve_n(x, nsolves=1)
                     new_y_concretes = map(func, new_x_concretes)
                     new_concrete_pairs.update(zip(new_x_concretes, new_y_concretes))
 
-                #Consider all the new set of sha3 pairs and rebuild the seen condition
+                # Consider all the new set of sha3 pairs and rebuild the seen condition
                 seen = False
                 for x_concrete, y_concrete in new_concrete_pairs:
                     if len(x) == len(x_concrete):  # If the size of the buffer wont
@@ -1279,13 +1279,7 @@ def match(state, func, symbolic_pairs, concrete_pairs, start=None):
                 # to match the following symbolic pairs
                 with state as temp_state:
                     temp_state.constrain(seen)
-                    if match(
-                        temp_state,
-                        func,
-                        new_symbolic_pairs,
-                        new_concrete_pairs,
-                        start=start,
-                    ):
+                    if match(temp_state, func, new_symbolic_pairs, new_concrete_pairs, start=start):
                         concrete_pairs.update(new_concrete_pairs)
                         return True
             return False

From 270102c98d120843c07198e5932761d48ce845d8 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Tue, 1 Oct 2019 14:44:35 -0300
Subject: [PATCH 20/37] Better concretize and calldataload

---
 manticore/core/smtlib/visitors.py |  2 +-
 manticore/ethereum/abi.py         |  1 +
 manticore/ethereum/detectors.py   |  1 -
 manticore/ethereum/manticore.py   |  3 ++
 manticore/platforms/evm.py        | 66 ++++++++++++++++++-------------
 5 files changed, 43 insertions(+), 30 deletions(-)

diff --git a/manticore/core/smtlib/visitors.py b/manticore/core/smtlib/visitors.py
index 8b74845ad..19851da39 100644
--- a/manticore/core/smtlib/visitors.py
+++ b/manticore/core/smtlib/visitors.py
@@ -786,7 +786,7 @@ def to_constant(expression):
 
 @lru_cache(maxsize=128, typed=True)
 def simplify(expression):
-    # expression = constant_folder(expression)
+    expression = constant_folder(expression)
     expression = arithmetic_simplify(expression)
     return expression
 
diff --git a/manticore/ethereum/abi.py b/manticore/ethereum/abi.py
index 0c6aff913..ed3cdc47d 100644
--- a/manticore/ethereum/abi.py
+++ b/manticore/ethereum/abi.py
@@ -253,6 +253,7 @@ def _deserialize(ty, buf, offset=0):
         elif ty[0] in ("array"):
             result = []
             dyn_offset = ABI._deserialize_int(buf[offset : offset + 32])
+            dyn_offset = to_constant(dyn_offset)
             rep = ty[1]
             ty_size = ABI._type_size(ty[2])
             if rep is None:
diff --git a/manticore/ethereum/detectors.py b/manticore/ethereum/detectors.py
index fc5f27cc3..4dbf9067e 100644
--- a/manticore/ethereum/detectors.py
+++ b/manticore/ethereum/detectors.py
@@ -75,7 +75,6 @@ def add_finding(self, state, address, pc, finding, at_init, constraint=True):
         self.get_findings(state).append((address, pc, finding, at_init, constraint))
         with self.locked_global_findings() as gf:
             gf.append((address, pc, finding, at_init))
-
         # Fixme for ever broken logger
         logger.warning(finding)
 
diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index 298e47a63..2d96ff27b 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -1502,6 +1502,9 @@ def generate_testcase(self, state, message="", only_if=None, name="user"):
         if len(local_findings):
             with testcase.open_stream("findings") as findings:
                 for address, pc, finding, at_init, constraint in local_findings:
+                    if not state.can_be_true(constraint):
+                        continue
+                    state.constrain(constraint)
                     findings.write("- %s -\n" % finding)
                     write_findings(findings, "  ", address, pc, at_init)
                     md = self.get_metadata(address)
diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index 879a9afa9..35b989aa5 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -78,6 +78,11 @@ def globalsha3(data):
     default=1024 * 1024,
     description="Max calldata offset to explore with. Iff offset or size in a calldata related instruction are symbolic it will be constrained to this constant",
 )
+consts.add(
+    "calldata_max_size",
+    default = 64,
+    description="Max calldata size to explore in each CALLDATACOPY. Iff size in a calldata related instruction are symbolic it will be constrained to be less than this constant. -1 means free(only use when gas is being tracked)",
+)
 
 # Auxiliary constants and functions
 TT256 = 2 ** 256
@@ -142,14 +147,17 @@ def __init__(
         self.gas = gas
         self.set_result(result, return_data)
 
-    def concretize(self, state):
-        conc_caller = state.solve_one(self.caller)
-        conc_address = state.solve_one(self.address)
-        conc_value = state.solve_one(self.value)
-        conc_gas = state.solve_one(self.gas)
-        conc_data = state.solve_one(self.data)
-        conc_return_data = state.solve_one(self.return_data)
-
+    def concretize(self, state, constrain=False):
+        """
+        :param state: a manticore state
+        :param bool constrain: If True, constrain expr to concretized value
+        """
+        conc_caller = state.solve_one(self.caller, constrain=constrain)
+        conc_address = state.solve_one(self.address, constrain=constrain)
+        conc_value = state.solve_one(self.value, constrain=constrain)
+        conc_gas = state.solve_one(self.gas, constrain=constrain)
+        conc_data = state.solve_one(self.data, constrain=constrain)
+        conc_return_data = state.solve_one(self.return_data, constrain=constrain)
         return Transaction(
             self.sort,
             conc_address,
@@ -160,7 +168,7 @@ def concretize(self, state):
             conc_gas,
             depth=self.depth,
             result=self.result,
-            return_data=bytearray(conc_return_data),
+            return_data=conc_return_data,
         )
 
     def to_dict(self, mevm):
@@ -556,8 +564,8 @@ def wrapper(*args, **kwargs):
                         "the value might not be tracked properly (This may affect detectors)"
                     )
                 logger.info(
-                    f"Concretizing instruction {args[0].world.current_vm.instruction} argument {arg} by {policy}"
-                )
+                    f"Concretizing instruction {args[0].world.current_vm.instruction} argument {arg} by {policy}")
+
                 raise ConcretizeArgument(index, policy=policy)
             return func(*args, **kwargs)
 
@@ -834,7 +842,7 @@ def _get_memfee(self, address, size=1):
         return Operators.ITEBV(512, size == 0, 0, Operators.ITEBV(512, flag, memfee, 0))
 
     def _allocate(self, address, size=1):
-        address_c = Operators.UDIV(Operators.ZEXTEND(address, 512) + size + 31, 32) * 32
+        address_c = Operators.UDIV(self.safe_add(address, size, 31), 32) * 32
         self._allocated = Operators.ITEBV(
             512, Operators.UGT(address_c, self._allocated), address_c, self.allocated
         )
@@ -1213,7 +1221,11 @@ def setstate(state, value):
             raise Concretize(
                 "Concretize PC", expression=expression, setstate=setstate, policy="ALL"
             )
-        # print(self)
+        #if self._checkpoint_data is None:
+        #    print(self)
+        #else:
+        #    print ("back from a fork")
+        #import pdb; pdb.set_trace()
         try:
             # import time
             # limbo = 0.0
@@ -1334,10 +1346,12 @@ def _store(self, offset, value, size=1):
                 "did_evm_write_memory", offset + i, Operators.EXTRACT(value, (size - i - 1) * 8, 8)
             )
 
-    def safe_add(self, a, b):
+    def safe_add(self, a, b, *args):
         a = Operators.ZEXTEND(a, 512)
         b = Operators.ZEXTEND(b, 512)
         result = a + b
+        if len(args) > 0:
+            result = self.safe_add(result, *args)
         return result
 
     def safe_mul(self, a, b):
@@ -1597,14 +1611,10 @@ def CALLVALUE(self):
     def CALLDATALOAD(self, offset):
         """Get input data of current environment"""
         # calldata_overflow = const.calldata_overflow
-        # calldata_underflow = const.calldata_underflow
         calldata_overflow = None  # 32
-        calldata_underflow = None  # 32
-        # if const.calldata_overlap:
         if calldata_overflow is not None:
-            self.constraints.add(offset + 32 <= len(self.data) + calldata_overflow)
+            self.constraints.add(self.safe_add(offset, 32) <= len(self.data) + calldata_overflow)
         if calldata_underflow is not None:
-            self.constraints.add(offset >= -calldata_underflow)
 
         self._use_calldata(offset, 32)
 
@@ -1612,7 +1622,7 @@ def CALLDATALOAD(self, offset):
         bytes = []
         for i in range(32):
             try:
-                c = simplify(Operators.ITEBV(8, offset + i < data_length, self.data[offset + i], 0))
+                c = simplify(Operators.ITEBV(8, Operators.ULT(self.safe_add(offset, i), data_length), self.data[offset + i], 0))
             except IndexError:
                 # offset + i is concrete and outside data
                 c = 0
@@ -1636,17 +1646,14 @@ def CALLDATACOPY_gas(self, mem_offset, data_offset, size):
         memfee = self._get_memfee(mem_offset, size)
         return self.safe_add(copyfee, memfee)
 
-    @concretized_args(size="SAMPLED")
+    #@concretized_args(size="SAMPLED")
     def CALLDATACOPY(self, mem_offset, data_offset, size):
         """Copy input data in current environment to memory"""
         # calldata_overflow = const.calldata_overflow
         # calldata_underflow = const.calldata_underflow
         calldata_overflow = None  # 32
-        calldata_underflow = None  # 32
-        # if const.calldata_overlap:
-        if calldata_underflow is not None:
-            self.constraints.add(data_offset + size <= len(self.data) + calldata_overflow)
-            self.constraints.add(data_offset >= -calldata_underflow)
+        if calldata_overflow is not None:
+            self.constraints.add(Operators.ULT( self.safe_add(data_offset, size), len(self.data) + calldata_overflow))
 
         self._use_calldata(data_offset, size)
         self._allocate(mem_offset, size)
@@ -1658,6 +1665,9 @@ def CALLDATACOPY(self, mem_offset, data_offset, size):
                 raise NotEnoughGas()
             self.constraints.add(cond)
 
+        if consts.calldata_max_size >= 0:
+            self.constraints.add(Operators.ULE(size, consts.calldata_max_size))
+
         max_size = size
         if issymbolic(max_size):
             max_size = Z3Solver.instance().max(self.constraints, size)
@@ -1677,7 +1687,7 @@ def CALLDATACOPY(self, mem_offset, data_offset, size):
             try:
                 c1 = Operators.ITEBV(
                     8,
-                    data_offset + i < len(self.data),
+                    Operators.ULT(self.safe_add(data_offset, i), len(self.data)),
                     Operators.ORD(self.data[data_offset + i]),
                     0,
                 )
@@ -2202,7 +2212,7 @@ def __str__(self):
         gas = self.gas
         if issymbolic(gas):
             gas = simplify(gas)
-            result.append(f"Gas: {translate_to_smtlib(gas)} {gas.taint}")
+            result.append(f"Gas: {translate_to_smtlib(gas)[:20]} {gas.taint}")
         else:
             result.append(f"Gas: {gas}")
 

From 04710865d9c6bfb8bd5e596b5d2669b70c9ac303 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Tue, 1 Oct 2019 14:45:48 -0300
Subject: [PATCH 21/37] black

---
 manticore/platforms/evm.py | 1 -
 1 file changed, 1 deletion(-)

diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index 35b989aa5..41742382c 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -1614,7 +1614,6 @@ def CALLDATALOAD(self, offset):
         calldata_overflow = None  # 32
         if calldata_overflow is not None:
             self.constraints.add(self.safe_add(offset, 32) <= len(self.data) + calldata_overflow)
-        if calldata_underflow is not None:
 
         self._use_calldata(offset, 32)
 

From 1de2fbd5dd22ff348afedc652e12c49b2f3f4170 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Tue, 1 Oct 2019 15:56:06 -0300
Subject: [PATCH 22/37] blkn

---
 manticore/platforms/evm.py | 26 ++++++++++++++++++--------
 1 file changed, 18 insertions(+), 8 deletions(-)

diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index 41742382c..4d7a5e417 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -80,7 +80,7 @@ def globalsha3(data):
 )
 consts.add(
     "calldata_max_size",
-    default = 64,
+    default=64,
     description="Max calldata size to explore in each CALLDATACOPY. Iff size in a calldata related instruction are symbolic it will be constrained to be less than this constant. -1 means free(only use when gas is being tracked)",
 )
 
@@ -564,7 +564,8 @@ def wrapper(*args, **kwargs):
                         "the value might not be tracked properly (This may affect detectors)"
                     )
                 logger.info(
-                    f"Concretizing instruction {args[0].world.current_vm.instruction} argument {arg} by {policy}")
+                    f"Concretizing instruction {args[0].world.current_vm.instruction} argument {arg} by {policy}"
+                )
 
                 raise ConcretizeArgument(index, policy=policy)
             return func(*args, **kwargs)
@@ -1221,11 +1222,11 @@ def setstate(state, value):
             raise Concretize(
                 "Concretize PC", expression=expression, setstate=setstate, policy="ALL"
             )
-        #if self._checkpoint_data is None:
+        # if self._checkpoint_data is None:
         #    print(self)
-        #else:
+        # else:
         #    print ("back from a fork")
-        #import pdb; pdb.set_trace()
+        # import pdb; pdb.set_trace()
         try:
             # import time
             # limbo = 0.0
@@ -1621,7 +1622,14 @@ def CALLDATALOAD(self, offset):
         bytes = []
         for i in range(32):
             try:
-                c = simplify(Operators.ITEBV(8, Operators.ULT(self.safe_add(offset, i), data_length), self.data[offset + i], 0))
+                c = simplify(
+                    Operators.ITEBV(
+                        8,
+                        Operators.ULT(self.safe_add(offset, i), data_length),
+                        self.data[offset + i],
+                        0,
+                    )
+                )
             except IndexError:
                 # offset + i is concrete and outside data
                 c = 0
@@ -1645,14 +1653,16 @@ def CALLDATACOPY_gas(self, mem_offset, data_offset, size):
         memfee = self._get_memfee(mem_offset, size)
         return self.safe_add(copyfee, memfee)
 
-    #@concretized_args(size="SAMPLED")
+    # @concretized_args(size="SAMPLED")
     def CALLDATACOPY(self, mem_offset, data_offset, size):
         """Copy input data in current environment to memory"""
         # calldata_overflow = const.calldata_overflow
         # calldata_underflow = const.calldata_underflow
         calldata_overflow = None  # 32
         if calldata_overflow is not None:
-            self.constraints.add(Operators.ULT( self.safe_add(data_offset, size), len(self.data) + calldata_overflow))
+            self.constraints.add(
+                Operators.ULT(self.safe_add(data_offset, size), len(self.data) + calldata_overflow)
+            )
 
         self._use_calldata(data_offset, size)
         self._allocate(mem_offset, size)

From 31f79c4032921d4b7e8c6a22706549120d9e02b1 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Wed, 2 Oct 2019 10:49:10 -0300
Subject: [PATCH 23/37] mulmod fix

---
 manticore/platforms/evm.py | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index 4d7a5e417..1a77d6f92 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -1434,7 +1434,8 @@ def SMOD(self, a, b):
     def ADDMOD(self, a, b, c):
         """Modulo addition operation"""
         try:
-            result = Operators.ITEBV(256, c == 0, 0, (a + b) % c)
+            result = Operators.EXTRACT(self.safe_add(a, b) % Operators.ZEXTEND(c, 512),0, 256)
+            result = Operators.ITEBV(256, c == 0, 0, result)
         except ZeroDivisionError:
             result = 0
         return result
@@ -1442,7 +1443,8 @@ def ADDMOD(self, a, b, c):
     def MULMOD(self, a, b, c):
         """Modulo addition operation"""
         try:
-            result = Operators.ITEBV(256, c == 0, 0, (a * b) % c)
+            result = Operators.EXTRACT(self.safe_mul(a, b) % Operators.ZEXTEND(c, 512),0, 256)
+            result = Operators.ITEBV(256, c == 0, 0, result)
         except ZeroDivisionError:
             result = 0
         return result

From b11bd928c0ddb4cc98a00ebfcdd6c18daffc4a1e Mon Sep 17 00:00:00 2001
From: Eric Hennenfent <eric.hennenfent@trailofbits.com>
Date: Wed, 2 Oct 2019 08:11:23 -0700
Subject: [PATCH 24/37] Blacken

---
 manticore/platforms/evm.py | 26 ++++++++++++++++++--------
 1 file changed, 18 insertions(+), 8 deletions(-)

diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index 41742382c..4d7a5e417 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -80,7 +80,7 @@ def globalsha3(data):
 )
 consts.add(
     "calldata_max_size",
-    default = 64,
+    default=64,
     description="Max calldata size to explore in each CALLDATACOPY. Iff size in a calldata related instruction are symbolic it will be constrained to be less than this constant. -1 means free(only use when gas is being tracked)",
 )
 
@@ -564,7 +564,8 @@ def wrapper(*args, **kwargs):
                         "the value might not be tracked properly (This may affect detectors)"
                     )
                 logger.info(
-                    f"Concretizing instruction {args[0].world.current_vm.instruction} argument {arg} by {policy}")
+                    f"Concretizing instruction {args[0].world.current_vm.instruction} argument {arg} by {policy}"
+                )
 
                 raise ConcretizeArgument(index, policy=policy)
             return func(*args, **kwargs)
@@ -1221,11 +1222,11 @@ def setstate(state, value):
             raise Concretize(
                 "Concretize PC", expression=expression, setstate=setstate, policy="ALL"
             )
-        #if self._checkpoint_data is None:
+        # if self._checkpoint_data is None:
         #    print(self)
-        #else:
+        # else:
         #    print ("back from a fork")
-        #import pdb; pdb.set_trace()
+        # import pdb; pdb.set_trace()
         try:
             # import time
             # limbo = 0.0
@@ -1621,7 +1622,14 @@ def CALLDATALOAD(self, offset):
         bytes = []
         for i in range(32):
             try:
-                c = simplify(Operators.ITEBV(8, Operators.ULT(self.safe_add(offset, i), data_length), self.data[offset + i], 0))
+                c = simplify(
+                    Operators.ITEBV(
+                        8,
+                        Operators.ULT(self.safe_add(offset, i), data_length),
+                        self.data[offset + i],
+                        0,
+                    )
+                )
             except IndexError:
                 # offset + i is concrete and outside data
                 c = 0
@@ -1645,14 +1653,16 @@ def CALLDATACOPY_gas(self, mem_offset, data_offset, size):
         memfee = self._get_memfee(mem_offset, size)
         return self.safe_add(copyfee, memfee)
 
-    #@concretized_args(size="SAMPLED")
+    # @concretized_args(size="SAMPLED")
     def CALLDATACOPY(self, mem_offset, data_offset, size):
         """Copy input data in current environment to memory"""
         # calldata_overflow = const.calldata_overflow
         # calldata_underflow = const.calldata_underflow
         calldata_overflow = None  # 32
         if calldata_overflow is not None:
-            self.constraints.add(Operators.ULT( self.safe_add(data_offset, size), len(self.data) + calldata_overflow))
+            self.constraints.add(
+                Operators.ULT(self.safe_add(data_offset, size), len(self.data) + calldata_overflow)
+            )
 
         self._use_calldata(data_offset, size)
         self._allocate(mem_offset, size)

From 5ec8afc3c152c8e9ed19146d297411f5be2b574e Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Wed, 2 Oct 2019 23:53:01 -0300
Subject: [PATCH 25/37] fix calldata rel tests

---
 manticore/platforms/evm.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index 1a77d6f92..a63bf27d6 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -80,7 +80,7 @@ def globalsha3(data):
 )
 consts.add(
     "calldata_max_size",
-    default=64,
+    default=-1,
     description="Max calldata size to explore in each CALLDATACOPY. Iff size in a calldata related instruction are symbolic it will be constrained to be less than this constant. -1 means free(only use when gas is being tracked)",
 )
 
@@ -1223,7 +1223,7 @@ def setstate(state, value):
                 "Concretize PC", expression=expression, setstate=setstate, policy="ALL"
             )
         # if self._checkpoint_data is None:
-        #    print(self)
+        #   print(self)
         # else:
         #    print ("back from a fork")
         # import pdb; pdb.set_trace()

From 632221cf2cf8f41e587ee16f3b9a72dd229599f5 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Wed, 2 Oct 2019 23:53:18 -0300
Subject: [PATCH 26/37] blk

---
 manticore/platforms/evm.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index a63bf27d6..ba807cec5 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -1434,7 +1434,7 @@ def SMOD(self, a, b):
     def ADDMOD(self, a, b, c):
         """Modulo addition operation"""
         try:
-            result = Operators.EXTRACT(self.safe_add(a, b) % Operators.ZEXTEND(c, 512),0, 256)
+            result = Operators.EXTRACT(self.safe_add(a, b) % Operators.ZEXTEND(c, 512), 0, 256)
             result = Operators.ITEBV(256, c == 0, 0, result)
         except ZeroDivisionError:
             result = 0
@@ -1443,7 +1443,7 @@ def ADDMOD(self, a, b, c):
     def MULMOD(self, a, b, c):
         """Modulo addition operation"""
         try:
-            result = Operators.EXTRACT(self.safe_mul(a, b) % Operators.ZEXTEND(c, 512),0, 256)
+            result = Operators.EXTRACT(self.safe_mul(a, b) % Operators.ZEXTEND(c, 512), 0, 256)
             result = Operators.ITEBV(256, c == 0, 0, result)
         except ZeroDivisionError:
             result = 0

From f4828428e989489568c35b8ce282e0786789fb74 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Thu, 10 Oct 2019 10:33:02 -0300
Subject: [PATCH 27/37] Better doc- review

---
 manticore/core/manticore.py     | 9 ++++++---
 manticore/ethereum/manticore.py | 4 +++-
 manticore/ethereum/solidity.py  | 3 +--
 3 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/manticore/core/manticore.py b/manticore/core/manticore.py
index 62c49dec0..f005540ce 100644
--- a/manticore/core/manticore.py
+++ b/manticore/core/manticore.py
@@ -635,18 +635,21 @@ def killed_states(self):
     def _all_states(self):
         """ Only allowed at not running.
             (At running we can have states at busy)
+            Returns a tuple with all active state ids.
+            Notably the "killed" states are not included here.
         """
         return tuple(self._ready_states) + tuple(
             self._terminated_states
-        )  # + tuple(self._killed_states)
-
+        )
     @property
     @sync
     def all_states(self):
         """
-        Iterates over the all states (ready and terminated and cancelled)
+        Iterates over the all states (ready and terminated)
         It holds a lock so no changes state lists are allowed
 
+        Notably the cancelled states are not included here.
+
         See also `ready_states`.
         """
         for state_id in self._all_states:
diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index b10c62179..c552810dd 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -1467,6 +1467,9 @@ def generate_testcase(self, state, message="", only_if=None, name="user"):
         :param state: The state to generate information about
         :param message: Accompanying message
         """
+        if not self.fix_unsound_symbolication(state):
+            return False
+
         if only_if is not None:
             with state as temp_state:
                 temp_state.constrain(only_if)
@@ -1681,7 +1684,6 @@ def worker_finalize(q):
                         for key, value in concrete_pairs:
                             global_summary.write("%s::%x\n" % (binascii.hexlify(key), value))
 
-        md = self.get_metadata(address)
         for address, md in self.metadata.items():
             with self._output.save_stream("global_%s.sol" % md.name) as global_src:
                 global_src.write(md.source_code)
diff --git a/manticore/ethereum/solidity.py b/manticore/ethereum/solidity.py
index e272473c5..6f8965104 100644
--- a/manticore/ethereum/solidity.py
+++ b/manticore/ethereum/solidity.py
@@ -109,8 +109,7 @@ def __build_source_map(self, bytecode, srcmap):
         # https://solidity.readthedocs.io/en/develop/miscellaneous.html#source-mappings
         new_srcmap = {}
         bytecode = self._without_metadata(bytecode)
-        if self.source_code and srcmap:
-
+        if self.source_code and bytecode and srcmap:
             asm_offset = 0
             asm_pos = 0
             md = dict(enumerate(srcmap[asm_pos].split(":")))

From 870fa05ad74f1bc15bb0e498e614d2c155623cff Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Fri, 11 Oct 2019 18:35:06 -0300
Subject: [PATCH 28/37] Better doc. Cleanups. sha3timeout changed

---
 manticore/core/manticore.py          |  5 +--
 manticore/core/smtlib/constraints.py |  3 +-
 manticore/core/smtlib/visitors.py    |  1 -
 manticore/core/state.py              |  5 +--
 manticore/ethereum/abi.py            |  3 +-
 manticore/ethereum/manticore.py      | 62 +++++++++++++++-------------
 manticore/platforms/evm.py           |  2 +-
 7 files changed, 41 insertions(+), 40 deletions(-)

diff --git a/manticore/core/manticore.py b/manticore/core/manticore.py
index f005540ce..cee72145b 100644
--- a/manticore/core/manticore.py
+++ b/manticore/core/manticore.py
@@ -638,9 +638,8 @@ def _all_states(self):
             Returns a tuple with all active state ids.
             Notably the "killed" states are not included here.
         """
-        return tuple(self._ready_states) + tuple(
-            self._terminated_states
-        )
+        return tuple(self._ready_states) + tuple(self._terminated_states)
+
     @property
     @sync
     def all_states(self):
diff --git a/manticore/core/smtlib/constraints.py b/manticore/core/smtlib/constraints.py
index 3cb4ed241..3d898bd62 100644
--- a/manticore/core/smtlib/constraints.py
+++ b/manticore/core/smtlib/constraints.py
@@ -140,8 +140,7 @@ def __get_related(self, related_to=None):
             related_constraints = set(self.constraints)
         return related_variables, related_constraints
 
-    def to_string(self, related_to=None, replace_constants=True):
-        replace_constants = False
+    def to_string(self, related_to=None, replace_constants=False):
         related_variables, related_constraints = self.__get_related(related_to)
 
         if replace_constants:
diff --git a/manticore/core/smtlib/visitors.py b/manticore/core/smtlib/visitors.py
index 19851da39..67437abfe 100644
--- a/manticore/core/smtlib/visitors.py
+++ b/manticore/core/smtlib/visitors.py
@@ -786,7 +786,6 @@ def to_constant(expression):
 
 @lru_cache(maxsize=128, typed=True)
 def simplify(expression):
-    expression = constant_folder(expression)
     expression = arithmetic_simplify(expression)
     return expression
 
diff --git a/manticore/core/state.py b/manticore/core/state.py
index cee21abfb..a331e08f0 100644
--- a/manticore/core/state.py
+++ b/manticore/core/state.py
@@ -314,12 +314,11 @@ def solve_one(self, *exprs, constrain=False):
         Concretize a symbolic :class:`~manticore.core.smtlib.expression.Expression` into
         one solution.
 
-        :param manticore.core.smtlib.Expression expr: Symbolic value to concretize
+        :param exprs: Symbolic value to concretize. An iterable of manticore.core.smtlib.Expression
         :param bool constrain: If True, constrain expr to concretized value
-        :return: Concrete value
+        :return: Concrete value or a tuple of concrete values
         :rtype: int
         """
-        # if len(exprs)>1:
         values = []
         for expr in exprs:
             if not issymbolic(expr):
diff --git a/manticore/ethereum/abi.py b/manticore/ethereum/abi.py
index ed3cdc47d..04fe24b8a 100644
--- a/manticore/ethereum/abi.py
+++ b/manticore/ethereum/abi.py
@@ -1,3 +1,4 @@
+import typing
 import logging
 import uuid
 
@@ -227,7 +228,7 @@ def deserialize(type_spec, data):
             raise EthereumError("Error {} deserializing type {:s}".format(str(e), type_spec))
 
     @staticmethod
-    def _deserialize(ty, buf, offset=0):
+    def _deserialize(ty, buf: typing.Union[bytearray, bytes, Array], offset=0):
         assert isinstance(buf, (bytearray, bytes, Array))
         result = None
         if ty[0] == "int":
diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index c552810dd..a9276bba9 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -68,7 +68,7 @@ def from_string(cls, name):
 )
 consts.add(
     "sha3timeout",
-    60 * 20,
+    60 * 90,
     "Default timeout for matching sha3 for unsound states (see unsound symbolication).",
 )
 
@@ -1187,11 +1187,11 @@ def on_unsound_symbolication(self, state, func, data, result):
                     break
             else:
                 # bijectiveness
-                for xa, ya in symbolic_pairs:
-                    if len(xa) == len(data):
-                        constraint = simplify((xa == data) == (ya == value))
+                for x, y in symbolic_pairs:
+                    if len(x) == len(data):
+                        constraint = simplify((x == data) == (y == value))
                     else:
-                        constraint = ya != value
+                        constraint = y != value
                     state.constrain(constraint)  # bijective
                 symbolic_pairs.append((data, value))
                 state.context[f"symbolic_func_sym_{name}"] = symbolic_pairs
@@ -1240,6 +1240,7 @@ def match(state, func, symbolic_pairs, concrete_pairs, start=None):
 
             """
             if time.time() - start > consts.sha3timeout:
+                logger.info("Timeout on sound check for state %d", state.id)
                 return False
 
             # The base case. No symbolic pairs. Just check if the state is feasible.
@@ -1284,34 +1285,37 @@ def match(state, func, symbolic_pairs, concrete_pairs, start=None):
                         return True
             return False
 
-        # Save concrete unction
+        soundcheck = state.context.get("soundcheck", None)
+        if soundcheck is not None:
+            return soundcheck
+
         with self.locked_context("ethereum", dict) as ethereum_context:
-            soundcheck = state.context.get("soundcheck", None)
-            if soundcheck is not None:
-                return soundcheck
             functions = ethereum_context.get("symbolic_func", dict())
-            for table in functions:
-                symbolic_pairs = state.context.get(f"symbolic_func_sym_{table}", ())
-                # if not constrain_bijectivity(state, symbolic_pairs):
-                #    # If UF does not comply with bijectiveness bail
-                #    return False
-
-                # symbolic_pairs = graph_sort(state, symbolic_pairs)
-                known_pairs = ethereum_context.get(f"symbolic_func_conc_{table}", set())
-                new_known_pairs = set(known_pairs)
-                if not match(
-                    state, functions[table], symbolic_pairs, new_known_pairs, start=time.time()
-                ):
-                    ethereum_context["soundcheck"] = False
-                    return False
+        for table in functions:
+            symbolic_pairs = state.context.get(f"symbolic_func_sym_{table}", ())
+            # if not constrain_bijectivity(state, symbolic_pairs):
+            #    # If UF does not comply with bijectiveness bail
+            #    return False
+
+            known_pairs = ethereum_context.get(f"symbolic_func_conc_{table}", set())
+            new_known_pairs = set(known_pairs)
+            if not match(
+                state, functions[table], symbolic_pairs, new_known_pairs, start=time.time()
+            ):
+                ethereum_context["soundcheck"] = False
+                return False
+
+            # Now paste the known pairs in the state constraints
+            concretize_known_pairs(state, symbolic_pairs, new_known_pairs)
+            state.context[f"symbolic_func_sym_{table}_done"] = symbolic_pairs
 
-                # Now paste the known pairs in the state constraints
-                concretize_known_pairs(state, symbolic_pairs, new_known_pairs)
-                ethereum_context[f"symbolic_func_conc_{table}"] = new_known_pairs
-                state.context[f"symbolic_func_sym_{table}_done"] = symbolic_pairs
+            # Share the concrete pairs with other states.
+            # Depends on the order in which the states are processed
+            # with self.locked_context("ethereum", dict) as ethereum_context:
+            #    ethereum_context[f"symbolic_func_conc_{table}"] = new_known_pairs
 
-            # Ok all functions had a match for current state
-            state.context["soundcheck"] = state.can_be_true(True)
+        # Ok all functions had a match for current state
+        state.context["soundcheck"] = state.can_be_true(True)
         return state.context["soundcheck"]
 
     def _terminate_state_callback(self, state, e):
diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index ba807cec5..1ff7e9bbf 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -1223,7 +1223,7 @@ def setstate(state, value):
                 "Concretize PC", expression=expression, setstate=setstate, policy="ALL"
             )
         # if self._checkpoint_data is None:
-        #   print(self)
+        #    print(self)
         # else:
         #    print ("back from a fork")
         # import pdb; pdb.set_trace()

From d3a5e8a4fb0d17895786c553e028a789f314fd63 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Tue, 15 Oct 2019 14:36:25 -0300
Subject: [PATCH 29/37] sha3 - 42mins

---
 manticore/ethereum/manticore.py | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index a9276bba9..e468a023e 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -1180,13 +1180,15 @@ def on_unsound_symbolication(self, state, func, data, result):
             value = state.new_symbolic_value(256)
 
             for x, y in symbolic_pairs:
+                # if we found another pair that matches use that instead
+                # the duplicated pair is not added to symbolic_pairs
                 if state.must_be_true(Operators.OR(x == data, y == value)):
                     constraint = simplify(Operators.AND(x == data, y == value))
                     state.constrain(constraint)
                     data, value = x, y
                     break
             else:
-                # bijectiveness
+                # bijectiveness; new pair is added to symbolic_pairs
                 for x, y in symbolic_pairs:
                     if len(x) == len(data):
                         constraint = simplify((x == data) == (y == value))
@@ -1195,6 +1197,7 @@ def on_unsound_symbolication(self, state, func, data, result):
                     state.constrain(constraint)  # bijective
                 symbolic_pairs.append((data, value))
                 state.context[f"symbolic_func_sym_{name}"] = symbolic_pairs
+
         else:
             value = func(data)
             with self.locked_context("ethereum", dict) as ethereum_context:
@@ -1253,7 +1256,7 @@ def match(state, func, symbolic_pairs, concrete_pairs, start=None):
             for i in range(len(symbolic_pairs)):
                 # shuffle and if it failed X times at some depth bail configurable
                 x, y = symbolic_pairs[i]
-                new_symbolic_pairs = symbolic_pairs[:i] + symbolic_pairs[i + 1 :]
+                new_symbolic_pairs = symbolic_pairs[:i] + symbolic_pairs[i + 1:]
                 new_concrete_pairs = set(concrete_pairs)
                 unseen = True  # Is added only unseen pairs could make it sat
                 for x_concrete, y_concrete in concrete_pairs:
@@ -1293,9 +1296,6 @@ def match(state, func, symbolic_pairs, concrete_pairs, start=None):
             functions = ethereum_context.get("symbolic_func", dict())
         for table in functions:
             symbolic_pairs = state.context.get(f"symbolic_func_sym_{table}", ())
-            # if not constrain_bijectivity(state, symbolic_pairs):
-            #    # If UF does not comply with bijectiveness bail
-            #    return False
 
             known_pairs = ethereum_context.get(f"symbolic_func_conc_{table}", set())
             new_known_pairs = set(known_pairs)

From 7893d93ca2921323a0c397c8c2371bc5a518f18f Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Tue, 15 Oct 2019 14:51:50 -0300
Subject: [PATCH 30/37] blkn

---
 manticore/ethereum/manticore.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index e468a023e..3fda69017 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -1256,7 +1256,7 @@ def match(state, func, symbolic_pairs, concrete_pairs, start=None):
             for i in range(len(symbolic_pairs)):
                 # shuffle and if it failed X times at some depth bail configurable
                 x, y = symbolic_pairs[i]
-                new_symbolic_pairs = symbolic_pairs[:i] + symbolic_pairs[i + 1:]
+                new_symbolic_pairs = symbolic_pairs[:i] + symbolic_pairs[i + 1 :]
                 new_concrete_pairs = set(concrete_pairs)
                 unseen = True  # Is added only unseen pairs could make it sat
                 for x_concrete, y_concrete in concrete_pairs:

From 2d2a3ee49f43314bd4b8b9da61e5bfca473eeeb6 Mon Sep 17 00:00:00 2001
From: Eric Hennenfent <eric.hennenfent@trailofbits.com>
Date: Tue, 22 Oct 2019 21:24:18 -0700
Subject: [PATCH 31/37] Fix spelling issues, duplicate code, and add type hints

---
 manticore/core/manticore.py         | 2 +-
 manticore/core/smtlib/expression.py | 5 -----
 manticore/ethereum/abi.py           | 8 +++++---
 manticore/ethereum/manticore.py     | 2 +-
 manticore/platforms/evm.py          | 2 +-
 5 files changed, 8 insertions(+), 11 deletions(-)

diff --git a/manticore/core/manticore.py b/manticore/core/manticore.py
index cee72145b..80caffc8a 100644
--- a/manticore/core/manticore.py
+++ b/manticore/core/manticore.py
@@ -665,7 +665,7 @@ def count_states(self):
     @sync
     def count_all_states(self):
         """ Total states count """
-        return len(self._all_states)
+        return self.count_states()
 
     @sync
     def count_ready_states(self):
diff --git a/manticore/core/smtlib/expression.py b/manticore/core/smtlib/expression.py
index 16bd0276f..6dce62503 100644
--- a/manticore/core/smtlib/expression.py
+++ b/manticore/core/smtlib/expression.py
@@ -236,11 +236,6 @@ def __init__(self, value, **kwargs):
         super().__init__(value, **kwargs)
 
 
-class BoolEqual(BoolOperation):
-    def __init__(self, a, b, **kwargs):
-        super().__init__(a, b, **kwargs)
-
-
 class BoolAnd(BoolOperation):
     def __init__(self, a, b, **kwargs):
         super().__init__(a, b, **kwargs)
diff --git a/manticore/ethereum/abi.py b/manticore/ethereum/abi.py
index 04fe24b8a..66fb679b8 100644
--- a/manticore/ethereum/abi.py
+++ b/manticore/ethereum/abi.py
@@ -303,7 +303,7 @@ def _serialize_uint(value, size=32, padding=0):
         return buffer
 
     @staticmethod
-    def _serialize_int(value, size=32, padding=0):
+    def _serialize_int(value: typing.Union[int, BitVec], size=32, padding=0):
         """
         Translates a signed python integral or a BitVec into a 32 byte string, MSB first
         """
@@ -356,7 +356,9 @@ def _readBE(data, nbytes, padding=False, offset=0):
         return Operators.CONCAT(nbytes * 8, *values)
 
     @staticmethod
-    def _deserialize_uint(data, nbytes=32, padding=0, offset=0):
+    def _deserialize_uint(
+        data: typing.Union[bytearray, bytes, Array], nbytes=32, padding=0, offset=0
+    ):
         """
         Read a `nbytes` bytes long big endian unsigned integer from `data` starting at `offset`
 
@@ -370,7 +372,7 @@ def _deserialize_uint(data, nbytes=32, padding=0, offset=0):
         return value
 
     @staticmethod
-    def _deserialize_int(data, nbytes=32, padding=0):
+    def _deserialize_int(data: typing.Union[bytearray, bytes, Array], nbytes=32, padding=0):
         """
         Read a `nbytes` bytes long big endian signed integer from `data` starting at `offset`
 
diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index 3fda69017..39f6f2f0a 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -1156,7 +1156,7 @@ def on_unsound_symbolication(self, state, func, data, result):
         """
 
         name = func.__name__
-        # Save concrete unction
+        # Save concrete function
         with self.locked_context("ethereum", dict) as ethereum_context:
             functions = ethereum_context.get("symbolic_func", dict())
             functions[name] = func
diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index 1ff7e9bbf..b62c29b25 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -3082,7 +3082,7 @@ def dump(self, stream, state, mevm, message):
             with state.constraints as temp_cs:
                 # make a free symbolic idex that could address any storage slot
                 index = temp_cs.new_bitvec(256)
-                # get the storage for accounbt_address
+                # get the storage for account_address
                 storage = blockchain.get_storage(account_address)
                 # we are interested only in used slots
                 temp_cs.add(storage.get(index) != 0)

From df1545748d0b5119b6399dc2574a83a4b3392bba Mon Sep 17 00:00:00 2001
From: Eric Hennenfent <eric.hennenfent@trailofbits.com>
Date: Tue, 22 Oct 2019 21:38:13 -0700
Subject: [PATCH 32/37] Rm commented code

Done as a separate commit for easy reversion
---
 manticore/platforms/evm.py | 17 -----------------
 1 file changed, 17 deletions(-)

diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
index 1a7c3ef3f..77ad46ba9 100644
--- a/manticore/platforms/evm.py
+++ b/manticore/platforms/evm.py
@@ -1222,28 +1222,11 @@ def setstate(state, value):
             raise Concretize(
                 "Concretize PC", expression=expression, setstate=setstate, policy="ALL"
             )
-        # if self._checkpoint_data is None:
-        #    print(self)
-        # else:
-        #    print ("back from a fork")
-        # import pdb; pdb.set_trace()
         try:
-            # import time
-            # limbo = 0.0
-            # a = time.time()
             self._check_jmpdest()
-            # b = time.time()
             last_pc, last_gas, instruction, arguments, fee, allocated = self._checkpoint()
-            # c = time.time()
-            # d = time.time()
             result = self._handler(*arguments)
-            # e = time.time()
             self._advance(result)
-            # f = time.time()
-            # if hasattr(self, 'F'):
-            #    limbo = (a-self.F)*100
-            # print(f"{instruction}\t\t %02.4f %02.4f %02.4f %02.4f %02.4f %02.4f"%((b-a)*100, (c-b)*100, (d-c)*100, (e-d)*100, (f-e)*100, limbo))
-            # self.F = time.time()
 
         except ConcretizeGas as ex:
 

From 07edfd5b32a5dcd39c5ca5d9873fc6cf0520a691 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Wed, 30 Oct 2019 10:43:41 -0300
Subject: [PATCH 33/37] review

---
 manticore/core/smtlib/visitors.py |  2 --
 tests/other/test_smtlibv2.py      | 31 +++++++++++++++++++++++++++++--
 2 files changed, 29 insertions(+), 4 deletions(-)

diff --git a/manticore/core/smtlib/visitors.py b/manticore/core/smtlib/visitors.py
index ae81c2676..696d0b295 100644
--- a/manticore/core/smtlib/visitors.py
+++ b/manticore/core/smtlib/visitors.py
@@ -331,8 +331,6 @@ def visit_BoolAnd(self, expression, a, b):
             return b
         if isinstance(b, Constant) and b.value == True:
             return a
-        if a is b:
-            return a
 
     def visit_Operation(self, expression, *operands):
         """ constant folding, if all operands of an expression are a Constant do the math """
diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py
index bf9ccab27..ddca37cc6 100644
--- a/tests/other/test_smtlibv2.py
+++ b/tests/other/test_smtlibv2.py
@@ -106,16 +106,43 @@ def testSolver(self):
         cs.add(a + b > 100)
         self.assertTrue(self.solver.check(cs))
 
-    def testBool(self):
+    def testBool1(self):
         cs = ConstraintSet()
         bf = BoolConstant(False)
         bt = BoolConstant(True)
         cs.add(Operators.AND(bf, bt))
+        self.assertFalse(self.solver.check(cs))
+
+    def testBool2(self):
+        cs = ConstraintSet()
+        bf = BoolConstant(False)
+        bt = BoolConstant(True)
         cs.add(Operators.AND(bf, bt, bt, bt))
+        self.assertFalse(self.solver.check(cs))
+
+    def testBool3(self):
+        cs = ConstraintSet()
+        bf = BoolConstant(False)
+        bt = BoolConstant(True)
+        cs.add(Operators.AND(bt, bt, bf, bt))
+        self.assertFalse(self.solver.check(cs))
+
+    def testBool4(self):
+        cs = ConstraintSet()
+        bf = BoolConstant(False)
+        bt = BoolConstant(True)
         cs.add(Operators.OR(True, bf))
         self.assertFalse(self.solver.check(cs))
 
-    def testBasicArray(self):
+    def testBool5(self):
+        cs = ConstraintSet()
+        bf = BoolConstant(False)
+        bt = BoolConstant(True)
+        cs.add(Operators.OR(bt, bt, False))
+        self.assertFalse(self.solver.check(cs))
+
+
+def testBasicArray(self):
         cs = ConstraintSet()
         # make array of 32->8 bits
         array = cs.new_array(32)

From 47105d5b33919daddaa453e0f1840c2a055b2559 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Wed, 30 Oct 2019 10:44:40 -0300
Subject: [PATCH 34/37] blkn

---
 tests/other/test_smtlibv2.py | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py
index ddca37cc6..a32f761f3 100644
--- a/tests/other/test_smtlibv2.py
+++ b/tests/other/test_smtlibv2.py
@@ -141,8 +141,7 @@ def testBool5(self):
         cs.add(Operators.OR(bt, bt, False))
         self.assertFalse(self.solver.check(cs))
 
-
-def testBasicArray(self):
+    def testBasicArray(self):
         cs = ConstraintSet()
         # make array of 32->8 bits
         array = cs.new_array(32)

From f3db81df0bc6ec266c7b37cba2ade18bdce0d3d6 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Wed, 30 Oct 2019 11:20:20 -0300
Subject: [PATCH 35/37] Remove hardcoded conf

---
 manticore/ethereum/manticore.py | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index d8036c939..38dfd9a3a 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -63,12 +63,12 @@ def from_string(cls, name):
 consts.add("defaultgas", 3000000, "Default gas value for ethereum transactions.")
 consts.add(
     "sha3",
-    default=Sha3Type.concretize,
+    default=Sha3Type.symbolicate,
     description="concretize(*): sound simple concretization\nsymbolicate: unsound symbolication with out of cycle false positive killing",
 )
 consts.add(
     "sha3timeout",
-    60 * 90,
+    60 * 60,
     "Default timeout for matching sha3 for unsound states (see unsound symbolication).",
 )
 
@@ -399,7 +399,6 @@ def __init__(self, workspace_url: str = None, policy: str = "random"):
         super().__init__(initial_state, workspace_url=workspace_url, policy=policy)
         self.subscribe("will_terminate_state", self._terminate_state_callback)
         self.subscribe("did_evm_execute_instruction", self._did_evm_execute_instruction_callback)
-        consts.sha3 = consts.sha3.symbolicate
         if consts.sha3 is consts.sha3.concretize:
             self.subscribe("on_symbolic_function", self._on_concretize)
         elif consts.sha3 is consts.sha3.symbolicate:

From b88ed2763e087ee7ece13ad0e6d8b677831ce5b4 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Wed, 30 Oct 2019 12:01:05 -0300
Subject: [PATCH 36/37] Fix expression bool test

---
 tests/other/test_smtlibv2.py | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/tests/other/test_smtlibv2.py b/tests/other/test_smtlibv2.py
index a32f761f3..4679c4a45 100644
--- a/tests/other/test_smtlibv2.py
+++ b/tests/other/test_smtlibv2.py
@@ -132,14 +132,8 @@ def testBool4(self):
         bf = BoolConstant(False)
         bt = BoolConstant(True)
         cs.add(Operators.OR(True, bf))
-        self.assertFalse(self.solver.check(cs))
-
-    def testBool5(self):
-        cs = ConstraintSet()
-        bf = BoolConstant(False)
-        bt = BoolConstant(True)
         cs.add(Operators.OR(bt, bt, False))
-        self.assertFalse(self.solver.check(cs))
+        self.assertTrue(self.solver.check(cs))
 
     def testBasicArray(self):
         cs = ConstraintSet()

From 4c791304b5fe38649f8fc496c22b08f862ccfe46 Mon Sep 17 00:00:00 2001
From: feliam <felipe.andres.manzano@gmail.com>
Date: Wed, 30 Oct 2019 13:38:21 -0300
Subject: [PATCH 37/37] Fix sha3concrete test

---
 manticore/ethereum/manticore.py | 4 ++--
 tests/ethereum/test_sha3.py     | 7 ++-----
 2 files changed, 4 insertions(+), 7 deletions(-)

diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py
index 38dfd9a3a..213e126ae 100644
--- a/manticore/ethereum/manticore.py
+++ b/manticore/ethereum/manticore.py
@@ -1120,7 +1120,7 @@ def _on_concretize(self, state, func, data, result):
         if not issymbolic(data):
             y_concrete = func(data)
         else:
-            with self.locked_context("ethereum") as context:
+            with self.locked_context("ethereum", dict) as context:
                 # adding a single random example so we can explore further
                 x_concrete = state.solve_one(data)
                 y_concrete = func(x_concrete)
@@ -1292,7 +1292,7 @@ def match(state, func, symbolic_pairs, concrete_pairs, start=None):
             return soundcheck
 
         with self.locked_context("ethereum", dict) as ethereum_context:
-            functions = ethereum_context.get("symbolic_func", dict())
+            functions = ethereum_context.get("symbolic_func", list())
         for table in functions:
             symbolic_pairs = state.context.get(f"symbolic_func_sym_{table}", ())
 
diff --git a/tests/ethereum/test_sha3.py b/tests/ethereum/test_sha3.py
index 3bb0936d2..be7eb2677 100644
--- a/tests/ethereum/test_sha3.py
+++ b/tests/ethereum/test_sha3.py
@@ -473,11 +473,8 @@ def test_example_concrete_1(self):
                 continue
             found += len(st.platform.logs)
 
-        self.assertEqual(found, 1)  # log is reachable
-        # x==10 && y == 10
-        # x==C  && y == C && C != 10 #log
-        # x != y
-        self.assertEqual(m.count_all_states(), 3)
+        self.assertEqual(found, 1)  # log is reachable (depends on concretization)
+        self.assertEqual(m.count_all_states(), 1)  # Only 1 state concretized
 
 
 if __name__ == "__main__":