Skip to content

Commit 1b248d6

Browse files
committed
Revert "test/check-implication/issue-1665-spec.k"
This reverts commit 508d58b.
1 parent 508d58b commit 1b248d6

File tree

4 files changed

+4
-23
lines changed

4 files changed

+4
-23
lines changed

test/check-implication/issue-1665-spec.k

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

test/check-implication/issue-1665-spec.k.out.golden

Lines changed: 0 additions & 1 deletion
This file was deleted.
Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,5 @@
11
module VERIFICATION
22
import TEST
3-
4-
rule begin _ => end 0
5-
63
endmodule
74

85
module ISSUE-1916-SPEC
@@ -11,5 +8,5 @@ module ISSUE-1916-SPEC
118
// Proving this claim requires that the right-hand side is simplified using
129
// the conditions from the left-hand side.
1310
//
14-
rule <k> begin _ => end ?_ </k> requires isFun(X) ensures true #And #Ceil(fun(X))
11+
rule <k> begin => end </k> requires isFun(X) ensures true #And #Ceil(fun(X))
1512
endmodule

test/check-implication/test.k

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
11
module TEST-SYNTAX
22
import INT
33

4-
syntax Pgm ::= "begin" Int [unused]
5-
syntax Pgm ::= "end" Int [unused]
4+
syntax Pgm ::= "begin" | "end"
65
syntax Int ::= fun(Int) [function, no-evaluators]
76
syntax Bool ::= isFun(Int) [function, functional, no-evaluators]
87

@@ -13,6 +12,8 @@ module TEST
1312

1413
configuration <k> $PGM:Pgm </k>
1514

15+
rule begin => end
16+
1617
rule [ceil-fun]: #Ceil(fun(X:Int)) => #True requires isFun(X) [anywhere, simplification]
1718

1819
endmodule

0 commit comments

Comments
 (0)