perf: isolate overhead for unsat core query generation

src/halmos/__main__.py

@@ -1072,9 +1072,10 @@ def solve(
         if not dump_filename:
             dump_filename = f"/tmp/{uuid.uuid4().hex}.smt2"
 
-        named_assertions = "".join(
-            [f"(assert (! |{assert_id}| :named <{assert_id}>))\n" for assert_id in query.assertions]
-        )
+        if args.cache_solver:
+            named_assertions = "".join(
+                [f"(assert (! |{assert_id}| :named <{assert_id}>))\n" for assert_id in query.assertions]
+            )
 
         with open(dump_filename, "w") as f:
             if args.verbose >= 1:
@@ -1083,7 +1084,8 @@ def solve(
                 f.write("(set-option :produce-unsat-cores true)\n")
             f.write("(set-logic QF_AUFBV)\n")
             f.write(query.smtlib)
-            f.write(named_assertions)
+            if args.cache_solver:
+                f.write(named_assertions)
             f.write("(check-sat)\n")
             f.write("(get-model)\n")
             if args.cache_solver:
@@ -1126,8 +1128,11 @@ def solve(
         ctx = Context()
         solver = mk_solver(args, ctx=ctx, assertion=True)
         solver.from_string(query.smtlib)
-        ids = [Bool(f"{x}", ctx) for x in query.assertions]
-        result = solver.check(*ids)
+        if args.cache_solver:
+            ids = [Bool(f"{x}", ctx) for x in query.assertions]
+            result = solver.check(*ids)
+        else:
+            result = solver.check()
         model = copy_model(solver.model()) if result == sat else None
 
         unsat_core = None

src/halmos/sevm.py

@@ -508,10 +508,13 @@ def __str__(self) -> str:
     def to_smt2(self, args) -> SMTQuery:
         ids = [str(cond.get_id()) for cond in self.conditions]
 
-        tmp_solver = SolverFor("QF_AUFBV")
-        for cond in self.conditions:
-            tmp_solver.assert_and_track(cond, str(cond.get_id()))
-        query = tmp_solver.to_smt2()
+        if args.cache_solver:
+            tmp_solver = SolverFor("QF_AUFBV")
+            for cond in self.conditions:
+                tmp_solver.assert_and_track(cond, str(cond.get_id()))
+            query = tmp_solver.to_smt2()
+        else:
+            query = self.solver.to_smt2()
         query = query.replace("(check-sat)", "")  # see __main__.solve()
 
         return SMTQuery(query, ids)