From 1026e9b516357657ee0c2bf0f4d0bc4a88479313 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 29 Jan 2026 11:19:27 +1100 Subject: [PATCH 1/5] WIP changed matcher code to prefer indeterminate function case, remove sort predicate bail-out --- .../library/Booster/Pattern/ApplyEquations.hs | 35 ----------- booster/library/Booster/Pattern/Match.hs | 18 +++--- .../simplify-log.txt.golden | 62 +++++-------------- 3 files changed, 24 insertions(+), 91 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index b5de2ece8e..df4f6280c4 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -844,27 +844,6 @@ applyEquations theory handler term = do ) err -{- | A sort predicate equation is characterised by the following: - * Its lhs is a function application (of a symbol starting with 'Lblis', not checked) - * function argument is a singleton K sequence - * containing an injection of a Variable into the 'KItem' sort - * rhs is a boolean - * requires and ensures are both empty (i.e., plain "true" DVs) - * the rule has no location information --} -isSortPredicate :: RewriteRule tag -> Bool -isSortPredicate rule - | SymbolApplication _funSym [] [arg] <- rule.lhs - , KSeq sort (Var v) <- arg -- implicitly: Injection sort KItem (Var v) - , v.variableSort == sort - , (rule.rhs == TrueBool || rule.rhs == FalseBool) - , [Predicate TrueBool] <- rule.requires -- , null rule.requires - , [Predicate TrueBool] <- rule.ensures -- , null rule.ensures - , UNKNOWN <- sourceRef rule.attributes = - True - | otherwise = - False - applyEquation :: forall io tag. LoggerMIO io => @@ -873,20 +852,6 @@ applyEquation :: EquationT io (Either ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) Term) -applyEquation (FunctionApplication _sym [] [term]) rule - | isSortPredicate rule - , KSeq _ (FunctionApplication _ _ _) <- term = - -- sort predicates only match on a sort injection, unevaluated - -- function applications may create false negatives - pure $ - Left - ( \ctxt -> - ctxt $ - withTermContext term $ - withContext CtxWarn $ - logMessage ("Refusing to apply sort predicate rule to an unevaluated term" :: Text) - , IndeterminateMatch - ) applyEquation term rule = runExceptT $ getPrettyModifiers >>= \case diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index cff7abacb5..9892a5f6df 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -341,15 +341,6 @@ matchInj failWith (DifferentSorts (Injection source1 target1 trm1) (Injection source2 target2 trm2)) | source1 == source2 = do enqueueRegularProblem trm1 trm2 - | Var v <- trm1 = do - -- variable in pattern, check source sorts and bind - subsorts <- gets mSubsorts - isSubsort <- - lift . withExcept (MatchFailed . SubsortingError) $ - checkSubsort subsorts source2 source1 - if isSubsort - then bindVariable matchType v (Injection source2 source1 trm2) - else failWith (DifferentSorts trm1 trm2) | FunctionApplication{} <- trm2 = do -- Functions may have a more general sort than the actual result. -- This means we cannot simply fail the rewrite: the match is @@ -361,6 +352,15 @@ matchInj if isSubsort then addIndeterminate trm1 trm2 else failWith (DifferentSorts (Injection source1 target1 trm1) (Injection source2 target2 trm2)) + | Var v <- trm1 = do + -- variable in pattern, check source sorts and bind + subsorts <- gets mSubsorts + isSubsort <- + lift . withExcept (MatchFailed . SubsortingError) $ + checkSubsort subsorts source2 source1 + if isSubsort + then bindVariable matchType v (Injection source2 source1 trm2) + else failWith (DifferentSorts trm1 trm2) | otherwise = failWith (DifferentSorts (Injection source1 target1 trm1) (Injection source2 target2 trm2)) {-# INLINE matchInj #-} 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 da1821699b..115eeffe63 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 @@ -35,10 +35,7 @@ {"context":[{"request":"4"},"booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= _<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(VarN:SortInt{}, \"0\")"} {"context":[{"request":"4"},"booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} {"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",{"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","execute",{"term":"db347c0"},"simplify",{"term":"721488a"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} {"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"} @@ -46,32 +43,16 @@ {"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",{"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":[]}]}]}]]}} -{"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":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= _<=Int_(VarN:SortInt{}, \"0\")"} +{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} +{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"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"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"hook":"BOOL.not"},"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":"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":"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",{"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":[]}]}]}]]}} -{"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":"db347c0"},{"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"}]}]]}} @@ -96,10 +77,7 @@ {"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",{"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","execute",{"term":"ac59308"},"simplify",{"term":"2a0d146"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} {"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"} @@ -107,26 +85,16 @@ {"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",{"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":[]}]}]}]]}} -{"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"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= _ Date: Thu, 29 Jan 2026 11:19:45 +1100 Subject: [PATCH 2/5] Bump K version dependency --- deps/k_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/k_release b/deps/k_release index 65a488eaa8..3d3a2dd674 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.1.300 +7.1.311 From 76ebbdbe61cd3405b7bc84db8db259325fcf1019 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 29 Jan 2026 15:51:07 +1100 Subject: [PATCH 3/5] WIP reorganise matching code --- booster/library/Booster/Pattern/Match.hs | 50 +++++++++++++++--------- 1 file changed, 32 insertions(+), 18 deletions(-) diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index 9892a5f6df..e6e1537ef6 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -330,7 +330,7 @@ matchInj :: Term -> StateT MatchState (Except MatchResult) () matchInj - matchType + _matchType source1 target1 trm1 @@ -341,28 +341,42 @@ matchInj failWith (DifferentSorts (Injection source1 target1 trm1) (Injection source2 target2 trm2)) | source1 == source2 = do enqueueRegularProblem trm1 trm2 - | FunctionApplication{} <- trm2 = do - -- Functions may have a more general sort than the actual result. - -- This means we cannot simply fail the rewrite: the match is - -- indeterminate if the function result is. +matchInj + matchType + source1 + target1 + trm1 + source2 + target2 + trm2 = + do subsorts <- gets mSubsorts - isSubsort <- -- rule requires a more specific sort? + s1IsSubsort <- lift . withExcept (MatchFailed . SubsortingError) $ checkSubsort subsorts source1 source2 - if isSubsort - then addIndeterminate trm1 trm2 - else failWith (DifferentSorts (Injection source1 target1 trm1) (Injection source2 target2 trm2)) - | Var v <- trm1 = do - -- variable in pattern, check source sorts and bind - subsorts <- gets mSubsorts - isSubsort <- + s2IsSubsort <- lift . withExcept (MatchFailed . SubsortingError) $ checkSubsort subsorts source2 source1 - if isSubsort - then bindVariable matchType v (Injection source2 source1 trm2) - else failWith (DifferentSorts trm1 trm2) - | otherwise = - failWith (DifferentSorts (Injection source1 target1 trm1) (Injection source2 target2 trm2)) + -- cases below, checking subsorting is as expected, too + + -- Functions may have a more general sort than the actual result. + -- This means we cannot simply fail the rewrite: the match is + -- indeterminate if the function result is. + case (s1IsSubsort, trm2) of + (True, FunctionApplication{}) -> + addIndeterminate trm1 trm2 + _ -> do + -- If the rule has a variable with a supersort of the + -- subject, trm2 can be bound with a suitable injection + case (s2IsSubsort, trm1) of + (True, Var v) -> + bindVariable matchType v (Injection source2 source1 trm2) + _ -> + -- truly different sorts, safe to just fail + failWith $ + DifferentSorts + (Injection source1 target1 trm1) + (Injection source2 target2 trm2) {-# INLINE matchInj #-} ----- Symbol Applications From 8d8710ecfaa920b2f30f0f11d8a5391f8506f9d7 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 29 Jan 2026 18:56:00 +1100 Subject: [PATCH 4/5] add a short-cut case for unrelated sorts --- booster/library/Booster/Pattern/Match.hs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index e6e1537ef6..67580f96d4 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -357,8 +357,10 @@ matchInj s2IsSubsort <- lift . withExcept (MatchFailed . SubsortingError) $ checkSubsort subsorts source2 source1 - -- cases below, checking subsorting is as expected, too - + -- cases below require a subsort relation (and source1 == + -- source2 is already handled) + unless (s1IsSubsort || s2IsSubsort) $ + failWith (DifferentSorts trm1 trm2) -- Functions may have a more general sort than the actual result. -- This means we cannot simply fail the rewrite: the match is -- indeterminate if the function result is. From 01737488536616e3c7186dd7f7973431238749f9 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 29 Jan 2026 19:10:53 +1100 Subject: [PATCH 5/5] adjust golden simplify-log (again) --- .../simplify-log.txt.golden | 70 ++++--------------- 1 file changed, 15 insertions(+), 55 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 115eeffe63..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 @@ -35,66 +35,26 @@ {"context":[{"request":"4"},"booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= _<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(VarN:SortInt{}, \"0\")"} {"context":[{"request":"4"},"booster","execute",{"term":"9893c04"},{"rewrite":"28f395c2f029144cab225e78d4bc6d7d6c54b12b2b14d0f806934911bc8ed0d1"},"constraint",{"term":"2cedcc8"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} {"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"},"simplify",{"term":"721488a"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} -{"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"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= _<=Int_(VarN:SortInt{}, \"0\")"} -{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"} -{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"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"},{"rewrite":"95ae0624ed05bd9fda100afe3522e14997852a9753240caa90be72f16a32414f"},"constraint",{"term":"e57758d"},{"hook":"BOOL.not"},"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":"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":"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":"3a244e5"},"simplify",{"term":"3a244e5"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} -{"context":[{"request":"4"},"booster","execute",{"term":"3a244e5"},"simplify",{"term":"db347c0"},{"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","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"},"simplify",{"term":"2a0d146"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} -{"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"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= _