create solver_output in case of errors too #570
Conversation
surprisingly hard to figure out what the corresponding path_id/query was when we get an error, so for now let's make this optional in solver_output this properly returns [ERROR] on tests that have solver_outputs with errors (could be PASS previously)
There was a problem hiding this comment.
Pull Request Overview
This PR improves error handling in the Halmos symbolic execution tool by ensuring that SolverOutput objects are created even when solver errors occur. This addresses an issue where it was difficult to determine the corresponding path_id and query when errors happened.
Key changes:
- Adds a new
from_errorstatic method toSolverOutputclass for creating error outputs - Refactors error handling in the solve callback to always create
SolverOutputobjects - Updates test configuration to use z3 solver instead of cvc5
Reviewed Changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| src/halmos/solve.py | Adds from_error static method to SolverOutput for creating error outputs |
| src/halmos/main.py | Refactors error handling to always create SolverOutput objects and improves error reporting |
| tests/test_config.py | Updates test configuration to use z3 solver instead of cvc5 |
| if not is_benign_solving_error(e): | ||
| error(f"encountered exception during assertion solving: {e!r}") | ||
| return SolverOutput.from_error(e, path_id=path_id, query_file=query_file) | ||
|
|
There was a problem hiding this comment.
originally, other OSErrors were re-raised from the catch block, but now they aren't. does this not alter behavior because exceptions raised from callbacks are silently ignored anyway?
There was a problem hiding this comment.
well I'm not sure why we re-raised, but it seems to me this is a good place to capture errors and keep track of errors
surprisingly hard to figure out what the corresponding path_id/query was when we get an error, so for now let's make this optional in solver_output
this properly returns [ERROR] on tests that have solver_outputs with errors (could be PASS previously)