fix: avoid raising when path exploration > first cex

src/halmos/__main__.py

@@ -56,6 +56,7 @@
     warn_code,
 )
 from .mapper import BuildOut, DeployAddressMapper
+from .processes import ShutdownError
 from .sevm import (
     EMPTY_BALANCE,
     EVM,
@@ -522,6 +523,12 @@ def solve_end_to_end_callback(future: Future):
     path_id = 0  # default value in case we don't enter the loop body
     submitted_futures = []
     for path_id, ex in enumerate(exs):
+        # check if early exit is triggered
+        if ctx.solving_ctx.executor.is_shutdown():
+            if args.debug:
+                print("aborting path exploration, executor has been shutdown")
+            break
+
         # cache exec in case we need to print it later
         if args.print_failed_states:
             ctx.exec_cache[path_id] = ex
@@ -560,9 +567,14 @@ def solve_end_to_end_callback(future: Future):
                 solving_ctx=ctx.solving_ctx,
             )
 
-            solve_future = ctx.thread_pool.submit(solve_end_to_end, path_ctx)
-            solve_future.add_done_callback(solve_end_to_end_callback)
-            submitted_futures.append(solve_future)
+            try:
+                solve_future = ctx.thread_pool.submit(solve_end_to_end, path_ctx)
+                solve_future.add_done_callback(solve_end_to_end_callback)
+                submitted_futures.append(solve_future)
+            except ShutdownError:
+                if args.debug:
+                    print("aborting path exploration, executor has been shutdown")
+                break
 
         elif ex.context.is_stuck():
             debug(f"Potential error path (id: {path_id})")

src/halmos/processes.py

@@ -23,7 +23,8 @@ def register(self, executor):
         self._executors.add(executor)
 
     def shutdown_all(self):
-        print("Shutting down all executors")
+        """Shuts down all registered executors."""
+
         for ex in list(self._executors):
             ex.shutdown(wait=False)
 
@@ -134,6 +135,10 @@ def is_running(self):
         return self.process and self.process.poll() is None
 
 
+class ShutdownError(RuntimeError):
+    """Raised when submitting a future to an executor that has been shutdown."""
+
+
 class PopenExecutor(concurrent.futures.Executor):
     """
     An executor that runs commands in subprocesses.
@@ -154,11 +159,13 @@ def __init__(self, max_workers: int = 1):
     def futures(self):
         return self._futures
 
-    def submit(self, future: PopenFuture):
-        """Accepts an unstarted PopenFuture and schedules it for execution."""
+    def submit(self, future: PopenFuture) -> PopenFuture:
+        """Accepts an unstarted PopenFuture and schedules it for execution.
+
+        Raises ShutdownError if the executor has been shutdown."""
 
         if self._shutdown.is_set():
-            raise RuntimeError("Cannot submit to a shutdown executor.")
+            raise ShutdownError()
 
         with self._lock:
             self._futures.append(future)