Try simplifying the remainder predicate before checking it with SMT

Author: geo2a

kore/src/Kore/Rewrite/RewriteStep.hs

@@ -84,6 +84,7 @@ import Kore.Simplify.Simplify (
     Simplifier,
     simplifyCondition,
  )
+import Kore.Simplify.Simplify qualified as Simplifier
 import Kore.Substitute
 import Logic (
     LogicT,
@@ -306,11 +307,22 @@ finalizeRulesParallel
                     & fmap fold
             let unifications = MultiOr.make (Conditional.withoutTerm <$> unifiedRules)
                 remainderPredicate = Remainder.remainder' unifications
-            debugRewriteRulesRemainder initial (length unifiedRules) remainderPredicate
+
+            simplifiedRemainderConditional <-
+                Logic.observeAllT $
+                    Simplifier.simplifyCondition
+                        ( sideCondition
+                            & SideCondition.addConditionWithReplacements
+                                (Pattern.withoutTerm initial)
+                        )
+                        (Condition.fromPredicate remainderPredicate)
+            let simplifiedRemainder = Remainder.remainder' $ MultiOr.make simplifiedRemainderConditional
+
+            debugRewriteRulesRemainder initial (length unifiedRules) simplifiedRemainder
             -- evaluate the remainder predicate to make sure it is actually satisfiable
             SMT.evalPredicate
                 (ErrorDecidePredicateUnknown $srcLoc Nothing)
-                remainderPredicate
+                simplifiedRemainder
                 Nothing
                 >>= \case
                     -- remainder condition is UNSAT: we prune the remainder branch early to avoid