add failing test

uclid-org · Jul 4, 2024 · 7033967 · 7033967
1 parent 6f3f8da
commit 7033967
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 0 deletions.
diff --git a/src/test/scala/SMTLIB2Spec.scala b/src/test/scala/SMTLIB2Spec.scala
@@ -445,6 +445,9 @@ class SMTLIB2Spec extends AnyFlatSpec {
   "issue-187b.ucl" should "verify all assertions." in {
     SMTLIB2Spec.expectedFails("./test/issue-187b.ucl", 0)
   }
+  "issue-255.ucl" should "faill single assertion." in {
+    SMTLIB2Spec.expectedFails("./test/issue-255.ucl", 1)
+  }
   "test-redundant-assign.ucl" should "verify all assertions." in {
     SMTLIB2Spec.expectedFails("./test/test-redundant-assign.ucl", 0)
   }

diff --git a/test/issue-255.ucl b/test/issue-255.ucl
@@ -0,0 +1,17 @@
+module main {
+    type t;
+    datatype a = A(x: t);
+
+    var y: a;
+    var z: t;
+
+    init {
+        assert y.x == z;
+    }
+
+    control {
+        bmc(0);
+        check;
+        print_results;
+    }
+}