From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Thu, 17 Feb 2011 05:27:48 +0000 (+0000)
Subject: some unit tests to work on slicing
X-Git-Tag: cvc5-1.0.0~8706
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2026786fb40e6278942918489823742cd690169c;p=cvc5.git

some unit tests to work on slicing
---

diff --git a/test/regress/regress0/bv/core/slice-01.cvc b/test/regress/regress0/bv/core/slice-01.cvc
new file mode 100644
index 000000000..e27f1c902
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-01.cvc
@@ -0,0 +1,5 @@
+x: BITVECTOR(64); 
+y, z : BITVECTOR(32);
+ASSERT(x = y @ z);
+QUERY(x[63:32] = y);
+
diff --git a/test/regress/regress0/bv/core/slice-01.smt b/test/regress/regress0/bv/core/slice-01.smt
new file mode 100644
index 000000000..f0fc25078
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-01.smt
@@ -0,0 +1,9 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[64]))
+  :extrafuns ((y BitVec[32]))
+  :extrafuns ((z BitVec[32]))
+  :assumption (= x (concat y z))
+  :formula (not (= (extract[63:32] x) y))
+)
diff --git a/test/regress/regress0/bv/core/slice-02.cvc b/test/regress/regress0/bv/core/slice-02.cvc
new file mode 100644
index 000000000..35eb43d55
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-02.cvc
@@ -0,0 +1,5 @@
+x: BITVECTOR(64); 
+y, z : BITVECTOR(32);
+ASSERT(x = y @ z);
+QUERY(x[31:0] = z);
+
diff --git a/test/regress/regress0/bv/core/slice-02.smt b/test/regress/regress0/bv/core/slice-02.smt
new file mode 100644
index 000000000..182c89b15
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-02.smt
@@ -0,0 +1,9 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[64]))
+  :extrafuns ((y BitVec[32]))
+  :extrafuns ((z BitVec[32]))
+  :assumption (= x (concat y z))
+  :formula (not (= (extract[31:0] x) z))
+)
diff --git a/test/regress/regress0/bv/core/slice-03.cvc b/test/regress/regress0/bv/core/slice-03.cvc
new file mode 100644
index 000000000..51fb1983c
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-03.cvc
@@ -0,0 +1,7 @@
+x1, x2: BITVECTOR(64); 
+y, z : BITVECTOR(32);
+ASSERT(x1 = y @ z);
+ASSERT(x2[63:32] = y);
+ASSERT(x2[31:0] = z);
+QUERY(x1 = x2);
+
diff --git a/test/regress/regress0/bv/core/slice-03.smt b/test/regress/regress0/bv/core/slice-03.smt
new file mode 100644
index 000000000..c827f926f
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-03.smt
@@ -0,0 +1,12 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x1 BitVec[64]))
+  :extrafuns ((x2 BitVec[64]))
+  :extrafuns ((y BitVec[32]))
+  :extrafuns ((z BitVec[32]))
+  :assumption (= x1 (concat y z))
+  :assumption (= (extract[63:32] x2) y)
+  :assumption (= (extract[31:0] x2) z)
+  :formula (not (= x1 x2))
+)
diff --git a/test/regress/regress0/bv/core/slice-04.cvc b/test/regress/regress0/bv/core/slice-04.cvc
new file mode 100644
index 000000000..97e5b0b57
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-04.cvc
@@ -0,0 +1,15 @@
+x1: BITVECTOR(64); 
+x2: BITVECTOR(32);
+x3: BITVECTOR(16);
+x4: BITVECTOR(8);
+x5: BITVECTOR(4);
+x6: BITVECTOR(2);
+x7: BITVECTOR(1);
+ASSERT(x1 = x2 @ x2);
+ASSERT(x2 = x3 @ x3);
+ASSERT(x3 = x4 @ x4);
+ASSERT(x4 = x5 @ x5);
+ASSERT(x5 = x6 @ x6);
+ASSERT(x6 = x7 @ x7);
+QUERY(x1[0:0] = x7);
+
diff --git a/test/regress/regress0/bv/core/slice-04.smt b/test/regress/regress0/bv/core/slice-04.smt
new file mode 100644
index 000000000..ef9cc6e81
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-04.smt
@@ -0,0 +1,18 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x1 BitVec[64]))
+  :extrafuns ((x2 BitVec[32]))
+  :extrafuns ((x3 BitVec[16]))
+  :extrafuns ((x4 BitVec[8]))
+  :extrafuns ((x5 BitVec[4]))
+  :extrafuns ((x6 BitVec[2]))
+  :extrafuns ((x7 BitVec[1]))
+  :assumption (= x1 (concat x2 x2))
+  :assumption (= x2 (concat x3 x3))
+  :assumption (= x3 (concat x4 x4))
+  :assumption (= x4 (concat x5 x5))
+  :assumption (= x5 (concat x6 x6))
+  :assumption (= x6 (concat x7 x7))
+  :formula (not (= (extract[0:0] x1) x7))
+)
diff --git a/test/regress/regress0/bv/core/slice-05.cvc b/test/regress/regress0/bv/core/slice-05.cvc
new file mode 100644
index 000000000..30fe1ed35
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-05.cvc
@@ -0,0 +1,15 @@
+x1: BITVECTOR(64); 
+x2: BITVECTOR(32);
+x3: BITVECTOR(16);
+x4: BITVECTOR(8);
+x5: BITVECTOR(4);
+x6: BITVECTOR(2);
+x7: BITVECTOR(1);
+ASSERT(x1 = x2 @ x2);
+ASSERT(x2 = x3 @ x3);
+ASSERT(x3 = x4 @ x4);
+ASSERT(x4 = x5 @ x5);
+ASSERT(x5 = x6 @ x6);
+ASSERT(x6 = x7 @ x7);
+QUERY(x1[63:63] = x7);
+
diff --git a/test/regress/regress0/bv/core/slice-05.smt b/test/regress/regress0/bv/core/slice-05.smt
new file mode 100644
index 000000000..75af2cd47
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-05.smt
@@ -0,0 +1,18 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x1 BitVec[64]))
+  :extrafuns ((x2 BitVec[32]))
+  :extrafuns ((x3 BitVec[16]))
+  :extrafuns ((x4 BitVec[8]))
+  :extrafuns ((x5 BitVec[4]))
+  :extrafuns ((x6 BitVec[2]))
+  :extrafuns ((x7 BitVec[1]))
+  :assumption (= x1 (concat x2 x2))
+  :assumption (= x2 (concat x3 x3))
+  :assumption (= x3 (concat x4 x4))
+  :assumption (= x4 (concat x5 x5))
+  :assumption (= x5 (concat x6 x6))
+  :assumption (= x6 (concat x7 x7))
+  :formula (not (= (extract[63:63] x1) x7))
+)
diff --git a/test/regress/regress0/bv/core/slice-06.cvc b/test/regress/regress0/bv/core/slice-06.cvc
new file mode 100644
index 000000000..554e65567
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-06.cvc
@@ -0,0 +1,15 @@
+x1: BITVECTOR(64); 
+x2: BITVECTOR(32);
+x3: BITVECTOR(16);
+x4: BITVECTOR(8);
+x5: BITVECTOR(4);
+x6: BITVECTOR(2);
+x7: BITVECTOR(1);
+ASSERT(x1 = x2 @ x2);
+ASSERT(x2 = x3 @ x3);
+ASSERT(x3 = x4 @ x4);
+ASSERT(x4 = x5 @ x5);
+ASSERT(x5 = x6 @ x6);
+ASSERT(x6 = x7 @ x7);
+QUERY(x1[63:63] = x1[0:0]);
+
diff --git a/test/regress/regress0/bv/core/slice-06.smt b/test/regress/regress0/bv/core/slice-06.smt
new file mode 100644
index 000000000..da3c7fc08
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-06.smt
@@ -0,0 +1,18 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x1 BitVec[64]))
+  :extrafuns ((x2 BitVec[32]))
+  :extrafuns ((x3 BitVec[16]))
+  :extrafuns ((x4 BitVec[8]))
+  :extrafuns ((x5 BitVec[4]))
+  :extrafuns ((x6 BitVec[2]))
+  :extrafuns ((x7 BitVec[1]))
+  :assumption (= x1 (concat x2 x2))
+  :assumption (= x2 (concat x3 x3))
+  :assumption (= x3 (concat x4 x4))
+  :assumption (= x4 (concat x5 x5))
+  :assumption (= x5 (concat x6 x6))
+  :assumption (= x6 (concat x7 x7))
+  :formula (not (= (extract[63:63] x1) (extract[0:0] x1)))
+)
diff --git a/test/regress/regress0/bv/core/slice-07.cvc b/test/regress/regress0/bv/core/slice-07.cvc
new file mode 100644
index 000000000..134037a40
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-07.cvc
@@ -0,0 +1,4 @@
+x: BITVECTOR(5); 
+ASSERT(x[4:1] = x[3:0]);
+QUERY(x[4:4]=x[0:0]);
+
diff --git a/test/regress/regress0/bv/core/slice-07.smt b/test/regress/regress0/bv/core/slice-07.smt
new file mode 100644
index 000000000..4918f1b41
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-07.smt
@@ -0,0 +1,7 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[5]))
+  :assumption (= (extract[4:1] x) (extract[3:0] x))
+  :formula (not (= (extract[4:4] x) (extract[0:0] x)))
+)
diff --git a/test/regress/regress0/bv/core/slice-08.cvc b/test/regress/regress0/bv/core/slice-08.cvc
new file mode 100644
index 000000000..bf5222844
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-08.cvc
@@ -0,0 +1,4 @@
+x: BITVECTOR(5); 
+ASSERT(x[4:3] = x[1:0]);
+QUERY(x[4:4]=x[0:0]);
+
diff --git a/test/regress/regress0/bv/core/slice-08.smt b/test/regress/regress0/bv/core/slice-08.smt
new file mode 100644
index 000000000..6c9c0162b
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-08.smt
@@ -0,0 +1,7 @@
+(benchmark slice
+  :status sat
+  :logic QF_BV
+  :extrafuns ((x BitVec[5]))
+  :assumption (= (extract[4:3] x) (extract[1:0] x))
+  :formula (not (= (extract[4:4] x) (extract[0:0] x)))
+)
diff --git a/test/regress/regress0/bv/core/slice-09.cvc b/test/regress/regress0/bv/core/slice-09.cvc
new file mode 100644
index 000000000..43876c923
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-09.cvc
@@ -0,0 +1,4 @@
+x: BITVECTOR(6); 
+ASSERT(x[5:2] = x[3:0]);
+QUERY(x[5:4]=x[1:0]);
+
diff --git a/test/regress/regress0/bv/core/slice-09.smt b/test/regress/regress0/bv/core/slice-09.smt
new file mode 100644
index 000000000..6a655442e
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-09.smt
@@ -0,0 +1,7 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[6]))
+  :assumption (= (extract[5:2] x) (extract[3:0] x))
+  :formula (not (= (extract[5:4] x) (extract[1:0] x)))
+)
diff --git a/test/regress/regress0/bv/core/slice-10.cvc b/test/regress/regress0/bv/core/slice-10.cvc
new file mode 100644
index 000000000..953d41ec2
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-10.cvc
@@ -0,0 +1,5 @@
+x : BITVECTOR(8);
+ASSERT(x[3:0] = 0bin0000);
+ASSERT(x[7:4] = 0bin1111);
+QUERY(x = 0bin11110000);
+
diff --git a/test/regress/regress0/bv/core/slice-10.smt b/test/regress/regress0/bv/core/slice-10.smt
new file mode 100644
index 000000000..cc2a9b9b6
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-10.smt
@@ -0,0 +1,8 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[8]))
+  :assumption (= (extract[3:0] x) bv0[4])
+  :assumption (= (extract[7:4] x) bv15[4])
+  :formula (not (= x bv240[8]))
+)
diff --git a/test/regress/regress0/bv/core/slice-11.cvc b/test/regress/regress0/bv/core/slice-11.cvc
new file mode 100644
index 000000000..0fc79c13e
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-11.cvc
@@ -0,0 +1,4 @@
+x : BITVECTOR(8);
+ASSERT(x = 0bin01010101);
+QUERY(x[0:0]@x[2:2]@x[4:4]@x[6:6] = 0bin1111);
+
diff --git a/test/regress/regress0/bv/core/slice-11.smt b/test/regress/regress0/bv/core/slice-11.smt
new file mode 100644
index 000000000..b69151d9d
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-11.smt
@@ -0,0 +1,7 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[8]))
+  :assumption (= x bv85[8])
+  :formula (not (= (concat (concat (concat (extract[0:0] x) (extract[2:2] x)) (extract[4:4] x)) (extract[6:6] x)) bv15[4]))
+)
diff --git a/test/regress/regress0/bv/core/slice-12.cvc b/test/regress/regress0/bv/core/slice-12.cvc
new file mode 100644
index 000000000..7d0d79336
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-12.cvc
@@ -0,0 +1,8 @@
+x, y: BITVECTOR(8);
+z1, z2: BITVECTOR(4);
+ASSERT(x = 0bin01010101);
+ASSERT(y = 0bin10101010);
+ASSERT(z1 = x[0:0]@x[2:2]@x[4:4]@x[6:6]);
+ASSERT(z2 = y[7:7]@y[5:5]@y[3:3]@y[1:1]);
+QUERY(z1 = z2);
+
diff --git a/test/regress/regress0/bv/core/slice-12.smt b/test/regress/regress0/bv/core/slice-12.smt
new file mode 100644
index 000000000..998dee663
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-12.smt
@@ -0,0 +1,13 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[8]))
+  :extrafuns ((y BitVec[8]))
+  :extrafuns ((z1 BitVec[4]))
+  :extrafuns ((z2 BitVec[4]))
+  :assumption (= x bv85[8])
+  :assumption (= y bv170[8])
+  :assumption (= z1 (concat (concat (concat (extract[0:0] x) (extract[2:2] x)) (extract[4:4] x)) (extract[6:6] x)))
+  :assumption (= z2 (concat (concat (concat (extract[7:7] y) (extract[5:5] y)) (extract[3:3] y)) (extract[1:1] y)))
+  :formula (not (= z1 z2))
+)
diff --git a/test/regress/regress0/bv/core/slice-13.cvc b/test/regress/regress0/bv/core/slice-13.cvc
new file mode 100644
index 000000000..0c3e82f97
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-13.cvc
@@ -0,0 +1,8 @@
+x, y: BITVECTOR(8);
+z1, z2: BITVECTOR(4);
+ASSERT(z1 = x[0:0]@x[2:2]@x[4:4]@x[6:6]);
+ASSERT(z2 = y[7:7]@y[5:5]@y[3:3]@y[1:1]);
+ASSERT(x = 0bin01010101);
+ASSERT(y = 0bin10101010);
+QUERY(z1 = z2);
+
diff --git a/test/regress/regress0/bv/core/slice-13.smt b/test/regress/regress0/bv/core/slice-13.smt
new file mode 100644
index 000000000..1c61a8fa9
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-13.smt
@@ -0,0 +1,13 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[8]))
+  :extrafuns ((y BitVec[8]))
+  :extrafuns ((z1 BitVec[4]))
+  :extrafuns ((z2 BitVec[4]))
+  :assumption (= z1 (concat (concat (concat (extract[0:0] x) (extract[2:2] x)) (extract[4:4] x)) (extract[6:6] x)))
+  :assumption (= z2 (concat (concat (concat (extract[7:7] y) (extract[5:5] y)) (extract[3:3] y)) (extract[1:1] y)))
+  :assumption (= x bv85[8])
+  :assumption (= y bv170[8])
+  :formula (not (= z1 z2))
+)
diff --git a/test/regress/regress0/bv/core/slice-14.cvc b/test/regress/regress0/bv/core/slice-14.cvc
new file mode 100644
index 000000000..286f948de
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-14.cvc
@@ -0,0 +1,5 @@
+x: BITVECTOR(16);
+ASSERT(x[15:1] = x[14:0]);
+ASSERT(x[0:0] = 0bin0);
+QUERY(x = 0bin0000000000000000);
+
diff --git a/test/regress/regress0/bv/core/slice-14.smt b/test/regress/regress0/bv/core/slice-14.smt
new file mode 100644
index 000000000..b40f7938d
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-14.smt
@@ -0,0 +1,8 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[16]))
+  :assumption (= (extract[15:1] x) (extract[14:0] x))
+  :assumption (= (extract[0:0] x) bv0[1])
+  :formula (not (= x bv0[16]))
+)
diff --git a/test/regress/regress0/bv/core/slice-15.cvc b/test/regress/regress0/bv/core/slice-15.cvc
new file mode 100644
index 000000000..076a54790
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-15.cvc
@@ -0,0 +1,5 @@
+x: BITVECTOR(16);
+ASSERT(x[15:15] = 0bin1);
+ASSERT(x[15:1] = x[14:0]);
+QUERY(x = 0bin1111111111111111);
+
diff --git a/test/regress/regress0/bv/core/slice-15.smt b/test/regress/regress0/bv/core/slice-15.smt
new file mode 100644
index 000000000..b45e603c7
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-15.smt
@@ -0,0 +1,8 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[16]))
+  :assumption (= (extract[15:15] x) bv1[1])
+  :assumption (= (extract[15:1] x) (extract[14:0] x))
+  :formula (not (= x bv65535[16]))
+)
diff --git a/test/regress/regress0/bv/core/slice-16.cvc b/test/regress/regress0/bv/core/slice-16.cvc
new file mode 100644
index 000000000..8a5b4bab9
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-16.cvc
@@ -0,0 +1,5 @@
+x: BITVECTOR(16);
+ASSERT(x[15:15] = 0bin1);
+ASSERT(x[15:2] = x[13:0]);
+QUERY(x = 0bin1111111111111111);
+
diff --git a/test/regress/regress0/bv/core/slice-16.smt b/test/regress/regress0/bv/core/slice-16.smt
new file mode 100644
index 000000000..5cadd2924
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-16.smt
@@ -0,0 +1,8 @@
+(benchmark slice  
+  :status sat
+  :logic QF_BV
+  :extrafuns ((x BitVec[16]))
+  :assumption (= (extract[15:15] x) bv1[1])
+  :assumption (= (extract[15:2] x) (extract[13:0] x))
+  :formula (not (= x bv65535[16]))
+)
diff --git a/test/regress/regress0/bv/core/slice-17.cvc b/test/regress/regress0/bv/core/slice-17.cvc
new file mode 100644
index 000000000..1f2a44423
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-17.cvc
@@ -0,0 +1,8 @@
+x: BITVECTOR(16);
+y: BITVECTOR(12);
+ASSERT(y = x[11:0]);
+ASSERT(y = x[15:4]);
+ASSERT(y[3:1] = y[2:0]);
+ASSERT(x[0:0] = 0bin1);
+QUERY(x = 0bin1111111111111111);
+
diff --git a/test/regress/regress0/bv/core/slice-17.smt b/test/regress/regress0/bv/core/slice-17.smt
new file mode 100644
index 000000000..589444634
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-17.smt
@@ -0,0 +1,11 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[16]))
+  :extrafuns ((y BitVec[12]))
+  :assumption (= y (extract[11:0] x))
+  :assumption (= y (extract[15:4] x))
+  :assumption (= (extract[3:1] y) (extract[2:0] y))
+  :assumption (= (extract[0:0] x) bv1[1])
+  :formula (not (= x bv65535[16]))
+)
diff --git a/test/regress/regress0/bv/core/slice-18.cvc b/test/regress/regress0/bv/core/slice-18.cvc
new file mode 100644
index 000000000..99f4707d8
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-18.cvc
@@ -0,0 +1,8 @@
+x: BITVECTOR(16);
+y: BITVECTOR(12);
+ASSERT(x[0:0] = 0bin1);
+ASSERT(y = x[11:0]);
+ASSERT(y = x[15:4]);
+ASSERT(y[3:1] = y[2:0]);
+QUERY(x = 0bin1111111111111111);
+
diff --git a/test/regress/regress0/bv/core/slice-18.smt b/test/regress/regress0/bv/core/slice-18.smt
new file mode 100644
index 000000000..7a97e7447
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-18.smt
@@ -0,0 +1,11 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[16]))
+  :extrafuns ((y BitVec[12]))
+  :assumption (= (extract[0:0] x) bv1[1])
+  :assumption (= y (extract[11:0] x))
+  :assumption (= y (extract[15:4] x))
+  :assumption (= (extract[3:1] y) (extract[2:0] y))
+  :formula (not (= x bv65535[16]))
+)
diff --git a/test/regress/regress0/bv/core/slice-19.cvc b/test/regress/regress0/bv/core/slice-19.cvc
new file mode 100644
index 000000000..0f76359b8
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-19.cvc
@@ -0,0 +1,8 @@
+x: BITVECTOR(16);
+y: BITVECTOR(12);
+ASSERT(y = x[11:0]);
+ASSERT(y = x[15:4]);
+ASSERT(y[3:2] = y[1:0]);
+ASSERT(x[1:0] = 0bin01);
+QUERY(x = 0bin0101010101010101);
+
diff --git a/test/regress/regress0/bv/core/slice-19.smt b/test/regress/regress0/bv/core/slice-19.smt
new file mode 100644
index 000000000..3e98d6149
--- /dev/null
+++ b/test/regress/regress0/bv/core/slice-19.smt
@@ -0,0 +1,11 @@
+(benchmark slice
+  :status unsat
+  :logic QF_BV
+  :extrafuns ((x BitVec[16]))
+  :extrafuns ((y BitVec[12]))
+  :assumption (= y (extract[11:0] x))
+  :assumption (= y (extract[15:4] x))
+  :assumption (= (extract[3:2] y) (extract[1:0] y))
+  :assumption (= (extract[1:0] x) bv1[2])
+  :formula (not (= x bv21845[16]))
+)