From b14ad6bc6fbab4bf39526a9eaa72010447d0de3f Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 18 Dec 2025 18:23:17 +1100 Subject: [PATCH 1/4] Only check top-level symbol when deciding to skip sort predicate rules The previous fix checked `isEvaluated` on the term in a sort predicate before applying rules. This is correct but leads to too many fall-backs which slow down symbolic execution when sort predicates are used in rewrite side conditions. The only case that matters is when an _unevaluated function_ is at the _head_ of the term in the sort predicate. This is now matched directly. --- .../library/Booster/Pattern/ApplyEquations.hs | 20 ++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 6340f46e04..ead319df44 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 = + , 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 From 00993663517090bd1a04f21e9f346e6dda6e36c3 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 18 Dec 2025 20:13:04 +1100 Subject: [PATCH 2/4] update test expectation for simplification log (fewer fall-backs) --- .../simplify-log.txt.golden | 100 +++--------------- 1 file changed, 16 insertions(+), 84 deletions(-) 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..7e81723475 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,92 +37,24 @@ {"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","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"} -{"context":[{"request":"4"},"kore","execute",{"term":"8f34340"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"cd6b03f"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} -{"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"},{"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":[]}]}]}]]}} -{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} -{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"match","failure","continue"],"message":{"remainder":[[{"tag":"App","name":"Lbl'Unds-LT-Eqls'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":"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":"db347c0"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"d1b77ee"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"hook":"BOOL.not"},"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"},{"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"},"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"},{"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":[]}]}]}]]}} -{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"d0a44bc"},{"term":"e57758d"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} -{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"d0a44bc"},{"term":"e57758d"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"match","failure","continue"],"message":{"remainder":[[{"tag":"App","name":"Lbl'Unds-LT-Eqls'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"},"simplify",{"term":"d0a44bc"},{"term":"e57758d"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (23, 10)"} -{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"d0a44bc"},{"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"},"simplify",{"term":"d0a44bc"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} -{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"473c428"},{"term":"f6f99de"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"} -{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"473c428"},{"term":"f6f99de"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md : (1119, 8)"} -{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"473c428"},{"term":"f6f99de"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"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"}]}]]}} -{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"473c428"},{"term":"f6f99de"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} -{"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"} -{"context":[{"request":"4"},"kore","execute",{"term":"f349e0b"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"cd6b03f"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} -{"context":[{"request":"4"},"kore","execute",{"term":"f349e0b"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"4edf1d1"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"} -{"context":[{"request":"4"},"kore","execute",{"term":"f349e0b"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"4edf1d1"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure"],"message":"equation did not match term: distinct injections"} -{"context":[{"request":"4"},"kore","execute",{"term":"f349e0b"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"4edf1d1"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"...resources/log-simplify-json.kore:3895:7"} -{"context":[{"request":"4"},"kore","execute",{"term":"f349e0b"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"4edf1d1"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} -{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md:1119:8-1119:29"} -{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"failure"],"message":"equation did not match term: unimplemented matching case"} -{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"function":"53fc758ece1ff16581673016dfacc556cc30fcf6b3c35b586f001d76a1f9336c"},"detail"],"message":"...kframework/builtin/domains.md:1118:8-1118:29"} -{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"function":"53fc758ece1ff16581673016dfacc556cc30fcf6b3c35b586f001d76a1f9336c"},"failure"],"message":"equation did not match term: unimplemented matching case"} -{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"detail"],"message":"...include/imp-semantics/imp-verification.k:23:10-23:42"} -{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"failure"],"message":"equation did not match term: distinct application symbols: Lbl'Unds-LT-'Int'Unds'{}, Lbl'Unds-LT-Eqls'Int'Unds'{}"} -{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k:24:10-24:42"} -{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"success",{"term":"23c17d0"},"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","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","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"} -{"context":[{"request":"4"},"kore","execute",{"term":"3c8c908"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} -{"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"},{"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":[]}]}]}]]}} -{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} -{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"match","failure","continue"],"message":{"remainder":[[{"tag":"App","name":"Lbl'Unds-LT-Eqls'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"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (23, 10)"} -{"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":"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":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"} +{"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md : (1119, 8)"} +{"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"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"}]}]]}} +{"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} +{"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"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":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} +{"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":[{"request":"4"},"booster","execute",{"term":"d3dc513"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"fd81940"},{"hook":"BOOL.not"},"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":"d3dc513"},"simplify",{"term":"50120f3"},{"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"},{"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":[]}]}]}]]}} -{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} -{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"match","failure","continue"],"message":{"remainder":[[{"tag":"App","name":"Lbl'Unds-LT-Eqls'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"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (23, 10)"} -{"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"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"BOOL.not"},"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","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} {"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} {"context":[{"request":"4"},"kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"} From 8afe8e3084fded2ef7ae688f0c0abea68d1c14ef Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 19 Dec 2025 06:32:25 +1100 Subject: [PATCH 3/4] fix function head match (was missing kseq node), revert log test expectation --- .../library/Booster/Pattern/ApplyEquations.hs | 2 +- .../simplify-log.txt.golden | 100 +++++++++++++++--- 2 files changed, 85 insertions(+), 17 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index ead319df44..b5de2ece8e 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -875,7 +875,7 @@ applyEquation :: (Either ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) Term) applyEquation (FunctionApplication _sym [] [term]) rule | isSortPredicate rule - , FunctionApplication _ _ _ <- term = + , KSeq _ (FunctionApplication _ _ _) <- term = -- sort predicates only match on a sort injection, unevaluated -- function applications may create false negatives pure $ 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 7e81723475..47c0e4d519 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,24 +37,92 @@ {"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"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} -{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"hook":"BOOL.not"},"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"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure","break","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"} +{"context":[{"request":"4"},"kore","execute",{"term":"8f34340"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"cd6b03f"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"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"},{"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":[]}]}]}]]}} +{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} +{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"match","failure","continue"],"message":{"remainder":[[{"tag":"App","name":"Lbl'Unds-LT-Eqls'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":"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"},"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":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"} -{"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md : (1119, 8)"} -{"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"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"}]}]]}} -{"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} -{"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"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":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} -{"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} -{"context":[{"request":"4"},"booster","execute",{"term":"d3dc513"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"fd81940"},{"hook":"BOOL.not"},"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":"d3dc513"},"simplify",{"term":"50120f3"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} +{"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"},"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"},{"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":[]}]}]}]]}} +{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"d0a44bc"},{"term":"e57758d"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} +{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"d0a44bc"},{"term":"e57758d"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"match","failure","continue"],"message":{"remainder":[[{"tag":"App","name":"Lbl'Unds-LT-Eqls'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"},"simplify",{"term":"d0a44bc"},{"term":"e57758d"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (23, 10)"} +{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"d0a44bc"},{"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"},"simplify",{"term":"d0a44bc"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} +{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"473c428"},{"term":"f6f99de"},{"hook":"BOOL.not"},"failure"],"message":"Hook returned no result"} +{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"473c428"},{"term":"f6f99de"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md : (1119, 8)"} +{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"473c428"},{"term":"f6f99de"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"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"}]}]]}} +{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"473c428"},{"term":"f6f99de"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} +{"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"} +{"context":[{"request":"4"},"kore","execute",{"term":"f349e0b"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"cd6b03f"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":[{"request":"4"},"kore","execute",{"term":"f349e0b"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"4edf1d1"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"} +{"context":[{"request":"4"},"kore","execute",{"term":"f349e0b"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"4edf1d1"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"failure"],"message":"equation did not match term: distinct injections"} +{"context":[{"request":"4"},"kore","execute",{"term":"f349e0b"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"4edf1d1"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"...resources/log-simplify-json.kore:3895:7"} +{"context":[{"request":"4"},"kore","execute",{"term":"f349e0b"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"4edf1d1"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} +{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"detail"],"message":"...kframework/builtin/domains.md:1119:8-1119:29"} +{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"failure"],"message":"equation did not match term: unimplemented matching case"} +{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"function":"53fc758ece1ff16581673016dfacc556cc30fcf6b3c35b586f001d76a1f9336c"},"detail"],"message":"...kframework/builtin/domains.md:1118:8-1118:29"} +{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"function":"53fc758ece1ff16581673016dfacc556cc30fcf6b3c35b586f001d76a1f9336c"},"failure"],"message":"equation did not match term: unimplemented matching case"} +{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"detail"],"message":"...include/imp-semantics/imp-verification.k:23:10-23:42"} +{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"failure"],"message":"equation did not match term: distinct application symbols: Lbl'Unds-LT-'Int'Unds'{}, Lbl'Unds-LT-Eqls'Int'Unds'{}"} +{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k:24:10-24:42"} +{"context":[{"request":"4"},"kore","execute",{"term":"3672b8e"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"success",{"term":"23c17d0"},"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","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","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"} +{"context":[{"request":"4"},"kore","execute",{"term":"3c8c908"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"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"},{"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":[]}]}]}]]}} +{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} +{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"match","failure","continue"],"message":{"remainder":[[{"tag":"App","name":"Lbl'Unds-LT-Eqls'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"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (23, 10)"} +{"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"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} -{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"BOOL.not"},"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":"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"},{"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":[]}]}]}]]}} +{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} +{"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"match","failure","continue"],"message":{"remainder":[[{"tag":"App","name":"Lbl'Unds-LT-Eqls'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"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"simplification":"cb079e42f8993a0cf744fd4996fa1635f79ecc3e07cf441d3d0b743da4b9b43f"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (23, 10)"} +{"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","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} {"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} {"context":[{"request":"4"},"kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"} From 3d3bf0dae7eb9169a5ad38b9494b9181e93e6348 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 19 Dec 2025 06:33:17 +1100 Subject: [PATCH 4/4] Adjust log test expectation to new logging --- .../simplify-log.txt.golden | 26 +++++++++++-------- 1 file changed, 15 insertions(+), 11 deletions(-) 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":[]}]}]}]]}}