From f3303375b4b79ac8e70b454eb566b51e03539be7 Mon Sep 17 00:00:00 2001
From: hra687261 <hra687261@gmail.com>
Date: Tue, 4 Jul 2023 07:02:30 +0200
Subject: [PATCH] Add failing tests

---
 tests/dolmen/bitv/errors/testfile-bitv046.expected |  2 ++
 tests/dolmen/bitv/errors/testfile-bitv046.smt2     | 10 ++++++++++
 tests/dolmen/bitv/errors/testfile-bitv047.expected |  2 ++
 tests/dolmen/bitv/errors/testfile-bitv047.smt2     |  7 +++++++
 4 files changed, 21 insertions(+)
 create mode 100644 tests/dolmen/bitv/errors/testfile-bitv046.expected
 create mode 100644 tests/dolmen/bitv/errors/testfile-bitv046.smt2
 create mode 100644 tests/dolmen/bitv/errors/testfile-bitv047.expected
 create mode 100644 tests/dolmen/bitv/errors/testfile-bitv047.smt2

diff --git a/tests/dolmen/bitv/errors/testfile-bitv046.expected b/tests/dolmen/bitv/errors/testfile-bitv046.expected
new file mode 100644
index 000000000..6f99ff0f4
--- /dev/null
+++ 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
new file mode 100644
index 000000000..cb15affb8
--- /dev/null
+++ 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
new file mode 100644
index 000000000..b2ee9c47d
--- /dev/null
+++ b/tests/dolmen/bitv/errors/testfile-bitv047.expected
@@ -0,0 +1,2 @@
+
+unsat
\ No newline at end of file
diff --git a/tests/dolmen/bitv/errors/testfile-bitv047.smt2 b/tests/dolmen/bitv/errors/testfile-bitv047.smt2
new file mode 100644
index 000000000..98aff74b7
--- /dev/null
+++ 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)