4 files changed, 34 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am
index 947dc65ad..0e559f6f2 100644
--- a/test/regress/regress0/bv/core/Makefile.am
+++ b/test/regress/regress0/bv/core/Makefile.am
@@ -41,6 +41,7 @@ TESTS =	\
 	equality-00.smt \
 	equality-01.smt \
 	equality-02.smt \
+  equality-05.smt \
 	bv_eq_diamond10.smt \
 	slice-01.smt \
 	slice-02.smt \
diff --git a/test/regress/regress0/bv/core/equality-05.cvc b/test/regress/regress0/bv/core/equality-05.cvc
new file mode 100644
index 000000000..93bef502d
--- /dev/null
+++ b/test/regress/regress0/bv/core/equality-05.cvc
@@ -0,0 +1,6 @@
+x,y:BITVECTOR(1);
+ASSERT(x = 0bin0);
+ASSERT(y = 0bin1);
+ASSERT(x = y);
+CHECKSAT;
+
diff --git a/test/regress/regress0/bv/core/equality-05.smt b/test/regress/regress0/bv/core/equality-05.smt
new file mode 100644
index 000000000..a7b9f6185
--- /dev/null
+++ b/test/regress/regress0/bv/core/equality-05.smt
@@ -0,0 +1,11 @@
+(benchmark equality
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[1]))
+  :extrafuns ((y BitVec[1]))
+  :assumption (= x bv0[1])
+  :assumption (= y bv1[1])
+  :assumption (= x y)
+  :formula
+true
+)
diff --git a/test/regress/regress0/bv/core/slice-20.smt b/test/regress/regress0/bv/core/slice-20.smt
new file mode 100644
index 000000000..66fac573b
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-20.smt
@@ -0,0 +1,16 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x1 BitVec[4]))
+  :extrafuns ((y1 BitVec[4]))
+  :extrafuns ((x2 BitVec[2]))
+  :extrafuns ((y2 BitVec[2]))
+  :extrafuns ((x3 BitVec[1]))
+  :extrafuns ((y3 BitVec[1]))
+  :assumption (= x1 y1)
+  :assumption (= x1 (concat x2 x2))
+  :assumption (= x2 (concat x3 x3))
+  :assumption (= y1 (concat y2 y2))
+  :assumption (= y2 (concat y3 y3))
+  :formula (not (= x3 y3))
+)