Abort on "Unknown" side conditions, don't crash #3907
Conversation
There was a problem hiding this comment.
I'd really want to merge this because it is a good idea in general (and it would fix an issue with my PR #3904 ), but I think it changes the intent of the SMTError and mixes results and errors.
The correct model would IMHO be to return Either SMTError (Maybe Bool) and catch the SMTSolverUnknown case.
| Left _ -> do | ||
| -- TODO: we could process SMTError here |
There was a problem hiding this comment.
We should probably restrict this to the SMTSolverUnknown case. An SMTTranslationError is an entirely different case (and the General error was meant to cover infrastructure issues).
| let errMsg = ("Inconsistent ground truth, check returns Nothing" :: Text) | ||
| Log.logMessage errMsg | ||
| throwE $ GeneralSMTError errMsg |
There was a problem hiding this comment.
This is not really an "error", rather a defensive strategy to avoid jumping to unjustified conclusions
| @@ -324,22 +322,22 @@ checkPredicates ctxt givenPs givenSubst psToCheck | |||
|
|
|||
| case (positive, negative) of | |||
| (Unsat, Unsat) -> throwSMT "Inconsistent ground truth: should have been caught above" | |||
| (Sat, Sat) -> fail "Implication not determined" | |||
| (Sat, Sat) -> throwE $ GeneralSMTError "Implication not determined" | |||
There was a problem hiding this comment.
Same here, this is actually a result (neither P nor not P are implied)
…d of exceptions (#3908) * Re-introduces the 'indeterminate' result for checkPredicates, and returns that on inconsistent ground truth. * In the rewrite, aborts on `SMTSolverUnknown` when checking requires clauses, but throws actual exceptions (terminating the request) on other SMT errors (translation error, general error). Follow-up to #3907
This PR makes sure we do not immediately hard-stop with an RPC error when receiving
Unknownfrom Z3 in Booster.checkPredicatesUnknownpredicates as any other unclear conditions: abort rewriting