From 59cd96a33b8f32405be2a20fc8230efc33b8dcdc Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 9 Dec 2020 03:57:13 -0600
Subject: Remove obsolete regressions (#5633)

This removes benchmarks for the following reasons:

- regress1/arith/arith-int are removed since there are many similar regressions (10 from this set are already enabled)
- bitvector cvc benchmarks are removed since their *.smt2 benchmarks are enabled
- other benchmarks are removed due to features we do not plan to support
- one placeholder benchmark is removed
---
 test/regress/regress0/bv/core/concat-merge-0.cvc     |  3 ---
 test/regress/regress0/bv/core/concat-merge-1.cvc     |  3 ---
 test/regress/regress0/bv/core/concat-merge-2.cvc     |  3 ---
 test/regress/regress0/bv/core/concat-merge-3.cvc     |  3 ---
 test/regress/regress0/bv/core/equality-00.cvc        |  4 ----
 test/regress/regress0/bv/core/equality-01.cvc        |  5 -----
 test/regress/regress0/bv/core/equality-02.cvc        | 15 ---------------
 test/regress/regress0/bv/core/equality-03.cvc        | 10 ----------
 test/regress/regress0/bv/core/equality-03.smtv1.smt2 | 20 --------------------
 test/regress/regress0/bv/core/extract-concat-0.cvc   |  2 --
 test/regress/regress0/bv/core/extract-concat-1.cvc   |  2 --
 test/regress/regress0/bv/core/extract-concat-10.cvc  |  2 --
 test/regress/regress0/bv/core/extract-concat-11.cvc  |  2 --
 test/regress/regress0/bv/core/extract-concat-2.cvc   |  2 --
 test/regress/regress0/bv/core/extract-concat-3.cvc   |  2 --
 test/regress/regress0/bv/core/extract-concat-4.cvc   |  2 --
 test/regress/regress0/bv/core/extract-concat-5.cvc   |  2 --
 test/regress/regress0/bv/core/extract-concat-6.cvc   |  2 --
 test/regress/regress0/bv/core/extract-concat-7.cvc   |  2 --
 test/regress/regress0/bv/core/extract-concat-8.cvc   |  2 --
 test/regress/regress0/bv/core/extract-concat-9.cvc   |  2 --
 test/regress/regress0/bv/core/extract-constant.cvc   |  2 --
 test/regress/regress0/bv/core/extract-extract-0.cvc  |  2 --
 test/regress/regress0/bv/core/extract-extract-1.cvc  |  2 --
 test/regress/regress0/bv/core/extract-extract-10.cvc |  2 --
 test/regress/regress0/bv/core/extract-extract-11.cvc |  2 --
 test/regress/regress0/bv/core/extract-extract-2.cvc  |  2 --
 test/regress/regress0/bv/core/extract-extract-3.cvc  |  2 --
 test/regress/regress0/bv/core/extract-extract-4.cvc  |  2 --
 test/regress/regress0/bv/core/extract-extract-5.cvc  |  2 --
 test/regress/regress0/bv/core/extract-extract-6.cvc  |  2 --
 test/regress/regress0/bv/core/extract-extract-7.cvc  |  2 --
 test/regress/regress0/bv/core/extract-extract-8.cvc  |  2 --
 test/regress/regress0/bv/core/extract-extract-9.cvc  |  2 --
 test/regress/regress0/bv/core/extract-whole-0.cvc    |  2 --
 test/regress/regress0/bv/core/extract-whole-1.cvc    |  2 --
 test/regress/regress0/bv/core/extract-whole-2.cvc    |  3 ---
 test/regress/regress0/bv/core/extract-whole-3.cvc    |  2 --
 test/regress/regress0/bv/core/extract-whole-4.cvc    |  3 ---
 test/regress/regress0/bv/core/slice-01.cvc           |  5 -----
 test/regress/regress0/bv/core/slice-02.cvc           |  5 -----
 test/regress/regress0/bv/core/slice-03.cvc           |  7 -------
 test/regress/regress0/bv/core/slice-04.cvc           | 15 ---------------
 test/regress/regress0/bv/core/slice-05.cvc           | 15 ---------------
 test/regress/regress0/bv/core/slice-06.cvc           | 15 ---------------
 test/regress/regress0/bv/core/slice-07.cvc           |  4 ----
 test/regress/regress0/bv/core/slice-08.cvc           |  4 ----
 test/regress/regress0/bv/core/slice-09.cvc           |  4 ----
 test/regress/regress0/bv/core/slice-10.cvc           |  5 -----
 test/regress/regress0/bv/core/slice-11.cvc           |  4 ----
 test/regress/regress0/bv/core/slice-12.cvc           |  8 --------
 test/regress/regress0/bv/core/slice-13.cvc           |  8 --------
 test/regress/regress0/bv/core/slice-14.cvc           |  5 -----
 test/regress/regress0/bv/core/slice-15.cvc           |  5 -----
 test/regress/regress0/bv/core/slice-16.cvc           |  5 -----
 test/regress/regress0/bv/core/slice-17.cvc           |  8 --------
 test/regress/regress0/bv/core/slice-18.cvc           |  8 --------
 test/regress/regress0/bv/core/slice-19.cvc           |  8 --------
 test/regress/regress0/bv/core/slice-20.cvc           | 13 -------------
 .../regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2    |  1 -
 60 files changed, 280 deletions(-)
 delete mode 100644 test/regress/regress0/bv/core/concat-merge-0.cvc
 delete mode 100644 test/regress/regress0/bv/core/concat-merge-1.cvc
 delete mode 100644 test/regress/regress0/bv/core/concat-merge-2.cvc
 delete mode 100644 test/regress/regress0/bv/core/concat-merge-3.cvc
 delete mode 100644 test/regress/regress0/bv/core/equality-00.cvc
 delete mode 100644 test/regress/regress0/bv/core/equality-01.cvc
 delete mode 100644 test/regress/regress0/bv/core/equality-02.cvc
 delete mode 100644 test/regress/regress0/bv/core/equality-03.cvc
 delete mode 100644 test/regress/regress0/bv/core/equality-03.smtv1.smt2
 delete mode 100644 test/regress/regress0/bv/core/extract-concat-0.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-concat-1.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-concat-10.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-concat-11.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-concat-2.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-concat-3.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-concat-4.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-concat-5.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-concat-6.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-concat-7.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-concat-8.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-concat-9.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-constant.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-extract-0.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-extract-1.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-extract-10.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-extract-11.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-extract-2.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-extract-3.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-extract-4.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-extract-5.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-extract-6.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-extract-7.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-extract-8.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-extract-9.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-whole-0.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-whole-1.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-whole-2.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-whole-3.cvc
 delete mode 100644 test/regress/regress0/bv/core/extract-whole-4.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-01.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-02.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-03.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-04.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-05.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-06.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-07.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-08.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-09.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-10.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-11.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-12.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-13.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-14.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-15.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-16.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-17.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-18.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-19.cvc
 delete mode 100644 test/regress/regress0/bv/core/slice-20.cvc
 delete mode 100644 test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2

(limited to 'test/regress/regress0')

diff --git a/test/regress/regress0/bv/core/concat-merge-0.cvc b/test/regress/regress0/bv/core/concat-merge-0.cvc
deleted file mode 100644
index 60341c03b..000000000
--- a/test/regress/regress0/bv/core/concat-merge-0.cvc
+++ /dev/null
@@ -1,3 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[2:1]   @ x[0:0]  = x[2:0] );
-
diff --git a/test/regress/regress0/bv/core/concat-merge-1.cvc b/test/regress/regress0/bv/core/concat-merge-1.cvc
deleted file mode 100644
index af0e8387b..000000000
--- a/test/regress/regress0/bv/core/concat-merge-1.cvc
+++ /dev/null
@@ -1,3 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[4:2]   @ x[1:0]  = x[4:0] );
-
diff --git a/test/regress/regress0/bv/core/concat-merge-2.cvc b/test/regress/regress0/bv/core/concat-merge-2.cvc
deleted file mode 100644
index 8ad7f2aa3..000000000
--- a/test/regress/regress0/bv/core/concat-merge-2.cvc
+++ /dev/null
@@ -1,3 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[8:4]   @ x[3:0]  = x[8:0] );
-
diff --git a/test/regress/regress0/bv/core/concat-merge-3.cvc b/test/regress/regress0/bv/core/concat-merge-3.cvc
deleted file mode 100644
index d46da1a55..000000000
--- a/test/regress/regress0/bv/core/concat-merge-3.cvc
+++ /dev/null
@@ -1,3 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[16:8]  @ x[7:0]  = x[16:0]);
-
diff --git a/test/regress/regress0/bv/core/equality-00.cvc b/test/regress/regress0/bv/core/equality-00.cvc
deleted file mode 100644
index e02c616ad..000000000
--- a/test/regress/regress0/bv/core/equality-00.cvc
+++ /dev/null
@@ -1,4 +0,0 @@
-x, y, z : BITVECTOR(32);
-ASSERT(x = y);
-ASSERT(y = z);
-QUERY(x = z);
\ No newline at end of file
diff --git a/test/regress/regress0/bv/core/equality-01.cvc b/test/regress/regress0/bv/core/equality-01.cvc
deleted file mode 100644
index e56af23dd..000000000
--- a/test/regress/regress0/bv/core/equality-01.cvc
+++ /dev/null
@@ -1,5 +0,0 @@
-x, y, z, w: BITVECTOR(32);
-ASSERT(x = y);
-ASSERT(y = z);
-ASSERT(z = w);
-QUERY(x = w);
\ No newline at end of file
diff --git a/test/regress/regress0/bv/core/equality-02.cvc b/test/regress/regress0/bv/core/equality-02.cvc
deleted file mode 100644
index e8f51d61a..000000000
--- a/test/regress/regress0/bv/core/equality-02.cvc
+++ /dev/null
@@ -1,15 +0,0 @@
-x0, x1, x2, x3 : BITVECTOR(32);
-y0, y1, y2, y3 : BITVECTOR(32);
-
-ASSERT (x0 = x1);
-ASSERT (x1 = x2);
-ASSERT (x2 = x3);
-
-ASSERT (y0 = y1);
-ASSERT (y1 = y2);
-ASSERT (y2 = y3);
-
-ASSERT (x0 = y0);
-
-QUERY (x3 = y3);
-
diff --git a/test/regress/regress0/bv/core/equality-03.cvc b/test/regress/regress0/bv/core/equality-03.cvc
deleted file mode 100644
index d2f18682c..000000000
--- a/test/regress/regress0/bv/core/equality-03.cvc
+++ /dev/null
@@ -1,10 +0,0 @@
-x0, x1, x2: BITVECTOR(32);
-y0, y1, y2: BITVECTOR(32);
-a0, a1, a2, a3 : BITVECTOR(32);
-
-ASSERT (a0 = x0 AND x0 = a1) XOR (a0 = y0 AND y0 = a1);
-ASSERT (a1 = x1 AND x1 = a2) XOR (a1 = y1 AND y1 = a2);
-ASSERT (a2 = x2 AND x2 = a3) XOR (a2 = y2 AND y2 = a3);
-
-QUERY (a0 = a3);
-
diff --git a/test/regress/regress0/bv/core/equality-03.smtv1.smt2 b/test/regress/regress0/bv/core/equality-03.smtv1.smt2
deleted file mode 100644
index e31d17a83..000000000
--- a/test/regress/regress0/bv/core/equality-03.smtv1.smt2
+++ /dev/null
@@ -1,20 +0,0 @@
-(set-option :incremental false)
-(set-info :source "Source unknown")
-(set-info :status unknown)
-(set-info :difficulty "unknown")
-(set-info :category "unknown")
-(set-logic QF_BV)
-(declare-fun x0 () (_ BitVec 32))
-(declare-fun x1 () (_ BitVec 32))
-(declare-fun x2 () (_ BitVec 32))
-(declare-fun y0 () (_ BitVec 32))
-(declare-fun y1 () (_ BitVec 32))
-(declare-fun y2 () (_ BitVec 32))
-(declare-fun a0 () (_ BitVec 32))
-(declare-fun a1 () (_ BitVec 32))
-(declare-fun a2 () (_ BitVec 32))
-(declare-fun a3 () (_ BitVec 32))
-(assert (xor (and (= a0 x0) (= x0 a1)) (and (= a0 y0) (= y0 a1))))
-(assert (xor (and (= a1 x1) (= x1 a2)) (and (= a1 y1) (= y1 a2))))
-(assert (xor (and (= a2 x2) (= x2 a3)) (and (= a2 y2) (= y2 a3))))
-(check-sat-assuming ( (not (= a0 a3)) ))
diff --git a/test/regress/regress0/bv/core/extract-concat-0.cvc b/test/regress/regress0/bv/core/extract-concat-0.cvc
deleted file mode 100644
index 9aa608265..000000000
--- a/test/regress/regress0/bv/core/extract-concat-0.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[63:32] = x[31:0]);
diff --git a/test/regress/regress0/bv/core/extract-concat-1.cvc b/test/regress/regress0/bv/core/extract-concat-1.cvc
deleted file mode 100644
index e192f159c..000000000
--- a/test/regress/regress0/bv/core/extract-concat-1.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[62:33] = x[30:1]);
diff --git a/test/regress/regress0/bv/core/extract-concat-10.cvc b/test/regress/regress0/bv/core/extract-concat-10.cvc
deleted file mode 100644
index 8d3b88fba..000000000
--- a/test/regress/regress0/bv/core/extract-concat-10.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-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-11.cvc b/test/regress/regress0/bv/core/extract-concat-11.cvc
deleted file mode 100644
index 2290eef04..000000000
--- a/test/regress/regress0/bv/core/extract-concat-11.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-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-2.cvc b/test/regress/regress0/bv/core/extract-concat-2.cvc
deleted file mode 100644
index bd1e3ff30..000000000
--- a/test/regress/regress0/bv/core/extract-concat-2.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[61:34] = x[29:2]);
diff --git a/test/regress/regress0/bv/core/extract-concat-3.cvc b/test/regress/regress0/bv/core/extract-concat-3.cvc
deleted file mode 100644
index 4e225be42..000000000
--- a/test/regress/regress0/bv/core/extract-concat-3.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[60:35] = x[28:3]);
diff --git a/test/regress/regress0/bv/core/extract-concat-4.cvc b/test/regress/regress0/bv/core/extract-concat-4.cvc
deleted file mode 100644
index 8ecf96e6f..000000000
--- a/test/regress/regress0/bv/core/extract-concat-4.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[31:0] = y[31:0]);
diff --git a/test/regress/regress0/bv/core/extract-concat-5.cvc b/test/regress/regress0/bv/core/extract-concat-5.cvc
deleted file mode 100644
index 378ca5d2a..000000000
--- a/test/regress/regress0/bv/core/extract-concat-5.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[30:1] = y[30:1]);
diff --git a/test/regress/regress0/bv/core/extract-concat-6.cvc b/test/regress/regress0/bv/core/extract-concat-6.cvc
deleted file mode 100644
index 41499b55b..000000000
--- a/test/regress/regress0/bv/core/extract-concat-6.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[29:2] = y[29:2]);
diff --git a/test/regress/regress0/bv/core/extract-concat-7.cvc b/test/regress/regress0/bv/core/extract-concat-7.cvc
deleted file mode 100644
index 838017f55..000000000
--- a/test/regress/regress0/bv/core/extract-concat-7.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[28:3] = y[28:3]);
diff --git a/test/regress/regress0/bv/core/extract-concat-8.cvc b/test/regress/regress0/bv/core/extract-concat-8.cvc
deleted file mode 100644
index 68982b0a6..000000000
--- a/test/regress/regress0/bv/core/extract-concat-8.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-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-9.cvc b/test/regress/regress0/bv/core/extract-concat-9.cvc
deleted file mode 100644
index 5f0e690cb..000000000
--- a/test/regress/regress0/bv/core/extract-concat-9.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x, y : BITVECTOR(32);
-QUERY ((x @ y)[61:2] = x[29:0] @ y[31:2]);
diff --git a/test/regress/regress0/bv/core/extract-constant.cvc b/test/regress/regress0/bv/core/extract-constant.cvc
deleted file mode 100644
index e70ccbf5e..000000000
--- a/test/regress/regress0/bv/core/extract-constant.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-QUERY (0bin000111000[6:2] = 0bin01110);
-
diff --git a/test/regress/regress0/bv/core/extract-extract-0.cvc b/test/regress/regress0/bv/core/extract-extract-0.cvc
deleted file mode 100644
index 7d1a4542c..000000000
--- a/test/regress/regress0/bv/core/extract-extract-0.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[31:0][31:0] = x[31:0]);
diff --git a/test/regress/regress0/bv/core/extract-extract-1.cvc b/test/regress/regress0/bv/core/extract-extract-1.cvc
deleted file mode 100644
index 86158e1cb..000000000
--- a/test/regress/regress0/bv/core/extract-extract-1.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[31:0][15:1] = x[15:1]);
diff --git a/test/regress/regress0/bv/core/extract-extract-10.cvc b/test/regress/regress0/bv/core/extract-extract-10.cvc
deleted file mode 100644
index 4710aa65a..000000000
--- a/test/regress/regress0/bv/core/extract-extract-10.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[7:2][2:2] = x[4:4]);
diff --git a/test/regress/regress0/bv/core/extract-extract-11.cvc b/test/regress/regress0/bv/core/extract-extract-11.cvc
deleted file mode 100644
index 27c7e1baa..000000000
--- a/test/regress/regress0/bv/core/extract-extract-11.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-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-2.cvc b/test/regress/regress0/bv/core/extract-extract-2.cvc
deleted file mode 100644
index fc90ab275..000000000
--- a/test/regress/regress0/bv/core/extract-extract-2.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[31:0][7:2]  = x[7:2]);
diff --git a/test/regress/regress0/bv/core/extract-extract-3.cvc b/test/regress/regress0/bv/core/extract-extract-3.cvc
deleted file mode 100644
index 3344c0359..000000000
--- a/test/regress/regress0/bv/core/extract-extract-3.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[31:0][4:4]  = x[4:4]);
diff --git a/test/regress/regress0/bv/core/extract-extract-4.cvc b/test/regress/regress0/bv/core/extract-extract-4.cvc
deleted file mode 100644
index 0ad43466b..000000000
--- a/test/regress/regress0/bv/core/extract-extract-4.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[15:1][14:0] = x[15:1]);
diff --git a/test/regress/regress0/bv/core/extract-extract-5.cvc b/test/regress/regress0/bv/core/extract-extract-5.cvc
deleted file mode 100644
index 0d6690527..000000000
--- a/test/regress/regress0/bv/core/extract-extract-5.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[15:1][7:1]  = x[8:2]);
diff --git a/test/regress/regress0/bv/core/extract-extract-6.cvc b/test/regress/regress0/bv/core/extract-extract-6.cvc
deleted file mode 100644
index 4c344f619..000000000
--- a/test/regress/regress0/bv/core/extract-extract-6.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[15:1][3:2]  = x[4:3]);
diff --git a/test/regress/regress0/bv/core/extract-extract-7.cvc b/test/regress/regress0/bv/core/extract-extract-7.cvc
deleted file mode 100644
index f911226bc..000000000
--- a/test/regress/regress0/bv/core/extract-extract-7.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[15:1][3:3]  = x[4:4]);
diff --git a/test/regress/regress0/bv/core/extract-extract-8.cvc b/test/regress/regress0/bv/core/extract-extract-8.cvc
deleted file mode 100644
index 9b782a70e..000000000
--- a/test/regress/regress0/bv/core/extract-extract-8.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[7:2][5:0] = x[7:2]);
diff --git a/test/regress/regress0/bv/core/extract-extract-9.cvc b/test/regress/regress0/bv/core/extract-extract-9.cvc
deleted file mode 100644
index 85c0acf49..000000000
--- a/test/regress/regress0/bv/core/extract-extract-9.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[7:2][3:1] = x[5:3]);
diff --git a/test/regress/regress0/bv/core/extract-whole-0.cvc b/test/regress/regress0/bv/core/extract-whole-0.cvc
deleted file mode 100644
index ea7e991cd..000000000
--- a/test/regress/regress0/bv/core/extract-whole-0.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-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-1.cvc b/test/regress/regress0/bv/core/extract-whole-1.cvc
deleted file mode 100644
index 8115c20b4..000000000
--- a/test/regress/regress0/bv/core/extract-whole-1.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-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-2.cvc b/test/regress/regress0/bv/core/extract-whole-2.cvc
deleted file mode 100644
index c6eb38be1..000000000
--- a/test/regress/regress0/bv/core/extract-whole-2.cvc
+++ /dev/null
@@ -1,3 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 = x @ 0bin010101);
-
diff --git a/test/regress/regress0/bv/core/extract-whole-3.cvc b/test/regress/regress0/bv/core/extract-whole-3.cvc
deleted file mode 100644
index 689383b7a..000000000
--- a/test/regress/regress0/bv/core/extract-whole-3.cvc
+++ /dev/null
@@ -1,2 +0,0 @@
-x : BITVECTOR(32);
-QUERY (0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ 0bin0 @ 0bin1 @ x = 0bin010101 @ x);
diff --git a/test/regress/regress0/bv/core/extract-whole-4.cvc b/test/regress/regress0/bv/core/extract-whole-4.cvc
deleted file mode 100644
index 1a3f367a0..000000000
--- a/test/regress/regress0/bv/core/extract-whole-4.cvc
+++ /dev/null
@@ -1,3 +0,0 @@
-x : BITVECTOR(32);
-QUERY (x[31:0] = x);
-
diff --git a/test/regress/regress0/bv/core/slice-01.cvc b/test/regress/regress0/bv/core/slice-01.cvc
deleted file mode 100644
index e27f1c902..000000000
--- a/test/regress/regress0/bv/core/slice-01.cvc
+++ /dev/null
@@ -1,5 +0,0 @@
-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-02.cvc b/test/regress/regress0/bv/core/slice-02.cvc
deleted file mode 100644
index 35eb43d55..000000000
--- a/test/regress/regress0/bv/core/slice-02.cvc
+++ /dev/null
@@ -1,5 +0,0 @@
-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-03.cvc b/test/regress/regress0/bv/core/slice-03.cvc
deleted file mode 100644
index 51fb1983c..000000000
--- a/test/regress/regress0/bv/core/slice-03.cvc
+++ /dev/null
@@ -1,7 +0,0 @@
-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-04.cvc b/test/regress/regress0/bv/core/slice-04.cvc
deleted file mode 100644
index 97e5b0b57..000000000
--- a/test/regress/regress0/bv/core/slice-04.cvc
+++ /dev/null
@@ -1,15 +0,0 @@
-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-05.cvc b/test/regress/regress0/bv/core/slice-05.cvc
deleted file mode 100644
index 30fe1ed35..000000000
--- a/test/regress/regress0/bv/core/slice-05.cvc
+++ /dev/null
@@ -1,15 +0,0 @@
-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-06.cvc b/test/regress/regress0/bv/core/slice-06.cvc
deleted file mode 100644
index 554e65567..000000000
--- a/test/regress/regress0/bv/core/slice-06.cvc
+++ /dev/null
@@ -1,15 +0,0 @@
-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-07.cvc b/test/regress/regress0/bv/core/slice-07.cvc
deleted file mode 100644
index 134037a40..000000000
--- a/test/regress/regress0/bv/core/slice-07.cvc
+++ /dev/null
@@ -1,4 +0,0 @@
-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-08.cvc b/test/regress/regress0/bv/core/slice-08.cvc
deleted file mode 100644
index bf5222844..000000000
--- a/test/regress/regress0/bv/core/slice-08.cvc
+++ /dev/null
@@ -1,4 +0,0 @@
-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-09.cvc b/test/regress/regress0/bv/core/slice-09.cvc
deleted file mode 100644
index 43876c923..000000000
--- a/test/regress/regress0/bv/core/slice-09.cvc
+++ /dev/null
@@ -1,4 +0,0 @@
-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-10.cvc b/test/regress/regress0/bv/core/slice-10.cvc
deleted file mode 100644
index 953d41ec2..000000000
--- a/test/regress/regress0/bv/core/slice-10.cvc
+++ /dev/null
@@ -1,5 +0,0 @@
-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-11.cvc b/test/regress/regress0/bv/core/slice-11.cvc
deleted file mode 100644
index 0fc79c13e..000000000
--- a/test/regress/regress0/bv/core/slice-11.cvc
+++ /dev/null
@@ -1,4 +0,0 @@
-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-12.cvc b/test/regress/regress0/bv/core/slice-12.cvc
deleted file mode 100644
index 7d0d79336..000000000
--- a/test/regress/regress0/bv/core/slice-12.cvc
+++ /dev/null
@@ -1,8 +0,0 @@
-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-13.cvc b/test/regress/regress0/bv/core/slice-13.cvc
deleted file mode 100644
index 0c3e82f97..000000000
--- a/test/regress/regress0/bv/core/slice-13.cvc
+++ /dev/null
@@ -1,8 +0,0 @@
-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-14.cvc b/test/regress/regress0/bv/core/slice-14.cvc
deleted file mode 100644
index 286f948de..000000000
--- a/test/regress/regress0/bv/core/slice-14.cvc
+++ /dev/null
@@ -1,5 +0,0 @@
-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-15.cvc b/test/regress/regress0/bv/core/slice-15.cvc
deleted file mode 100644
index 076a54790..000000000
--- a/test/regress/regress0/bv/core/slice-15.cvc
+++ /dev/null
@@ -1,5 +0,0 @@
-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-16.cvc b/test/regress/regress0/bv/core/slice-16.cvc
deleted file mode 100644
index 8a5b4bab9..000000000
--- a/test/regress/regress0/bv/core/slice-16.cvc
+++ /dev/null
@@ -1,5 +0,0 @@
-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-17.cvc b/test/regress/regress0/bv/core/slice-17.cvc
deleted file mode 100644
index 1f2a44423..000000000
--- a/test/regress/regress0/bv/core/slice-17.cvc
+++ /dev/null
@@ -1,8 +0,0 @@
-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-18.cvc b/test/regress/regress0/bv/core/slice-18.cvc
deleted file mode 100644
index 99f4707d8..000000000
--- a/test/regress/regress0/bv/core/slice-18.cvc
+++ /dev/null
@@ -1,8 +0,0 @@
-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-19.cvc b/test/regress/regress0/bv/core/slice-19.cvc
deleted file mode 100644
index 0f76359b8..000000000
--- a/test/regress/regress0/bv/core/slice-19.cvc
+++ /dev/null
@@ -1,8 +0,0 @@
-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-20.cvc b/test/regress/regress0/bv/core/slice-20.cvc
deleted file mode 100644
index a211b5f2e..000000000
--- a/test/regress/regress0/bv/core/slice-20.cvc
+++ /dev/null
@@ -1,13 +0,0 @@
-x1, y1: BITVECTOR(4);
-x2, y2: BITVECTOR(2);
-x3, y3: BITVECTOR(1);
-
-ASSERT(x1 = y1);
-
-ASSERT(x1 = x2 @ x2);
-ASSERT(x2 = x3 @ x3);
-
-ASSERT(y1 = y2 @ y2);
-ASSERT(y2 = y3 @ y3);
-
-QUERY(x3 = y3);
\ No newline at end of file
diff --git a/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 b/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2
deleted file mode 100644
index 70c0057f9..000000000
--- a/test/regress/regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2
+++ /dev/null
@@ -1 +0,0 @@
-; PLACEHOLDER: benchmark to be added
-- 
cgit v1.2.3