tests/ethereum_bench/test_consensys_benchmark.py FE                                                              [100%]

======================================================== ERRORS ========================================================
_______________________ ERROR at teardown of EthBenchmark.test_integer_overflow_storageinvariant _______________________

self = <tests.ethereum_bench.test_consensys_benchmark.EthBenchmark testMethod=test_integer_overflow_storageinvariant>

    def tearDown(self):
>       self.mevm.finalize()

tests/ethereum_bench/test_consensys_benchmark.py:28:
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
manticore/core/manticore.py:128: in newFunction
    return func(self, *args, **kw)
manticore/ethereum/manticore.py:1738: in finalize
    "{:x}: {:2.2f}%\n".format(int(address), self.global_coverage(address))
manticore/ethereum/manticore.py:1814: in global_coverage
    runtime_bytecode = state.solve_one(code)
manticore/core/state.py:344: in solve_one
    return self.solve_one_n(expr, constrain=constrain)[0]
manticore/core/state.py:362: in solve_one_n
    value = self._solver.get_value(self._constraints, expr)
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _

self = <manticore.core.smtlib.solver.Z3Solver object at 0x7f32e7f27370>
constraints = <manticore.core.smtlib.constraints.ConstraintSet object at 0x7f32e7c23b50>
expressions = (<ArrayProxy at 7f32e7cd4590>,), values = [], start = 1586986530.1181638
temp_cs = <manticore.core.smtlib.constraints.ConstraintSet object at 0x7f32e7c93bb0>

    def get_value(self, constraints, *expressions):
        """
        Ask the solver for one possible result of given expressions using
        given set of constraints.
        """
        values = []
        start = time.time()
        with constraints as temp_cs:
            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.to_string())
                    if not self._is_sat():
>                       raise SolverError(
                            "Solver could not find a value for expression under current constraint set"
                        )
E                       manticore.exceptions.SolverError: Solver could not find a value for expression under current constraint set

manticore/core/smtlib/solver.py:622: SolverError