Emit log only if the remainder is satisfiable

Author: geo2a

kore/src/Kore/Log/DebugRewriteRulesRemainder.hs

@@ -38,10 +38,15 @@ import Pretty (
  )
 import Pretty qualified
 
+{- This log entry will be emitted if, after unifying with rewrite rules,
+   there is a satisfiable remainder condition  -}
 data DebugRewriteRulesRemainder = DebugRewriteRulesRemainder
     { configuration :: !(Pattern VariableName)
+    -- ^ the state the rules unified with
     , rulesCount :: !Int
+    -- ^ how many rules were unified
     , remainder :: !(Predicate RewritingVariableName)
+    -- ^ the condition not covered by the rules
     }
     deriving stock (Show)
 
@@ -81,7 +86,7 @@ instance Entry DebugRewriteRulesRemainder where
                     [ "After applying "
                     , pretty rulesCount
                     , " rewrite rules"
-                    , "there is a remainder condition: "
+                    , "there is a satisfiable remainder condition: "
                     , Pretty.group . pretty $ remainder
                     ]
                 )

kore/src/Kore/Rewrite/RewriteStep.hs

@@ -306,7 +306,6 @@ finalizeRulesParallel
                     & fmap fold
             let unifications = MultiOr.make (Conditional.withoutTerm <$> unifiedRules)
                 remainderPredicate = Remainder.remainder' unifications
-            debugRewriteRulesRemainder initial (length unifiedRules) remainderPredicate
             -- evaluate the remainder predicate to make sure it is actually satisfiable
             SMT.evalPredicate
                 (ErrorDecidePredicateUnknown $srcLoc Nothing)
@@ -316,7 +315,8 @@ finalizeRulesParallel
                     -- remainder condition is UNSAT: we prune the remainder branch early to avoid
                     -- jumping into the pit of function evaluation in the configuration under the
                     -- contradictory condition (the unsatisfiable remainder)
-                    Just False ->
+                    Just False -> do
+                        debugRewriteRulesRemainder initial (length unifiedRules) remainderPredicate
                         return
                             Step.Results
                                 { results = Seq.fromList results