Demote Abort log to Warn

runtimeverification · Oct 23, 2024 · 5bec591 · 5bec591
1 parent 7455041
commit 5bec591
Show file tree

Hide file tree

Showing 2 changed files with 401 additions and 1 deletion.
diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs
@@ -530,7 +530,7 @@ applyRule pat@Pattern{ceilConditions} rule =
         solver <- lift $ RewriteT $ (.smtSolver) <$> ask
         SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList stillUnclear) >>= \case
             SMT.IsUnknown reason -> do
-                withContext CtxAbort $ logMessage reason
+                withContext CtxWarn $ logMessage reason
                 -- return unclear rewrite rule condition if the condition is indeterminate
                 withContext CtxConstraint . withContext CtxWarn . logMessage $
                     WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> stillUnclear)]) $