Manticore verifier

.github/workflows/ci.yml

@@ -167,8 +167,8 @@ jobs:
             coverage run -m manticore . --contract MetaCoin --workspace output --exclude-all --evm.oog ignore --evm.txfail optimistic
             # Truffle smoke test. We test if manticore is able to generate states
             # from a truffle project. 
-            if [ "$(ls output/*tx -l | wc -l)" != "26" ]; then
-                echo "Truffle test failed" `ls output/*tx -l | wc -l` "!= 26"
+            if [ "$(ls output/*tx -l | wc -l)" -lt "25" ]; then
+                echo "Truffle test failed" `ls output/*tx -l | wc -l` "< 25"
                 return 1
             fi
             echo "Truffle test succeded"

manticore/__main__.py

@@ -212,9 +212,7 @@ def positive(value):
     )
 
     eth_flags.add_argument(
-        "--limit-loops",
-        action="store_true",
-        help="Avoid exploring constant functions for human transactions",
+        "--limit-loops", action="store_true", help="Limit loops depth",
     )
 
     eth_flags.add_argument(

manticore/core/manticore.py

@@ -428,6 +428,16 @@ def clear_terminated_states(self):
             self._remove(state_id)
         assert self.count_terminated_states() == 0
 
+    @sync
+    @at_not_running
+    def clear_ready_states(self):
+        """ Simply remove all states from terminated list """
+        terminated_states_ids = tuple(self._terminated_states)
+        for state_id in terminated_states_ids:
+            self._terminated_states.remove(state_id)
+            self._remove(state_id)
+        assert self.count_terminated_states() == 0
+
     def __str__(self):
         return f"<{str(type(self))[8:-2]}| Alive States: {self.count_ready_states()}; Running States: {self.count_busy_states()} Terminated States: {self.count_terminated_states()} Killed States: {self.count_killed_states()} Started: {self._running.value} Killed: {self._killed.value}>"
 

manticore/core/smtlib/solver.py

@@ -593,7 +593,7 @@ def get_value(self, constraints: ConstraintSet, *expressions):
         """
         values = []
         start = time.time()
-        with constraints as temp_cs:
+        with constraints.related_to(*expressions) as temp_cs:
             for expression in expressions:
                 if not issymbolic(expression):
                     values.append(expression)