Fix crash on low rlimit #859
Conversation
| // Sometimes Z3 responds with "(error ...)" followed by "unknown" | ||
| if (outcomeSExp.Name is "error" && responseStack.TryPeek(out var sExpr) && sExpr.Name is "unknown") { | ||
| responseStack.Pop(); | ||
| } |
There was a problem hiding this comment.
Would it be better to do this before ParseOutcome(...) instead? Or perhaps we should also set wasUnknown to true ourselves so we hit ParseReasonUnknown below?
There was a problem hiding this comment.
I considered that, but ultimately the error message is what really tells us what the outcome is, somewhat confusingly.
|
|
||
| if (options.LibOptions.ProduceUnsatCores) { | ||
| if (options.LibOptions.ProduceUnsatCores && responseStack.Count > 0) { |
There was a problem hiding this comment.
Shouldn't we communicate some kind of error explicitly if ProduceUnsatCores is on but responseStack is empty?
There was a problem hiding this comment.
Yes, we should. I'll add that.
| @@ -1209,6 +1209,7 @@ protected SolverOutcome ParseOutcome(SExpr resp, out bool wasUnknown) | |||
| case "error": | |||
| if (resp.Arguments.Length == 1 && resp.Arguments[0].IsId && | |||
| (resp.Arguments[0].Name.Contains("max. resource limit exceeded") | |||
| || resp.Arguments[0].Name.Contains("push canceled") | |||
There was a problem hiding this comment.
Is this because the only reason a push is ever cancelled is when Boogie itself determines resource limits are reached?
There was a problem hiding this comment.
Yes, exactly. I've confirmed this in the Z3 source code.
### Description Bump Boogie dependency to v3.1.3 This most importantly includes boogie-org/boogie#859 ### How has this been tested? Existing tests should be sufficient. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
Z3 has multiple ways of responding that the resource limit has been exceeded. In some cases it responds with an error message including "push canceled". This updates Boogie to handle more of the strange side cases.