add test

boogie-org · Oct 25, 2024 · 52d5765 · 52d5765
1 parent c59f931
commit 52d5765
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/Test/datatypes/is-cons.bpl b/Test/datatypes/is-cons.bpl
@@ -0,0 +1,12 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype X {
+    A'(a: int),
+    B'(b: bool)
+}
+
+procedure P(x: X) {
+    assume x is A';
+    assert !(x is B');
+}
diff --git a/Test/datatypes/is-cons.bpl.expect b/Test/datatypes/is-cons.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@

		Boogie program verifier finished with 1 verified, 0 errors