-
Notifications
You must be signed in to change notification settings - Fork 112
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.
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
Fix hanging when solver exits with a non-zero exit code #821
Conversation
The text of the I/O error is slightly different
@@ -74,6 +75,10 @@ public SMTLibProcess(SMTLibOptions libOptions, SMTLibSolverOptions options) | |||
|
|||
private void SolverExited(object sender, EventArgs e) | |||
{ | |||
if (options.Verbosity >= 2) { | |||
Console.WriteLine($"[SMT-ERR-{{0}}] Solver exited with code {solver.ExitCode}."); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'd ask you to avoid calls to Console.
, but I see this file already contains them ^,^
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, we should refactor it to use something more parameterized.
Looks amazing. How did you find this? Also, I added a commit to increment the version. |
It was a rather frustrating bout of debugging, I must say! I've known that this was an issue for a while, and I expected that the
Thanks! |
Previously, if the solver quit abruptly with a non-zero exit code (such as for a segmentation fault), Boogie would hang. These changes turn that into a well-behaved solver exception.