Skip to content

handle failed solver processes #567

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
daejunpark wants to merge 2 commits into from
Closed

handle failed solver processes #567

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e3b548b
handle failed solver processes
daejunpark Jul 26, 2025
cec9fda
Merge branch 'main' into fix/solver-process-exception
daejunpark Jul 26, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions src/halmos/__main__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1193,6 +1193,11 @@ def run_test(ctx: FunctionContext) -> TestResult:
REVERT_ALL,
f"{funsig}: all paths have been reverted; the setup state or inputs may have been too restrictive.",
)
elif len(ctx.solver_outputs) < len(submitted_futures):
Copy link
Contributor

@0xkarmacoma 0xkarmacoma Jul 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm a bit concerned about relying on the number of solver outputs to infer that an error occured

when an exception is raised in solver subprocesses, their result may not be added to the solver_outputs list

this seems to be the real issue? ideally we want to capture the errors and add failed outputs to ctx.solver_outputs, no?

Copy link
Collaborator Author

@daejunpark daejunpark Jul 28, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ideally we want to capture the errors and add failed outputs to ctx.solver_outputs, no?

yes, but it needs some more work, as the solver output object currently needs more info that isn't available at some places exceptions occur.

# some solver results are missing, likely due to exceptions.
# not an early exit, as counter["sat"] > 0 would have been handled earlier.
passfail = color_error("[ERROR]")
exitcode = Exitcode.EXCEPTION.value
else:
passfail = color_good("[PASS]")
exitcode = Exitcode.PASS.value
Expand Down
Loading