test/issue-1665

Author: ttuegel

test/issue-1665/Makefile

@@ -0,0 +1 @@
+include $(CURDIR)/../include.mk

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

@@ -0,0 +1,12 @@
+module VERIFICATION
+  import TEST
+endmodule
+
+module ISSUE-1665-SPEC
+  import VERIFICATION
+
+  // Proving this claim requires inferring that the left-hand side of an
+  // intermediate proof goal is defined.
+  //
+  rule <k> begin _ => end ?_ </k>
+endmodule

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

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

test/issue-1665/test.k

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