diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs
index 6340f46e04..b5de2ece8e 100644
--- a/booster/library/Booster/Pattern/ApplyEquations.hs
+++ b/booster/library/Booster/Pattern/ApplyEquations.hs
@@ -873,18 +873,20 @@ applyEquation ::
     EquationT
         io
         (Either ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) Term)
-applyEquation (FunctionApplication _sym [] [Term term _]) rule
+applyEquation (FunctionApplication _sym [] [term]) rule
     | isSortPredicate rule
-    , not term.isEvaluated =
+    , KSeq _ (FunctionApplication _ _ _) <- term =
         -- sort predicates only match on a sort injection, unevaluated
         -- function applications may create false negatives
-        getPrettyModifiers >>= \case
-            ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> do
-                pure $
-                    Left
-                        ( \ctxt -> ctxt $ logWarn "Refusing to apply sort predicate rule to an unevaluated term"
-                        , IndeterminateMatch
-                        )
+        pure $
+            Left
+                ( \ctxt ->
+                    ctxt $
+                        withTermContext term $
+                            withContext CtxWarn $
+                                logMessage ("Refusing to apply sort predicate rule to an unevaluated term" :: Text)
+                , IndeterminateMatch
+                )
 applyEquation term rule =
     runExceptT $
         getPrettyModifiers >>= \case
diff --git a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
index 47c0e4d519..da1821699b 100644
--- a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
+++ b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
@@ -37,7 +37,8 @@
 {"context":[{"request":"4"},"booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
 {"context":[{"request":"4"},"booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
-{"context":[{"request":"4"},"booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break","warn"],"message":"Refusing to apply sort predicate rule to an unevaluated term"}
+{"context":[{"request":"4"},"booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break",{"term":"ce7b0ad"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortBool","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}}}
+{"context":[{"request":"4"},"booster","execute",{"term":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break",{"term":"ce7b0ad"},"warn"],"message":"Refusing to apply sort predicate rule to an unevaluated term"}
 {"context":[{"request":"4"},"booster","simplify",{"term":"db347c0"},{"term":"721488a"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","simplify",{"term":"db347c0"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"kore","execute",{"term":"8f34340"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"cd6b03f"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"}
@@ -45,7 +46,8 @@
 {"context":[{"request":"4"},"booster","execute","simplify",{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
-{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break","warn"],"message":"Refusing to apply sort predicate rule to an unevaluated term"}
+{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break",{"term":"ce7b0ad"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortBool","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}}}
+{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break",{"term":"ce7b0ad"},"warn"],"message":"Refusing to apply sort predicate rule to an unevaluated term"}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md :  (1119, 8)"}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"tag":"App","name":"LblisKResult","sorts":[],"args":[{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortBool","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}]}]]}}
@@ -54,11 +56,14 @@
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"detail"],"message":"...include/imp-semantics/imp-verification.k :  (23, 10)"}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"match","failure","continue"],"message":{"remainder":[[{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"Eq#VarA","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"EVar","name":"Eq#VarB","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]},{"tag":"App","name":"LblisKResult","sorts":[],"args":[{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortBool","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}]}]]}}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
-{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break","warn"],"message":"Refusing to apply sort predicate rule to an unevaluated term"}
+{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= !__EXPRESSIONS-SYNTAX_Expr_Expr(_<=Int_(VarN:SortInt{}, \"0\"))"}
+{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"}
+{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"e702940"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"3a244e5"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"d0a44bc"},{"term":"e57758d"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"d0a44bc"},{"term":"e57758d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
-{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"d0a44bc"},{"term":"e57758d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break","warn"],"message":"Refusing to apply sort predicate rule to an unevaluated term"}
+{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"d0a44bc"},{"term":"e57758d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break",{"term":"ce7b0ad"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortBool","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}}}
+{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"d0a44bc"},{"term":"e57758d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break",{"term":"ce7b0ad"},"warn"],"message":"Refusing to apply sort predicate rule to an unevaluated term"}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"d0a44bc"},{"term":"e57758d"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"d0a44bc"},{"term":"e57758d"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md :  (1119, 8)"}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"d0a44bc"},{"term":"e57758d"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"tag":"App","name":"LblisKResult","sorts":[],"args":[{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortBool","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}]}]]}}
@@ -74,10 +79,6 @@
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"473c428"},{"term":"f6f99de"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"success",{"term":"8f1e2b8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}}}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"473c428"},{"term":"f6f99de"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"473c428"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
-{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"404bc7b"},{"term":"e702940"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
-{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"404bc7b"},{"term":"e702940"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
-{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"404bc7b"},{"term":"e702940"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break","warn"],"message":"Refusing to apply sort predicate rule to an unevaluated term"}
-{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"404bc7b"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","simplify",{"term":"3a244e5"},{"term":"fdceb0b"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","simplify",{"term":"3a244e5"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"kore","execute",{"term":"f349e0b"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"cd6b03f"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"}
@@ -97,7 +98,8 @@
 {"context":[{"request":"4"},"booster","execute","simplify",{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"ac59308"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"c60c929"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"ac59308"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"c60c929"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
-{"context":[{"request":"4"},"booster","execute",{"term":"ac59308"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"c60c929"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break","warn"],"message":"Refusing to apply sort predicate rule to an unevaluated term"}
+{"context":[{"request":"4"},"booster","execute",{"term":"ac59308"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"c60c929"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break",{"term":"a5d2bf2"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortBool","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}}}
+{"context":[{"request":"4"},"booster","execute",{"term":"ac59308"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"c60c929"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break",{"term":"a5d2bf2"},"warn"],"message":"Refusing to apply sort predicate rule to an unevaluated term"}
 {"context":[{"request":"4"},"booster","simplify",{"term":"ac59308"},{"term":"2a0d146"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","simplify",{"term":"ac59308"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"kore","execute",{"term":"3c8c908"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"}
@@ -105,7 +107,8 @@
 {"context":[{"request":"4"},"booster","execute","simplify",{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
-{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break","warn"],"message":"Refusing to apply sort predicate rule to an unevaluated term"}
+{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break",{"term":"a5d2bf2"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortBool","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}}}
+{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break",{"term":"a5d2bf2"},"warn"],"message":"Refusing to apply sort predicate rule to an unevaluated term"}
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md :  (1119, 8)"}
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"tag":"App","name":"LblisKResult","sorts":[],"args":[{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortBool","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}]}]]}}
@@ -115,7 +118,8 @@
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"match","failure","continue"],"message":{"remainder":[[{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"Eq#VarA","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"EVar","name":"Eq#VarB","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]},{"tag":"App","name":"LblisKResult","sorts":[],"args":[{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortBool","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}]}]]}}
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},"simplify",{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
-{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break","warn"],"message":"Refusing to apply sort predicate rule to an unevaluated term"}
+{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break",{"term":"a5d2bf2"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortBool","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}}}
+{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break",{"term":"a5d2bf2"},"warn"],"message":"Refusing to apply sort predicate rule to an unevaluated term"}
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md :  (1119, 8)"}
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"tag":"App","name":"LblisKResult","sorts":[],"args":[{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortBool","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}]}]]}}