bitvector rewriting for the core theory and testcases

68 files changed, 289 insertions, 0 deletions

diff --git a/test/regress/regress0/bv/core/concat-merge-0.cvc b/test/regress/regress0/bv/core/concat-merge-0.cvc
new file mode 100644
index 000000000..60341c03b
--- /dev/null
+++ b/test/regress/regress0/bv/core/concat-merge-0.cvc
@@ -0,0 +1,3 @@
+x : BITVECTOR(32);
+QUERY (x[2:1]   @ x[0:0]  = x[2:0] );
+
diff --git a/test/regress/regress0/bv/core/concat-merge-0.smt b/test/regress/regress0/bv/core/concat-merge-0.smt
new file mode 100644
index 000000000..c68d4ec53
--- /dev/null
+++ b/test/regress/regress0/bv/core/concat-merge-0.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (concat (extract[2:1] x) (extract[0:0] x)) (extract[2:0] x)))
+)
diff --git a/test/regress/regress0/bv/core/concat-merge-1.cvc b/test/regress/regress0/bv/core/concat-merge-1.cvc
new file mode 100644
index 000000000..af0e8387b
--- /dev/null
+++ b/test/regress/regress0/bv/core/concat-merge-1.cvc
@@ -0,0 +1,3 @@
+x : BITVECTOR(32);
+QUERY (x[4:2]   @ x[1:0]  = x[4:0] );
+
diff --git a/test/regress/regress0/bv/core/concat-merge-1.smt b/test/regress/regress0/bv/core/concat-merge-1.smt
new file mode 100644
index 000000000..4b6702598
--- /dev/null
+++ b/test/regress/regress0/bv/core/concat-merge-1.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (concat (extract[4:2] x) (extract[1:0] x)) (extract[4:0] x)))
+)
diff --git a/test/regress/regress0/bv/core/concat-merge-2.cvc b/test/regress/regress0/bv/core/concat-merge-2.cvc
new file mode 100644
index 000000000..8ad7f2aa3
--- /dev/null
+++ b/test/regress/regress0/bv/core/concat-merge-2.cvc
@@ -0,0 +1,3 @@
+x : BITVECTOR(32);
+QUERY (x[8:4]   @ x[3:0]  = x[8:0] );
+
diff --git a/test/regress/regress0/bv/core/concat-merge-2.smt b/test/regress/regress0/bv/core/concat-merge-2.smt
new file mode 100644
index 000000000..2350d6d8b
--- /dev/null
+++ b/test/regress/regress0/bv/core/concat-merge-2.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (concat (extract[8:4] x) (extract[3:0] x)) (extract[8:0] x)))
+)
diff --git a/test/regress/regress0/bv/core/concat-merge-3.cvc b/test/regress/regress0/bv/core/concat-merge-3.cvc
new file mode 100644
index 000000000..d46da1a55
--- /dev/null
+++ b/test/regress/regress0/bv/core/concat-merge-3.cvc
@@ -0,0 +1,3 @@
+x : BITVECTOR(32);
+QUERY (x[16:8]  @ x[7:0]  = x[16:0]);
+
diff --git a/test/regress/regress0/bv/core/concat-merge-3.smt b/test/regress/regress0/bv/core/concat-merge-3.smt
new file mode 100644
index 000000000..303357541
--- /dev/null
+++ b/test/regress/regress0/bv/core/concat-merge-3.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (concat (extract[16:8] x) (extract[7:0] x)) (extract[16:0] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-concat-0.cvc b/test/regress/regress0/bv/core/extract-concat-0.cvc
new file mode 100644
index 000000000..9aa608265
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-0.cvc
@@ -0,0 +1,2 @@
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[63:32] = x[31:0]);
diff --git a/test/regress/regress0/bv/core/extract-concat-0.smt b/test/regress/regress0/bv/core/extract-concat-0.smt
new file mode 100644
index 000000000..c4d6c7e02
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-0.smt
@@ -0,0 +1,7 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :formula
+(not (= (extract[63:32] (concat x y)) (extract[31:0] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-concat-1.cvc b/test/regress/regress0/bv/core/extract-concat-1.cvc
new file mode 100644
index 000000000..e192f159c
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-1.cvc
@@ -0,0 +1,2 @@
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[62:33] = x[30:1]);
diff --git a/test/regress/regress0/bv/core/extract-concat-1.smt b/test/regress/regress0/bv/core/extract-concat-1.smt
new file mode 100644
index 000000000..0f5a2c187
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-1.smt
@@ -0,0 +1,7 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :formula
+(not (= (extract[62:33] (concat x y)) (extract[30:1] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-concat-10.cvc b/test/regress/regress0/bv/core/extract-concat-10.cvc
new file mode 100644
index 000000000..8d3b88fba
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-10.cvc
@@ -0,0 +1,2 @@
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[60:3] = x[28:0] @ y[31:3]);
diff --git a/test/regress/regress0/bv/core/extract-concat-10.smt b/test/regress/regress0/bv/core/extract-concat-10.smt
new file mode 100644
index 000000000..ed44a9abb
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-10.smt
@@ -0,0 +1,7 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :formula
+(not (= (extract[60:3] (concat x y)) (concat (extract[28:0] x) (extract[31:3] y))))
+)
diff --git a/test/regress/regress0/bv/core/extract-concat-11.cvc b/test/regress/regress0/bv/core/extract-concat-11.cvc
new file mode 100644
index 000000000..2290eef04
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-11.cvc
@@ -0,0 +1,2 @@
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[59:4] = x[27:0] @ y[31:4]);
diff --git a/test/regress/regress0/bv/core/extract-concat-11.smt b/test/regress/regress0/bv/core/extract-concat-11.smt
new file mode 100644
index 000000000..ed1f6275e
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-11.smt
@@ -0,0 +1,7 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :formula
+(not (= (extract[59:4] (concat x y)) (concat (extract[27:0] x) (extract[31:4] y))))
+)
diff --git a/test/regress/regress0/bv/core/extract-concat-2.cvc b/test/regress/regress0/bv/core/extract-concat-2.cvc
new file mode 100644
index 000000000..bd1e3ff30
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-2.cvc
@@ -0,0 +1,2 @@
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[61:34] = x[29:2]);
diff --git a/test/regress/regress0/bv/core/extract-concat-2.smt b/test/regress/regress0/bv/core/extract-concat-2.smt
new file mode 100644
index 000000000..fb8c61464
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-2.smt
@@ -0,0 +1,7 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :formula
+(not (= (extract[61:34] (concat x y)) (extract[29:2] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-concat-3.cvc b/test/regress/regress0/bv/core/extract-concat-3.cvc
new file mode 100644
index 000000000..4e225be42
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-3.cvc
@@ -0,0 +1,2 @@
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[60:35] = x[28:3]);
diff --git a/test/regress/regress0/bv/core/extract-concat-3.smt b/test/regress/regress0/bv/core/extract-concat-3.smt
new file mode 100644
index 000000000..f89115ecf
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-3.smt
@@ -0,0 +1,7 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :formula
+(not (= (extract[60:35] (concat x y)) (extract[28:3] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-concat-4.cvc b/test/regress/regress0/bv/core/extract-concat-4.cvc
new file mode 100644
index 000000000..8ecf96e6f
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-4.cvc
@@ -0,0 +1,2 @@
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[31:0] = y[31:0]);
diff --git a/test/regress/regress0/bv/core/extract-concat-4.smt b/test/regress/regress0/bv/core/extract-concat-4.smt
new file mode 100644
index 000000000..29ea62916
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-4.smt
@@ -0,0 +1,7 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :formula
+(not (= (extract[31:0] (concat x y)) (extract[31:0] y)))
+)
diff --git a/test/regress/regress0/bv/core/extract-concat-5.cvc b/test/regress/regress0/bv/core/extract-concat-5.cvc
new file mode 100644
index 000000000..378ca5d2a
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-5.cvc
@@ -0,0 +1,2 @@
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[30:1] = y[30:1]);
diff --git a/test/regress/regress0/bv/core/extract-concat-5.smt b/test/regress/regress0/bv/core/extract-concat-5.smt
new file mode 100644
index 000000000..8f137ef05
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-5.smt
@@ -0,0 +1,7 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :formula
+(not (= (extract[30:1] (concat x y)) (extract[30:1] y)))
+)
diff --git a/test/regress/regress0/bv/core/extract-concat-6.cvc b/test/regress/regress0/bv/core/extract-concat-6.cvc
new file mode 100644
index 000000000..41499b55b
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-6.cvc
@@ -0,0 +1,2 @@
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[29:2] = y[29:2]);
diff --git a/test/regress/regress0/bv/core/extract-concat-6.smt b/test/regress/regress0/bv/core/extract-concat-6.smt
new file mode 100644
index 000000000..0ef6e2ee6
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-6.smt
@@ -0,0 +1,7 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :formula
+(not (= (extract[29:2] (concat x y)) (extract[29:2] y)))
+)
diff --git a/test/regress/regress0/bv/core/extract-concat-7.cvc b/test/regress/regress0/bv/core/extract-concat-7.cvc
new file mode 100644
index 000000000..838017f55
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-7.cvc
@@ -0,0 +1,2 @@
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[28:3] = y[28:3]);
diff --git a/test/regress/regress0/bv/core/extract-concat-7.smt b/test/regress/regress0/bv/core/extract-concat-7.smt
new file mode 100644
index 000000000..f1a9bf161
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-7.smt
@@ -0,0 +1,7 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :formula
+(not (= (extract[28:3] (concat x y)) (extract[28:3] y)))
+)
diff --git a/test/regress/regress0/bv/core/extract-concat-8.cvc b/test/regress/regress0/bv/core/extract-concat-8.cvc
new file mode 100644
index 000000000..68982b0a6
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-8.cvc
@@ -0,0 +1,2 @@
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[62:1] = x[30:0] @ y[31:1]);
diff --git a/test/regress/regress0/bv/core/extract-concat-8.smt b/test/regress/regress0/bv/core/extract-concat-8.smt
new file mode 100644
index 000000000..c317e94e1
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-8.smt
@@ -0,0 +1,7 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :formula
+(not (= (extract[62:1] (concat x y)) (concat (extract[30:0] x) (extract[31:1] y))))
+)
diff --git a/test/regress/regress0/bv/core/extract-concat-9.cvc b/test/regress/regress0/bv/core/extract-concat-9.cvc
new file mode 100644
index 000000000..5f0e690cb
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-9.cvc
@@ -0,0 +1,2 @@
+x, y : BITVECTOR(32);
+QUERY ((x @ y)[61:2] = x[29:0] @ y[31:2]);
diff --git a/test/regress/regress0/bv/core/extract-concat-9.smt b/test/regress/regress0/bv/core/extract-concat-9.smt
new file mode 100644
index 000000000..668842dfc
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-concat-9.smt
@@ -0,0 +1,7 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :extrafuns ((y BitVec[32]))
+  :formula
+(not (= (extract[61:2] (concat x y)) (concat (extract[29:0] x) (extract[31:2] y))))
+)
diff --git a/test/regress/regress0/bv/core/extract-constant.cvc b/test/regress/regress0/bv/core/extract-constant.cvc
new file mode 100644
index 000000000..e70ccbf5e
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-constant.cvc
@@ -0,0 +1,2 @@
+QUERY (0bin000111000[6:2] = 0bin01110);
+
diff --git a/test/regress/regress0/bv/core/extract-constant.smt b/test/regress/regress0/bv/core/extract-constant.smt
new file mode 100644
index 000000000..a36bb6ea7
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-constant.smt
@@ -0,0 +1,5 @@
+(benchmark B_
+  :logic QF_BV
+  :formula
+(not (= (extract[6:2] bv56[9]) bv14[5]))
+)
diff --git a/test/regress/regress0/bv/core/extract-extract-0.cvc b/test/regress/regress0/bv/core/extract-extract-0.cvc
new file mode 100644
index 000000000..7d1a4542c
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-0.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (x[31:0][31:0] = x[31:0]);
diff --git a/test/regress/regress0/bv/core/extract-extract-0.smt b/test/regress/regress0/bv/core/extract-extract-0.smt
new file mode 100644
index 000000000..971ad9e8d
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-0.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(let (?cvc_0 (extract[31:0] x)) (not (= (extract[31:0] ?cvc_0) ?cvc_0)))
+)
diff --git a/test/regress/regress0/bv/core/extract-extract-1.cvc b/test/regress/regress0/bv/core/extract-extract-1.cvc
new file mode 100644
index 000000000..86158e1cb
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-1.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (x[31:0][15:1] = x[15:1]);
diff --git a/test/regress/regress0/bv/core/extract-extract-1.smt b/test/regress/regress0/bv/core/extract-extract-1.smt
new file mode 100644
index 000000000..098e417b9
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-1.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (extract[15:1] (extract[31:0] x)) (extract[15:1] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-extract-10.cvc b/test/regress/regress0/bv/core/extract-extract-10.cvc
new file mode 100644
index 000000000..4710aa65a
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-10.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (x[7:2][2:2] = x[4:4]);
diff --git a/test/regress/regress0/bv/core/extract-extract-10.smt b/test/regress/regress0/bv/core/extract-extract-10.smt
new file mode 100644
index 000000000..d277f5fdb
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-10.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (extract[2:2] (extract[7:2] x)) (extract[4:4] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-extract-11.cvc b/test/regress/regress0/bv/core/extract-extract-11.cvc
new file mode 100644
index 000000000..27c7e1baa
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-11.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (x[30:1][28:2][26:3][23:4][19:5][14:6][8:7][0:0] = x[28:28]);
\ No newline at end of file
diff --git a/test/regress/regress0/bv/core/extract-extract-11.smt b/test/regress/regress0/bv/core/extract-extract-11.smt
new file mode 100644
index 000000000..189c7ef47
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-11.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (extract[0:0] (extract[8:7] (extract[14:6] (extract[19:5] (extract[23:4] (extract[26:3] (extract[28:2] (extract[30:1] x)))))))) (extract[28:28] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-extract-2.cvc b/test/regress/regress0/bv/core/extract-extract-2.cvc
new file mode 100644
index 000000000..fc90ab275
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-2.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (x[31:0][7:2]  = x[7:2]);
diff --git a/test/regress/regress0/bv/core/extract-extract-2.smt b/test/regress/regress0/bv/core/extract-extract-2.smt
new file mode 100644
index 000000000..f423ec9ad
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-2.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (extract[7:2] (extract[31:0] x)) (extract[7:2] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-extract-3.cvc b/test/regress/regress0/bv/core/extract-extract-3.cvc
new file mode 100644
index 000000000..3344c0359
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-3.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (x[31:0][4:4]  = x[4:4]);
diff --git a/test/regress/regress0/bv/core/extract-extract-3.smt b/test/regress/regress0/bv/core/extract-extract-3.smt
new file mode 100644
index 000000000..e614c4c92
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-3.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (extract[4:4] (extract[31:0] x)) (extract[4:4] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-extract-4.cvc b/test/regress/regress0/bv/core/extract-extract-4.cvc
new file mode 100644
index 000000000..0ad43466b
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-4.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (x[15:1][14:0] = x[15:1]);
diff --git a/test/regress/regress0/bv/core/extract-extract-4.smt b/test/regress/regress0/bv/core/extract-extract-4.smt
new file mode 100644
index 000000000..2b9c92946
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-4.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(let (?cvc_0 (extract[15:1] x)) (not (= (extract[14:0] ?cvc_0) ?cvc_0)))
+)
diff --git a/test/regress/regress0/bv/core/extract-extract-5.cvc b/test/regress/regress0/bv/core/extract-extract-5.cvc
new file mode 100644
index 000000000..0d6690527
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-5.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (x[15:1][7:1]  = x[8:2]);
diff --git a/test/regress/regress0/bv/core/extract-extract-5.smt b/test/regress/regress0/bv/core/extract-extract-5.smt
new file mode 100644
index 000000000..0623ce997
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-5.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (extract[7:1] (extract[15:1] x)) (extract[8:2] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-extract-6.cvc b/test/regress/regress0/bv/core/extract-extract-6.cvc
new file mode 100644
index 000000000..4c344f619
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-6.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (x[15:1][3:2]  = x[4:3]);
diff --git a/test/regress/regress0/bv/core/extract-extract-6.smt b/test/regress/regress0/bv/core/extract-extract-6.smt
new file mode 100644
index 000000000..851bd6f68
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-6.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (extract[3:2] (extract[15:1] x)) (extract[4:3] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-extract-7.cvc b/test/regress/regress0/bv/core/extract-extract-7.cvc
new file mode 100644
index 000000000..f911226bc
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-7.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (x[15:1][3:3]  = x[4:4]);
diff --git a/test/regress/regress0/bv/core/extract-extract-7.smt b/test/regress/regress0/bv/core/extract-extract-7.smt
new file mode 100644
index 000000000..e6a2acc13
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-7.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (extract[3:3] (extract[15:1] x)) (extract[4:4] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-extract-8.cvc b/test/regress/regress0/bv/core/extract-extract-8.cvc
new file mode 100644
index 000000000..9b782a70e
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-8.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (x[7:2][5:0] = x[7:2]);
diff --git a/test/regress/regress0/bv/core/extract-extract-8.smt b/test/regress/regress0/bv/core/extract-extract-8.smt
new file mode 100644
index 000000000..7a808f31a
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-8.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(let (?cvc_0 (extract[7:2] x)) (not (= (extract[5:0] ?cvc_0) ?cvc_0)))
+)
diff --git a/test/regress/regress0/bv/core/extract-extract-9.cvc b/test/regress/regress0/bv/core/extract-extract-9.cvc
new file mode 100644
index 000000000..85c0acf49
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-9.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (x[7:2][3:1] = x[5:3]);
diff --git a/test/regress/regress0/bv/core/extract-extract-9.smt b/test/regress/regress0/bv/core/extract-extract-9.smt
new file mode 100644
index 000000000..7a3c8e3da
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-extract-9.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (extract[3:1] (extract[7:2] x)) (extract[5:3] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-whole-0.cvc b/test/regress/regress0/bv/core/extract-whole-0.cvc
new file mode 100644
index 000000000..ea7e991cd
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-whole-0.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (0bin0 @ x[31:31] @ x[30:20] @ x[19:10] @ x[9:1] @ x[0:0] @ 0bin0 = 0bin0 @ x @ 0bin0);
diff --git a/test/regress/regress0/bv/core/extract-whole-0.smt b/test/regress/regress0/bv/core/extract-whole-0.smt
new file mode 100644
index 000000000..83025250f
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-whole-0.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (concat (concat (concat (concat (concat (concat bv0[1] (extract[31:31] x)) (extract[30:20] x)) (extract[19:10] x)) (extract[9:1] x)) (extract[0:0] x)) bv0[1]) (concat (concat bv0[1] x) bv0[1])))
+)
diff --git a/test/regress/regress0/bv/core/extract-whole-1.cvc b/test/regress/regress0/bv/core/extract-whole-1.cvc
new file mode 100644
index 000000000..8115c20b4
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-whole-1.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (x[31:31] @ x[30:20] @ x[19:10] @ x[9:1] @ x[0:0] = x);
diff --git a/test/regress/regress0/bv/core/extract-whole-1.smt b/test/regress/regress0/bv/core/extract-whole-1.smt
new file mode 100644
index 000000000..bc74e0ca9
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-whole-1.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (concat (concat (concat (concat (extract[31:31] x) (extract[30:20] x)) (extract[19:10] x)) (extract[9:1] x)) (extract[0:0] x)) x))
+)
diff --git a/test/regress/regress0/bv/core/extract-whole-2.cvc b/test/regress/regress0/bv/core/extract-whole-2.cvc
new file mode 100644
index 000000000..c6eb38be1
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-whole-2.cvc
@@ -0,0 +1,3 @@
+x : BITVECTOR(32);
+QUERY (x @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 = x @ 0bin010101);
+
diff --git a/test/regress/regress0/bv/core/extract-whole-2.smt b/test/regress/regress0/bv/core/extract-whole-2.smt
new file mode 100644
index 000000000..c661678eb
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-whole-2.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (concat (concat (concat (concat (concat (concat x bv0[1]) bv1[1]) bv0[1]) bv1[1]) bv0[1]) bv1[1]) (concat x bv21[6])))
+)
diff --git a/test/regress/regress0/bv/core/extract-whole-3.cvc b/test/regress/regress0/bv/core/extract-whole-3.cvc
new file mode 100644
index 000000000..689383b7a
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-whole-3.cvc
@@ -0,0 +1,2 @@
+x : BITVECTOR(32);
+QUERY (0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ x = 0bin010101 @ x);
diff --git a/test/regress/regress0/bv/core/extract-whole-3.smt b/test/regress/regress0/bv/core/extract-whole-3.smt
new file mode 100644
index 000000000..2767384af
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-whole-3.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (concat (concat (concat (concat (concat (concat bv0[1] bv1[1]) bv0[1]) bv1[1]) bv0[1]) bv1[1]) x) (concat bv21[6] x)))
+)
diff --git a/test/regress/regress0/bv/core/extract-whole-4.cvc b/test/regress/regress0/bv/core/extract-whole-4.cvc
new file mode 100644
index 000000000..1a3f367a0
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-whole-4.cvc
@@ -0,0 +1,3 @@
+x : BITVECTOR(32);
+QUERY (x[31:0] = x);
+
diff --git a/test/regress/regress0/bv/core/extract-whole-4.smt b/test/regress/regress0/bv/core/extract-whole-4.smt
new file mode 100644
index 000000000..41d2f0594
--- /dev/null
+++ b/test/regress/regress0/bv/core/extract-whole-4.smt
@@ -0,0 +1,6 @@
+(benchmark B_
+  :logic QF_BV
+  :extrafuns ((x BitVec[32]))
+  :formula
+(not (= (extract[31:0] x) x))
+)