Add failing tests

OCamlPro · Jul 4, 2023 · f330337 · f330337
1 parent c6e9d83
commit f330337
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 0 deletions.
diff --git a/tests/dolmen/bitv/errors/testfile-bitv046.expected b/tests/dolmen/bitv/errors/testfile-bitv046.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/dolmen/bitv/errors/testfile-bitv046.smt2 b/tests/dolmen/bitv/errors/testfile-bitv046.smt2
@@ -0,0 +1,10 @@
+(set-logic BV)
+(assert
+  (distinct
+    (exists
+      ((x (_ BitVec 2)))
+      (= (_ bv0 2) (bvashr x (_ bv0 2))))
+    (exists
+      ((y (_ BitVec 2)))
+      (= (_ bv0 2) (bvand y (_ bv0 2))))))
+(check-sat)
diff --git a/tests/dolmen/bitv/errors/testfile-bitv047.expected b/tests/dolmen/bitv/errors/testfile-bitv047.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/dolmen/bitv/errors/testfile-bitv047.smt2 b/tests/dolmen/bitv/errors/testfile-bitv047.smt2
@@ -0,0 +1,7 @@
+(set-logic BV)
+(assert
+  (exists ((x (_ BitVec 2)))
+    (and
+      (bvslt x (_ bv1 2))
+      (forall ((y (_ BitVec 2))) (= y (_ bv1 2))))))
+(check-sat)