From 5068e5901ee39466755244953da9ade51000ba12 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Wed, 22 Jan 2025 15:00:00 -0800 Subject: [PATCH] finish merge --- src/halmos/__main__.py | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 4956dd1c..720b2c52 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -568,12 +568,20 @@ def solve_end_to_end_callback(future: Future): submitted_futures.append(solve_future) elif ex.context.is_stuck(): - debug(f"Potential error path (id: {idx+1})") - res, _, _ = solve(ex.path.to_smt2(args), args) + debug(f"Potential error path (id: {path_id})") + path_ctx = PathContext( + args=args, + path_id=path_id, + query=ex.path.to_smt2(args), + solving_ctx=ctx.solving_ctx, + ) + res, _, _ = solve_low_level(path_ctx) if res != unsat: - stuck.append((idx, ex, ex.context.get_stuck_reason())) + stuck.append((path_id, ex, ex.context.get_stuck_reason())) if args.print_blocked_states: - traces[idx] = f"{hexify(ex.path)}\n{rendered_trace(ex.context)}" + ctx.traces[path_id] = ( + f"{hexify(ex.path)}\n{rendered_trace(ex.context)}" + ) elif not error_output: if args.print_success_states: