HOTFIX abort rewrite when SMT solver times out (#4078)

When the SMT solver timed out while checking `requires` clauses of a
rule, the unclear conditions were returned in the same way as conditions
that were known to be indeterminate. This created bogus branches in
proofs when the solver had a problem to decide a condition.

On such timeouts, and on inconsistent ground truths, booster now aborts
the entire rewrite. This might lead to increased spurious aborts in
complex proofs, but is probably better than having to prune the bogus
branches from the client side. The fall-back to legacy kore was able to
prune the bogus branch easily in the case that was investigated.

Author: jberthold

booster/library/Booster/Pattern/Rewrite.hs

@@ -590,15 +590,18 @@ applyRule pat@Pattern{ceilConditions} rule =
         -- check unclear requires-clauses in the context of known constraints (priorKnowledge)
         solver <- lift $ RewriteT $ (.smtSolver) <$> ask
         SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList stillUnclear) >>= \case
-            SMT.IsUnknown reason -> do
-                withContext CtxWarn $ logMessage reason
-                -- return unclear rewrite rule condition if the condition is indeterminate
-                withContext CtxConstraint . withContext CtxWarn . logMessage $
+            SMT.IsUnknown SMT.ImplicationIndeterminate -> do
+                -- return unclear conditions if SMT solver reports the condition indeterminate
+                withContexts [CtxConstraint, CtxSMT] . logMessage $
                     WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> stillUnclear)]) $
                         renderOneLineText $
-                            "Uncertain about condition(s) in a rule:"
+                            "Indeterminate condition(s) after SMT solver:"
                                 <+> (hsep . punctuate comma . map (pretty' @mods) $ stillUnclear)
-                pure unclearRequires
+                pure stillUnclear
+            SMT.IsUnknown reason -> do
+                -- abort on unclear predicates due to SMT solver timeout or inconsistent ground truth
+                withContexts [CtxConstraint, CtxSMT, CtxWarn] $ logMessage reason
+                smtUnclear stillUnclear
             SMT.IsInvalid -> do
                 -- requires is actually false given the prior
                 withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
@@ -649,7 +652,7 @@ applyRule pat@Pattern{ceilConditions} rule =
 
         pure newConstraints
 
-    smtUnclear :: [Predicate] -> RewriteRuleAppT (RewriteT io) ()
+    smtUnclear :: [Predicate] -> RewriteRuleAppT (RewriteT io) a
     smtUnclear predicates = do
         ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
         withContext CtxConstraint . withContext CtxAbort . logMessage $