From ce5b936a7fb7af4d61baae2b9c5abd10ecacebc6 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Mon, 2 Dec 2024 21:24:59 +1100
Subject: [PATCH] HOTFIX abort rewrite when SMT solver times out

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.
---
 booster/library/Booster/Pattern/Rewrite.hs | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs
index 920c8ea18e..635104f4fc 100644
--- a/booster/library/Booster/Pattern/Rewrite.hs
+++ b/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 $