diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 1648de042e..9cfd55f9b9 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -114,7 +114,7 @@ jobs: stack-2-${{ runner.os }}-ghc-${{ env.ghc_version }}-${{ hashFiles('stack.yaml') }} stack-2-${{ runner.os }}-ghc-${{ env.ghc_version }} - - uses: haskell/actions/setup@v2 + - uses: haskell-actions/setup@v2 id: setup-haskell-stack with: ghc-version: ${{ env.ghc_version }} @@ -148,7 +148,7 @@ jobs: stack-haddock-2-${{ runner.os }}-ghc-${{ env.ghc_version }}-${{ hashFiles('stack.yaml') }} stack-haddock-2-${{ runner.os }}-ghc-${{ env.ghc_version }} - - uses: haskell/actions/setup@v2 + - uses: haskell-actions/setup@v2 id: setup-haskell-stack with: ghc-version: ${{ env.ghc_version }} diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 61eeaa8432..fe42aa485c 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -183,7 +183,7 @@ jobs: stack-2-${{ runner.os }}-ghc-${{ env.ghc_version }}-${{ hashFiles('stack.yaml') }} stack-2-${{ runner.os }}-ghc-${{ env.ghc_version }} - - uses: haskell/actions/setup@v2 + - uses: haskell-actions/setup@v2 id: setup-haskell-stack with: ghc-version: ${{ env.ghc_version }} diff --git a/deps/k_release b/deps/k_release index 01dc08c911..f8d93b0c69 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -6.0.181 +6.2.27 diff --git a/test/issue-1665/test.k b/test/issue-1665/test.k index 600543644c..3cd97fa55e 100644 --- a/test/issue-1665/test.k +++ b/test/issue-1665/test.k @@ -3,7 +3,7 @@ module TEST-SYNTAX syntax Pgm ::= "begin" Int | "end" Int syntax Int ::= fun(Int) [function, no-evaluators] - syntax Bool ::= isFun(Int) [function, functional, no-evaluators] + syntax Bool ::= isFun(Int) [function, total, no-evaluators] endmodule @@ -14,6 +14,6 @@ module TEST rule begin X => end fun(X) - rule [ceil-fun]: #Ceil(fun(X:Int)) => #True requires isFun(X) [simplification] + rule [ceil-fun]: #Ceil(fun(X:Int)) => #Top requires isFun(X) [simplification] endmodule diff --git a/test/issue-1916/test.k b/test/issue-1916/test.k index 1cc3e33904..91235315bd 100644 --- a/test/issue-1916/test.k +++ b/test/issue-1916/test.k @@ -5,7 +5,7 @@ module TEST-SYNTAX syntax Pgm ::= "begin" | "end" syntax Int ::= fun(Int) [function, no-evaluators] - syntax Bool ::= isFun(Int) [function, functional, no-evaluators] + syntax Bool ::= isFun(Int) [function, total, no-evaluators] endmodule @@ -16,6 +16,6 @@ module TEST rule begin => end - rule [ceil-fun]: #Ceil(fun(X:Int)) => #True requires isFun(X) [simplification] + rule [ceil-fun]: #Ceil(fun(X:Int)) => #Top requires isFun(X) [simplification] endmodule diff --git a/test/issue-2378/test-spec.k.out.golden b/test/issue-2378/test-spec.k.out.golden index 3977e9dea4..eb9218e160 100644 --- a/test/issue-2378/test-spec.k.out.golden +++ b/test/issue-2378/test-spec.k.out.golden @@ -1,16 +1 @@ - #Not ( #Exists _Gen0 . #Exists S . { - keys ( _M ) - #Equals - S - SetItem ( _Gen0 ) - } ) -#And - #Not ( { - .Set - #Equals - keys ( _M ) - } ) -#And - - b ( keys ( _M ) ) ~> _DotVar1 ~> . - +b ( keys ( _M ) ) diff --git a/test/map/map-iteration/test-1-spec.k b/test/map/map-iteration/test-1-spec.k index 9d67669800..493fcb2b88 100644 --- a/test/map/map-iteration/test-1-spec.k +++ b/test/map/map-iteration/test-1-spec.k @@ -3,7 +3,6 @@ requires "test.k" module TEST-1-SPEC imports TEST - claim runTest( f( a |-> 1 b |-> 2 ) ) => doneTest( b |-> 2 c |-> 3 ) + claim runTest( f( a |-> 1 b |-> 2 ) ) => doneTest( b |-> 2 c |-> 3 ) endmodule - diff --git a/test/overloads/simple-lists/broken-spec.k.out.golden b/test/overloads/simple-lists/broken-spec.k.out.golden index a73cfee30f..5a3ed37c93 100644 --- a/test/overloads/simple-lists/broken-spec.k.out.golden +++ b/test/overloads/simple-lists/broken-spec.k.out.golden @@ -1,3 +1 @@ - - i1 i2 .EmptyStmts ~> _DotVar1 ~> . - +i1 i2 .EmptyStmts diff --git a/test/regression-evm/test-dsvalue-peek-pass-rough.sh b/test/regression-evm/test-dsvalue-peek-pass-rough.sh index bb0a2b2240..26c56371e4 100755 --- a/test/regression-evm/test-dsvalue-peek-pass-rough.sh +++ b/test/regression-evm/test-dsvalue-peek-pass-rough.sh @@ -13,8 +13,6 @@ exec kore-exec \ --log-level \ warning \ --enable-log-timestamps \ - --log-entries \ - DebugTransition \ --prove test-dsvalue-peek-pass-rough-spec.kore \ --spec-module DSVALUE-PEEK-PASS-ROUGH-SPEC \ --graph-search breadth-first \ diff --git a/test/regression-evm/test-flipper-addu48u48-fail-rough.sh b/test/regression-evm/test-flipper-addu48u48-fail-rough.sh index 62971c1481..f017b002df 100755 --- a/test/regression-evm/test-flipper-addu48u48-fail-rough.sh +++ b/test/regression-evm/test-flipper-addu48u48-fail-rough.sh @@ -13,8 +13,6 @@ exec kore-exec \ --log-level \ warning \ --enable-log-timestamps \ - --log-entries \ - DebugTransition \ --prove test-flipper-addu48u48-fail-rough-spec.kore \ --spec-module FLIPPER-ADDU48U48-FAIL-ROUGH-SPEC \ --graph-search breadth-first \ diff --git a/test/regression-evm/test-functional.sh b/test/regression-evm/test-functional.sh index 7591ca45e3..c2ab40fe73 100755 --- a/test/regression-evm/test-functional.sh +++ b/test/regression-evm/test-functional.sh @@ -13,8 +13,6 @@ exec kore-exec \ --log-level \ warning \ --enable-log-timestamps \ - --log-entries \ - DebugTransition \ --prove test-functional-spec.kore \ --spec-module FUNCTIONAL-SPEC \ --graph-search breadth-first \ diff --git a/test/regression-evm/test-lemmas.sh b/test/regression-evm/test-lemmas.sh index 238cf66ac6..dd7cde2765 100755 --- a/test/regression-evm/test-lemmas.sh +++ b/test/regression-evm/test-lemmas.sh @@ -13,8 +13,6 @@ exec kore-exec \ --log-level \ warning \ --enable-log-timestamps \ - --log-entries \ - DebugTransition \ --prove test-lemmas-spec.kore \ --spec-module LEMMAS-SPEC \ --graph-search breadth-first \ diff --git a/test/regression-evm/test-storagevar03.sh b/test/regression-evm/test-storagevar03.sh index e3a193832a..4c8099284f 100755 --- a/test/regression-evm/test-storagevar03.sh +++ b/test/regression-evm/test-storagevar03.sh @@ -13,8 +13,6 @@ exec kore-exec \ --log-level \ warning \ --enable-log-timestamps \ - --log-entries \ - DebugTransition \ --prove test-storagevar03-spec.kore \ --spec-module STORAGEVAR03-SPEC \ --graph-search breadth-first \ diff --git a/test/regression-evm/test-sum-to-n.sh b/test/regression-evm/test-sum-to-n.sh index d44ade0f58..fd3ee12677 100755 --- a/test/regression-evm/test-sum-to-n.sh +++ b/test/regression-evm/test-sum-to-n.sh @@ -13,8 +13,6 @@ exec kore-exec \ --log-level \ warning \ --enable-log-timestamps \ - --log-entries \ - DebugTransition \ --prove test-sum-to-n-spec.kore \ --spec-module SUM-TO-N-SPEC \ --graph-search breadth-first \ diff --git a/test/regression-evm/test-totalSupply.sh b/test/regression-evm/test-totalSupply.sh index c4c74a9586..9b1ceec15e 100755 --- a/test/regression-evm/test-totalSupply.sh +++ b/test/regression-evm/test-totalSupply.sh @@ -13,8 +13,6 @@ exec kore-exec \ --log-level \ warning \ --enable-log-timestamps \ - --log-entries \ - DebugTransition \ --prove test-totalSupply-spec.kore \ --spec-module TOTALSUPPLY-SPEC \ --graph-search breadth-first \ diff --git a/test/remove-destination/test-1-spec.k.out.golden b/test/remove-destination/test-1-spec.k.out.golden index e07f653255..307398e062 100644 --- a/test/remove-destination/test-1-spec.k.out.golden +++ b/test/remove-destination/test-1-spec.k.out.golden @@ -34,10 +34,8 @@ 4 } ) #And - - a ( K:Int |-> V:Int - M ) ~> _DotVar1 ~> . - + a ( K:Int |-> V:Int + M ) #And { false diff --git a/test/save-proofs/test-1-spec.k b/test/save-proofs/test-1-spec.k index 8edf541f9e..bc70a3a2a5 100644 --- a/test/save-proofs/test-1-spec.k +++ b/test/save-proofs/test-1-spec.k @@ -4,5 +4,5 @@ requires "save-proofs.k" module TEST-1-SPEC imports SAVE-PROOFS - claim BB(X:Int) => CC(X:Int) + claim BB(X:Int) => CC(X:Int) endmodule diff --git a/test/save-proofs/test-1-spec.k.save-proofs.kore.golden b/test/save-proofs/test-1-spec.k.save-proofs.kore.golden index f3e2190654..c2f11f1329 100644 --- a/test/save-proofs/test-1-spec.k.save-proofs.kore.golden +++ b/test/save-proofs/test-1-spec.k.save-proofs.kore.golden @@ -17,33 +17,37 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d LblBB'LParUndsRParUnds'SAVE-PROOFS'Unds'KItem'Unds'Int{}( /* T Fn D Sfa */ VarX:SortInt{} ), - /* T Fn D Sfa */ Var'Unds'DotVar1:SortK{} + /* T Fn D Sfa Cl */ dotk{}() ) ), /* T Fn D Spa */ Lbl'-LT-'generatedCounter'-GT-'{}( - /* T Fn D Sfa */ Var'Unds'DotVar2:SortInt{} + /* T Fn D Sfa */ Var'Unds'Gen0:SortInt{} ) ) ), /* Spa */ weakAlwaysFinally{SortGeneratedTopCell{}}( - /* T Fn D Spa */ - Lbl'-LT-'generatedTop'-GT-'{}( + /* Spa */ + \exists{SortGeneratedTopCell{}}( + Var'QuesUnds'Gen1:SortInt{}, /* T Fn D Spa */ - Lbl'-LT-'k'-GT-'{}( + Lbl'-LT-'generatedTop'-GT-'{}( /* T Fn D Spa */ - kseq{}( + Lbl'-LT-'k'-GT-'{}( /* T Fn D Spa */ - LblCC'LParUndsRParUnds'SAVE-PROOFS'Unds'KItem'Unds'Int{}( - /* T Fn D Sfa */ VarX:SortInt{} - ), - /* T Fn D Sfa */ Var'Unds'DotVar1:SortK{} + kseq{}( + /* T Fn D Spa */ + LblCC'LParUndsRParUnds'SAVE-PROOFS'Unds'KItem'Unds'Int{}( + /* T Fn D Sfa */ VarX:SortInt{} + ), + /* T Fn D Sfa Cl */ dotk{}() + ) + ), + /* T Fn D Spa */ + Lbl'-LT-'generatedCounter'-GT-'{}( + /* T Fn D Sfa */ Var'QuesUnds'Gen1:SortInt{} ) - ), - /* T Fn D Spa */ - Lbl'-LT-'generatedCounter'-GT-'{}( - /* T Fn D Sfa */ Var'Unds'DotVar2:SortInt{} ) ) ) diff --git a/test/save-proofs/test-2-spec.k b/test/save-proofs/test-2-spec.k index 3f8bf4ae17..531eb93188 100644 --- a/test/save-proofs/test-2-spec.k +++ b/test/save-proofs/test-2-spec.k @@ -7,7 +7,7 @@ module TEST-2-SPEC imports SAVE-PROOFS // This claim would fail, but it is loaded from the saved claims. - claim BB(X:Int) => CC(X:Int) + claim BB(X:Int) => CC(X:Int) // This claim requires the first claim. - claim AA(X:Int) => DD(X:Int) + claim AA(X:Int) => DD(X:Int) endmodule diff --git a/test/set/set-iteration/test-1-spec.k b/test/set/set-iteration/test-1-spec.k index aa60c34347..52a1676bd0 100644 --- a/test/set/set-iteration/test-1-spec.k +++ b/test/set/set-iteration/test-1-spec.k @@ -3,7 +3,7 @@ requires "test.k" module TEST-1-SPEC imports TEST - claim runTest( f( SetItem(a) SetItem(b) ) ) - => doneTest( SetItem(b) SetItem(c) ) + claim runTest( f( SetItem(a) SetItem(b) ) ) + => doneTest( SetItem(b) SetItem(c) ) endmodule diff --git a/test/set/set-iteration/test-2-spec.k b/test/set/set-iteration/test-2-spec.k index d0383ae15a..488ed5e54b 100644 --- a/test/set/set-iteration/test-2-spec.k +++ b/test/set/set-iteration/test-2-spec.k @@ -3,8 +3,8 @@ requires "test.k" module TEST-2-SPEC imports TEST - claim runTest( f( SetItem(X:Element) SetItem(Y:Element) ) ) - => doneTest( SetItem(g(X)) SetItem(g(Y)) ) + claim runTest( f( SetItem(X:Element) SetItem(Y:Element) ) ) + => doneTest( SetItem(g(X)) SetItem(g(Y)) ) requires (X =/=K Y) andBool (g(X) =/=K g(Y)) diff --git a/test/set/set-iteration/test.k b/test/set/set-iteration/test.k index a541083c01..93f432db9f 100644 --- a/test/set/set-iteration/test.k +++ b/test/set/set-iteration/test.k @@ -7,13 +7,13 @@ module TEST syntax Element ::= "a" | "b" | "c" - syntax Element ::= g(Element) [function, functional] + syntax Element ::= g(Element) [function, total] rule g(a) => b rule g(b) => c rule g(c) => a - syntax Set ::= f(Set) [function, functional] + syntax Set ::= f(Set) [function, total] rule f(.Set) => .Set rule f(SetItem(E:Element) S:Set) => SetItem(g(E)) f(S) diff --git a/test/simplification/Makefile b/test/simplification/Makefile index 1130bc2e5f..3c90844db8 100644 --- a/test/simplification/Makefile +++ b/test/simplification/Makefile @@ -1,10 +1,12 @@ DEF = simplification include $(CURDIR)/../include.mk +.PHONY: a-spec.k.out + a-spec.k.out: KORE_EXEC_OPTS = --debug-attempt-equation=SIMPLIFICATION.f.positive a-spec.k.out: a-spec.k simplification.k $(TEST_DEPS) @echo ">>>" $(CURDIR) "kprove" $< rm -f $@ $(KPROVE) $(KPROVE_OPTS) $(KPROVE_SPEC) 1> /dev/null 2> $@ || true - grep -q "equation is not applicable" $@ || mv $@ $@.fail + grep -q "equation is not applicable" $@ && rm $@ || mv $@ $@.fail diff --git a/test/simplification/a-spec.k.out.golden b/test/simplification/a-spec.k.out.golden index 52d89dc625..e69de29bb2 100644 --- a/test/simplification/a-spec.k.out.golden +++ b/test/simplification/a-spec.k.out.golden @@ -1,1994 +0,0 @@ -kore-exec: [191335] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ RuleVarX:SortInt{} - ) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [194889] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ RuleVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* D Sfa */ \top{_}() - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ RuleVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [200565] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ RuleVarX:SortInt{} - ) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [202710] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ RuleVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Spa */ - \equals{SortGeneratedCounterCell{}, _}( - /* T Fn D Sfa */ - RuleVar'Unds'DotVar0:SortGeneratedCounterCell{}, - /* T Fn D Sfa */ - Lbl'-LT-'generatedCounter'-GT-'{}( - /* Created: Kore.Rewrite.Rule.Expand.maybeNewVariable */ - /* T Fn D Sfa */ - RuleVar'Unds'DotVar1:SortInt{} - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ RuleVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [209093] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ RuleVarX:SortInt{} - ) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [211356] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ RuleVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Spc */ - \and{_}( - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ RuleVarX:SortInt{} - ) - ), - /* Spa */ - \equals{SortGeneratedCounterCell{}, _}( - /* T Fn D Sfa */ - RuleVar'Unds'DotVar0:SortGeneratedCounterCell{}, - /* T Fn D Sfa */ - Lbl'-LT-'generatedCounter'-GT-'{}( - /* Created: Kore.Rewrite.Rule.Expand.maybeNewVariable */ - /* T Fn D Sfa */ - RuleVar'Unds'DotVar1:SortInt{} - ) - ) - ) - TermLike replacements: - Predicate replacements: - Key: - /* Spa */ - \equals{SortGeneratedCounterCell{}, _}( - /* T Fn D Sfa */ - RuleVar'Unds'DotVar0:SortGeneratedCounterCell{}, - /* T Fn D Sfa */ - Lbl'-LT-'generatedCounter'-GT-'{}( - /* Created: Kore.Rewrite.Rule.Expand.maybeNewVariable */ - /* T Fn D Sfa */ - RuleVar'Unds'DotVar1:SortInt{} - ) - ) - Value: - /* D Sfa */ \top{_}() - Key: - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ RuleVarX:SortInt{} - ) - ) - Value: - /* D Sfa */ \top{_}() - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ RuleVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [220296] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ RuleVarX:SortInt{} - ) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [222376] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ RuleVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* D Sfa */ \top{_}() - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ RuleVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [227900] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while simplifying the claim - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [230257] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* D Sfa */ \top{_}() - TermLike replacements: - Predicate replacements: - Assumed to be defined: - /* Fn Spa */ - /* Inj: */ inj{SortS{}, SortKItem{}}( - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while simplifying the claim -kore-exec: [235962] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while simplifying the claim - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [238376] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - TermLike replacements: - Predicate replacements: - Key: - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - Value: - /* D Sfa */ \top{_}() - Assumed to be defined: - /* Fn Spa */ - /* Inj: */ inj{SortS{}, SortKItem{}}( - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while simplifying the claim -kore-exec: [246232] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [248495] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* D Sfa */ \top{_}() - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [253953] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [256380] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Sfc */ - \not{_}( - /* Sfc */ - \equals{SortS{}, _}( - /* T Fn D Sfa Cl */ Lbla'Unds'SIMPLIFICATION'Unds'S{}(), - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [262765] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [265085] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [270526] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [273200] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Spu */ - \and{_}( - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ), - /* Spc */ - \not{_}( - /* Sfc */ - \equals{SortS{}, _}( - /* T Fn D Sfa Cl */ Lbla'Unds'SIMPLIFICATION'Unds'S{}(), - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - ) - ) - TermLike replacements: - Predicate replacements: - Key: - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - Value: - /* D Sfa */ \top{_}() - Key: - /* Sfc */ - \equals{SortS{}, _}( - /* T Fn D Sfa Cl */ Lbla'Unds'SIMPLIFICATION'Unds'S{}(), - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - Value: - /* Fn Sfa */ \bottom{_}() - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [282243] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [284432] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* D Sfa */ \top{_}() - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [289425] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [292185] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Spc */ - \not{_}( - /* Sfc */ - \equals{SortS{}, _}( - /* T Fn D Sfa Cl */ Lbla'Unds'SIMPLIFICATION'Unds'S{}(), - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [298026] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [300704] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [306360] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [308580] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* D Sfa */ \top{_}() - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [313513] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [315819] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Spc */ - \not{_}( - /* Sfc */ - \equals{SortS{}, _}( - /* T Fn D Sfa Cl */ Lbla'Unds'SIMPLIFICATION'Unds'S{}(), - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [321643] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [324315] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [329887] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [332087] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* D Sfa */ \top{_}() - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [336984] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [339520] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Spc */ - \not{_}( - /* Sfc */ - \equals{SortS{}, _}( - /* T Fn D Sfa Cl */ Lbla'Unds'SIMPLIFICATION'Unds'S{}(), - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [345421] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [348022] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [354131] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [356395] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* D Sfa */ \top{_}() - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [361560] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [363839] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Spc */ - \not{_}( - /* Sfc */ - \equals{SortS{}, _}( - /* T Fn D Sfa Cl */ Lbla'Unds'SIMPLIFICATION'Unds'S{}(), - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [369624] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [371862] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [377842] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [380201] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Spu */ - \and{_}( - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ), - /* Spc */ - \not{_}( - /* Sfc */ - \equals{SortS{}, _}( - /* T Fn D Sfa Cl */ Lbla'Unds'SIMPLIFICATION'Unds'S{}(), - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - ) - ) - TermLike replacements: - Predicate replacements: - Key: - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - Value: - /* D Sfa */ \top{_}() - Key: - /* Sfc */ - \equals{SortS{}, _}( - /* T Fn D Sfa Cl */ Lbla'Unds'SIMPLIFICATION'Unds'S{}(), - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - Value: - /* Fn Sfa */ \bottom{_}() - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [389001] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [391254] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* D Sfa */ \top{_}() - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [396146] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [398575] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Spc */ - \not{_}( - /* Sfc */ - \equals{SortS{}, _}( - /* T Fn D Sfa Cl */ Lbla'Unds'SIMPLIFICATION'Unds'S{}(), - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [404334] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [406691] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [412531] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [414786] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* D Sfa */ \top{_}() - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [419692] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [421969] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Spc */ - \not{_}( - /* Sfc */ - \equals{SortS{}, _}( - /* T Fn D Sfa Cl */ Lbla'Unds'SIMPLIFICATION'Unds'S{}(), - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [427797] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [429999] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [435446] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [437558] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* D Sfa */ \top{_}() - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [442404] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [444636] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Spc */ - \not{_}( - /* Sfc */ - \equals{SortS{}, _}( - /* T Fn D Sfa Cl */ Lbla'Unds'SIMPLIFICATION'Unds'S{}(), - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [450325] Debug (DebugAttemptEquation): - applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 to term: - /* Fn Spa */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) -Context: - (InfoReachability) while checking the implication - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 -kore-exec: [452579] Debug (DebugAttemptEquation): - equation is not applicable: - Could not infer the equation requirement: - /* Spa */ - \equals{SortBool{}, _}( - /* T Fn D Spa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ), - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") - ) - and the matching requirement: - /* D Sfa */ \top{_}() - from the side condition: - Assumed true condition: - /* Sfc */ - \ceil{SortS{}, _}( - /* Fn Sfc */ - Lblf'LParUndsRParUnds'SIMPLIFICATION'Unds'S'Unds'Int{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{} - ) - ) - TermLike replacements: - Predicate replacements: - Assumed to be defined: - The negated implication is: - \and( - /* term: */ - /* D Sfa */ \top{_}(), - \and( - /* predicate: */ - /* Sfa */ - \not{_}( - /* Sfa */ - \equals{SortBool{}, _}( - /* T Fn D Sfa Cl */ \dv{SortBool{}}("true"), - /* T Fn D Sfa */ - Lbl'Unds-GT-'Int'Unds'{}( - /* T Fn D Sfa */ ConfigVarX:SortInt{}, - /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") - ) - ) - ), - /* substitution: */ - \top() - )) -Context: - (DebugAttemptEquation) while applying equation (label: SIMPLIFICATION.f.positive ) at /home/alexey/Projects/RV/haskell-backend/test/simplification/simplification.k:9:24-9:55 - (InfoReachability) while checking the implication -kore-exec: [458566] Warning (WarnStuckClaimState): - The configuration's term unifies with the destination's term, but the implication check between the conditions has failed. Location: /home/alexey/Projects/RV/haskell-backend/test/simplification/a-spec.k:7:11-7:33 -Context: - (InfoReachability) while checking the implication -[Warning] Compiler: Variable 'X' defined but not used. Prefix variable name -with underscore if this is intentional. - Source(/home/alexey/Projects/RV/haskell-backend/test/simplification/a-spec.k) - Location(7,17,7,18) - 7 | claim f(X:Int) => a - . ^ -[Error] Prover: backend terminated because the configuration cannot be -rewritten further. See output for more details. diff --git a/test/simplify-rhs/test-1-repl-script-spec.k.out.golden b/test/simplify-rhs/test-1-repl-script-spec.k.out.golden index df6dbcaab8..c9da86dd1f 100644 --- a/test/simplify-rhs/test-1-repl-script-spec.k.out.golden +++ b/test/simplify-rhs/test-1-repl-script-spec.k.out.golden @@ -1,8 +1,4 @@ Kore (0)> ProveSteps 1 - - evaluated ~> _DotVar1 ~> . - + a #Implies - #wAF ( - evaluated ~> _DotVar1 ~> . - ) + #wAF ( evaluated ) diff --git a/test/tiny/a-to-c-spec.k b/test/tiny/a-to-c-spec.k index 7904470b83..8f0a7acef2 100644 --- a/test/tiny/a-to-c-spec.k +++ b/test/tiny/a-to-c-spec.k @@ -3,6 +3,6 @@ requires "tiny.k" module A-TO-C-SPEC imports TINY - claim a => c + claim a => c endmodule diff --git a/test/tiny/mixed-claims-spec.k b/test/tiny/mixed-claims-spec.k index 4bab82ad71..38f215b563 100644 --- a/test/tiny/mixed-claims-spec.k +++ b/test/tiny/mixed-claims-spec.k @@ -4,8 +4,8 @@ module MIXED-CLAIMS-SPEC imports TINY imports TINY - claim b => d [one-path] + claim b => d [one-path] - claim a => d [all-path] + claim a => d [all-path] endmodule diff --git a/test/unification2/test-spec.k b/test/unification2/test-spec.k index 23f7f60d4b..8655d6de98 100644 --- a/test/unification2/test-spec.k +++ b/test/unification2/test-spec.k @@ -1,5 +1,5 @@ module TEST-SPEC imports TEST - claim (mapLookup(address(X), address(X) |-> u(_) M:Map) => ?_:Maybe) ~> M:Map ~> _:K + claim (mapLookup(address(X), address(X) |-> u(_) M:Map) => ?_:Maybe) ~> M:Map ~> _:K endmodule