Skip to content

Commit e39ec77

Browse files
Update dependency: deps/k_release (#3149)
* deps/k_release: v5.3.112 * deps/k_release: v5.3.113 * deps/k_release: v5.3.114 * deps/k_release: v5.3.116 * deps/k_release: v5.3.117 * deps/k_release: v5.3.118 * deps/k_release: v5.3.120 * deps/k_release: v5.3.121 * Remove anywhere attribute from simplification rules * deps/k_release: v5.3.122 * deps/k_release: v5.3.123 * deps/k_release: v5.3.125 * deps/k_release: v5.3.126 * Remove unsupported test from suite Co-authored-by: ana-pantilie <45069775+ana-pantilie@users.noreply.github.com> Co-authored-by: ana-pantilie <ana.pantilie95@gmail.com>
1 parent 9f7010f commit e39ec77

File tree

8 files changed

+9
-13
lines changed

8 files changed

+9
-13
lines changed

deps/k_release

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
v5.3.98
1+
v5.3.126

test/issue-1665/test.k

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,6 @@ module TEST
1414

1515
rule begin X => end fun(X)
1616

17-
rule [ceil-fun]: #Ceil(fun(X:Int)) => #True requires isFun(X) [anywhere, simplification]
17+
rule [ceil-fun]: #Ceil(fun(X:Int)) => #True requires isFun(X) [simplification]
1818

1919
endmodule

test/issue-1916/test.k

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,6 @@ module TEST
1616

1717
rule begin => end
1818

19-
rule [ceil-fun]: #Ceil(fun(X:Int)) => #True requires isFun(X) [anywhere, simplification]
19+
rule [ceil-fun]: #Ceil(fun(X:Int)) => #True requires isFun(X) [simplification]
2020

2121
endmodule

test/issue-3107/ceil-set.k

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,6 @@ module CEIL-SET
1414
rule <k> eval ( S ) => evalResult ( S ) </k>
1515

1616
rule [setCeil]: #Ceil(@S1:Set @S2:Set) => {intersectSet(@S1, @S2) #Equals .Set} #And #Ceil(@S1) #And #Ceil(@S2)
17-
[anywhere, simplification]
17+
[simplification]
1818

19-
endmodule
19+
endmodule

test/ml-simplification/test.k

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ module TEST
33
imports BOOL
44

55
rule {I +Int J #Equals I +Int K} => #Bottom
6-
requires notBool J ==Int K [anywhere, simplification]
6+
requires notBool J ==Int K [simplification]
77

88
syntax Test ::= runTest( K ) | doneTest( K )
99

test/setvars/4.setvars

Lines changed: 0 additions & 1 deletion
This file was deleted.

test/setvars/4.setvars.out.golden

Lines changed: 0 additions & 3 deletions
This file was deleted.

test/setvars/setvars.k

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,8 @@ module SETVARS
1313
syntax Int ::= h(Int) [function]
1414
rule h(@X:Int) => @X +Int 1 [simplification]
1515

16-
syntax KItem ::= i(Int)
17-
rule i(@X:Int) => @X +Int 1 [simplification,anywhere]
16+
// syntax KItem ::= i(Int)
17+
// rule i(@X:Int) => @X +Int 1 [anywhere] // This is not yet supported
1818

1919
syntax Int ::= j(Int, Int) [function, functional]
2020

@@ -26,6 +26,6 @@ module SETVARS
2626
#Ceil(@I1:Int /Int @I2:Int)
2727
=>
2828
{(@I2 =/=Int 0) #Equals true} #And #Ceil(@I1) #And #Ceil(@I2)
29-
[anywhere]
29+
[simplification]
3030
*/
3131
endmodule

0 commit comments

Comments
 (0)