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

Author: ttuegel

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

@@ -0,0 +1,16 @@
+module VERIFICATION
+  import TEST
+
+  rule begin X => end fun(X)
+
+endmodule
+
+module ISSUE-1665-SPEC
+  import VERIFICATION
+
+  // Proving this claim requires recognizing that #Not(#Ceil(fun(_))) makes the
+  // left-hand side #False.
+  //
+  rule <k> begin X => end ?_ </k>
+
+endmodule

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

@@ -0,0 +1 @@
+#True

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

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

test/check-implication/test.k

@@ -1,7 +1,8 @@
 module TEST-SYNTAX
   import INT
 
-  syntax Pgm ::= "begin" | "end"
+  syntax Pgm ::= "begin" Int [unused]
+  syntax Pgm ::= "end" Int [unused]
   syntax Int ::= fun(Int) [function, no-evaluators]
   syntax Bool ::= isFun(Int) [function, functional, no-evaluators]
 
@@ -12,8 +13,6 @@ module TEST
 
   configuration <k> $PGM:Pgm </k>
 
-  rule begin => end
-
   rule [ceil-fun]: #Ceil(fun(X:Int)) => #True requires isFun(X) [anywhere, simplification]
 
 endmodule