fix unsafe setup_ex.path.to_smt2() access

Author: 0xkarmacoma

src/halmos/__main__.py

@@ -318,7 +318,7 @@ def setup(ctx: FunctionContext) -> Exec:
     )
 
     setup_exs_all = sevm.run(setup_ex)
-    setup_exs_no_error: list[Exec] = []
+    setup_exs_no_error: list[tuple[Exec, SMTQuery]] = []
 
     for path_id, setup_ex in enumerate(setup_exs_all):
         if args.verbose >= VERBOSITY_TRACE_SETUP:
@@ -339,24 +339,25 @@ def setup(ctx: FunctionContext) -> Exec:
                 render_trace(setup_ex.context)
 
         else:
-            setup_exs_no_error.append(setup_ex)
+            # note: ex.path.to_smt2() needs to be called at this point. The solver object is shared across paths,
+            # and solver.to_smt2() will return a different query if it is called after a different path is explored.
+            setup_exs_no_error.append((setup_ex, setup_ex.path.to_smt2(args)))
 
     setup_exs: list[Exec] = []
 
     match setup_exs_no_error:
         case []:
             pass
-        case [ex]:
+        case [(ex, _)]:
             setup_exs.append(ex)
         case _:
-            for path_id, ex in enumerate(setup_exs_no_error):
+            for path_id, (ex, query) in enumerate(setup_exs_no_error):
                 path_ctx = PathContext(
                     args=args,
                     path_id=path_id,
-                    query=ex.path.to_smt2(args),
+                    query=query,
                     solving_ctx=ctx.solving_ctx,
                 )
-
                 solver_output = solve_low_level(path_ctx)
                 if solver_output.result != unsat:
                     setup_exs.append(ex)

src/halmos/solve.py

@@ -445,8 +445,10 @@ def solve_end_to_end(ctx: PathContext) -> SolverOutput:
         refined_ctx = ctx.refine()
 
         if refined_ctx.query.smtlib != query.smtlib:
-            # recurse with the refined query
-            return solve_end_to_end(refined_ctx)
+            # note that check_unsat_cores cannot return true for the refined query, because it relies on only
+            # constraint ids, which don't change after refinement
+            # therefore we can skip the unsat core check in solve_end_to_end and go directly to solve_low_level
+            return solve_low_level(refined_ctx)
         else:
             verbose("    Refinement did not change the query, no need to solve again")