Move slow regress0 benchmarks to regress1, increment regress1 through regress3.

104 files changed, 111 insertions, 101 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 45842065f..c790165ef 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -147,16 +147,13 @@ BUG_TESTS = \
 	bug398.smt2 \
 	bug421.smt2 \
 	bug421b.smt2 \
-	bug425.cvc \
 	bug480.smt2 \
 	bug484.smt2 \
 	bug486.cvc \
 	bug507.smt2 \
 	bug512.minimized.smt2 \
 	bug516.smt2 \
-	bug519.smt2 \
 	bug520.smt2 \
-	bug521.smt2 \
 	bug521.minimized.smt2 \
 	bug522.smt2 \
 	bug528a.smt2 \
diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am
index 38705c22a..d88128e72 100644
--- a/test/regress/regress0/aufbv/Makefile.am
+++ b/test/regress/regress0/aufbv/Makefile.am
@@ -48,7 +48,6 @@ TESTS =	\
 	fuzz07.smt \
 	fuzz08.smt \
 	fuzz09.smt \
-	fuzz10.smt \
 	fuzz11.smt \
 	fuzz12.smt \
 	fuzz13.smt \
diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index d182539bc..82ea731d4 100644
--- a/test/regress/regress0/auflia/Makefile.am
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -19,7 +19,6 @@ MAKEFLAGS = -k
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =	\
-        bug330.smt2 \
 	bug336.smt2 \
 	fuzz01.delta01.smt \
 	fuzz02.smt \
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index d85b3d109..0b99024eb 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -78,7 +78,6 @@ SMT_TESTS = \
 	fuzz33.delta01.smt \
 	fuzz33.smt \
 	fuzz34.delta01.smt \
-	fuzz34.smt \
 	fuzz35.delta01.smt \
 	fuzz35.smt \
 	fuzz36.delta01.smt \
@@ -86,7 +85,6 @@ SMT_TESTS = \
 	fuzz37.delta01.smt \
 	fuzz37.smt \
 	fuzz38.delta01.smt \
-	fuzz38.smt \
 	fuzz39.delta01.smt \
 	fuzz39.smt \
 	fuzz40.delta01.smt \
@@ -95,8 +93,7 @@ SMT_TESTS = \
 	calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt \
 	smtcompbug.smt \
 	unsound1.smt2 \
-	unsound1-reduced.smt2 \
-	bv-proof00.smt
+	unsound1-reduced.smt2
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS = divtest.smt2
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 350a948aa..c177129b4 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -64,7 +64,6 @@ TESTS =	\
 	cdt-non-canon-stream.smt2 \
 	stream-singleton.smt2 \
 	is_test.smt2 \
-	manos-model.smt2 \
 	bug625.smt2 \
 	cdt-model-cade15.smt2 \
 	sc-cdt1.smt2  \
diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index 90a18f0e2..6aea21f3f 100644
--- a/test/regress/regress0/decision/Makefile.am
+++ b/test/regress/regress0/decision/Makefile.am
@@ -34,7 +34,6 @@ TESTS =	\
 	error20.delta01.smt \
 	error122.smt \
 	error122.delta01.smt \
-	error3.smt \
 	error3.delta01.smt \
 	pp-regfile.delta01.smt \
 	pp-regfile.delta02.smt
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index b7daadfd1..c10b3c668 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -53,7 +53,6 @@ TESTS =	\
 	nun-0208-to.smt2 \
 	datatypes-ufinite.smt2 \
 	datatypes-ufinite-nested.smt2 \
-	ForElimination-scala-9.smt2 \
 	agree466.smt2 \
 	LeftistHeap.scala-8-ncm.smt2 \
 	sc-crash-052316.smt2 \
diff --git a/test/regress/regress0/lemmas/Makefile.am b/test/regress/regress0/lemmas/Makefile.am
index 9ede6d4c0..26610304a 100644
--- a/test/regress/regress0/lemmas/Makefile.am
+++ b/test/regress/regress0/lemmas/Makefile.am
@@ -25,11 +25,8 @@ MAKEFLAGS = -k
 SMT_TESTS = \
 	clocksynchro_5clocks.main_invar.base.model.smt \
 	sc_init_frame_gap.induction.smt \
-	clocksynchro_5clocks.main_invar.base.smt \
 	mode_cntrl.induction.smt \
-	fs_not_sc_seen.induction.smt \
-	pursuit-safety-8.smt \
-	simple_startup_9nodes.abstract.base.smt
+	fs_not_sc_seen.induction.smt
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am
index 31f99905c..3224563ab 100644
--- a/test/regress/regress0/rewriterules/Makefile.am
+++ b/test/regress/regress0/rewriterules/Makefile.am
@@ -26,11 +26,9 @@ TESTS =	\
 	length_gen_020.smt2 \
 	datatypes.smt2 \
 	datatypes_sat.smt2 \
-	reachability_back_to_the_future.smt2 \
 	relation.smt2 \
 	simulate_rewriting.smt2 \
-	native_arrays.smt2 \
-	read5.smt2
+	native_arrays.smt2 
 
 # length_trick2.smt2 reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2
 
diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
index b43a9a570..d7bfa2d57 100644
--- a/test/regress/regress0/sep/Makefile.am
+++ b/test/regress/regress0/sep/Makefile.am
@@ -33,20 +33,16 @@ TESTS =	\
   nspatial-simp.smt2 \
   sep-neg-1refine.smt2 \
   sep-neg-simple.smt2 \
-  sep-simp-unc.smt2 \
   sep-simp-unsat-emp.smt2 \
   simple-neg-sat.smt2 \
   wand-simp-sat.smt2 \
   wand-simp-sat2.smt2 \
   wand-simp-unsat.smt2 \
   sep-nterm-again.smt2 \
-  split-find-unsat.smt2 \
-  split-find-unsat-w-emp.smt2 \
   nemp.smt2 \
   wand-crash.smt2 \
   wand-nterm-simp.smt2 \
   wand-nterm-simp2.smt2 \
-  loop-1220.smt2 \
   chain-int.smt2 \
   sep-neg-swap.smt2 \
   sep-neg-nstrict2.smt2 \
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 2f36cc188..9c970c45a 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -50,7 +50,6 @@ TESTS =	\
 	fuzz15201.smt2 \
 	fuzz31811.smt2 \
 	rec_copy_loop_check_heap_access_43_4.smt2 \
-	sets-disequal.smt2 \
 	sets-equal.smt2 \
 	sets-inter.smt2 \
 	sets-sample.smt2 \
@@ -64,8 +63,7 @@ TESTS =	\
 	union-1b.smt2 \
 	union-2.smt2 \
 	dt-simp-mem.smt2 \
-	card3-ground.smt2 \
-	card-vc6-minimized.smt2
+	card3-ground.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 2e4fd4e1c..88f3763e1 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -79,8 +79,6 @@ TESTS = \
   cmu-2db2-extf-reg.smt2 \
   norn-nel-bug-052116.smt2 \
   cmu-disagree-0707-dd.smt2 \
-  cmu-5042-0707-2.smt2 \
-  cmu-dis-0707-3.smt2 \
   nf-ff-contains-abs.smt2  \
   csp-prefix-exp-bug.smt2 \
   cmu-substr-rw.smt2 \
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index b503a65b8..695c52cc6 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -50,8 +50,7 @@ TESTS = commutative.sy \
         no-mention.sy \
         max2-univ.sy \
         strings-small.sy \
-        strings-unconstrained.sy \
-        hd-sdiv.sy
+        strings-unconstrained.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
index 5f292b893..c399a797f 100644
--- a/test/regress/regress1/Makefile.am
+++ b/test/regress/regress1/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . arith
+SUBDIRS = . bv aufbv auflia datatypes rewriterules lemmas decision fmf strings sets sygus sep
 
 # don't override a BINARY imported from a personal.mk
 @mk_if@eq ($(BINARY),)
@@ -20,50 +20,16 @@ MAKEFLAGS = -k
 # These are run for all build profiles.
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
-TESTS =	bug136.smt \
-	bug148.smt \
-	bug394.smt2 \
-	DTP_k2_n35_c175_s15.smt2 \
-	GEO123+1.minimized.smt2 \
-	error1.smt \
-	friedman_n4_i5.smt \
-	hole7.cvc \
-	hole8.cvc \
-	instance_1444.smt \
-	fuzz_2.smt \
-	hash_sat_10_09.smt2 \
-	hash_sat_07_17.smt2 \
-	ooo.tag10.smt2 \
-	hash_sat_06_19.smt2 \
-	hash_sat_09_09.smt2 \
-	ooo.rf6.smt2 \
-	auflia-fuzz06.smt \
-	piVC_5581bd.smt2 \
-	typed_v1l50016-simp.cvc \
-	FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 \
-	xs-09-16-3-4-1-5.smt \
-	xs-09-16-3-4-1-5.decn.smt \
-	uflia-error0.smt2
-
-EXTRA_DIST = $(TESTS) \
-	FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect \
-	uflia-error0.smt2.expect \
-	xs-09-16-3-4-1-5.decn.smt.expect
-
-#if CVC4_BUILD_PROFILE_COMPETITION
-#else
-#TESTS += \
-#	error.cvc
-#endif
-#
-# and make sure to distribute it
-#EXTRA_DIST += \
-#	error.cvc
+TESTS =	bug425.cvc \
+  bug519.smt2 \
+  bug521.smt2
+  
+EXTRA_DIST = $(TESTS)
 
 # synonyms for "check" in this directory
 .PHONY: regress regress1 test
 regress regress1 test: check
 
 # do nothing in this subdir
-.PHONY: regress0 regress2 regress3
-regress0 regress2 regress3:
+.PHONY: regress0 regress2 regress3 regress4
+regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress0/aufbv/fuzz10.smt b/test/regress/regress1/aufbv/fuzz10.smt
index b838f80f0..b838f80f0 100644
--- a/test/regress/regress0/aufbv/fuzz10.smt
+++ b/test/regress/regress1/aufbv/fuzz10.smt
diff --git a/test/regress/regress0/auflia/bug330.smt2 b/test/regress/regress1/auflia/bug330.smt2
index d05a8b2a0..d05a8b2a0 100644
--- a/test/regress/regress0/auflia/bug330.smt2
+++ b/test/regress/regress1/auflia/bug330.smt2
diff --git a/test/regress/regress0/bug425.cvc b/test/regress/regress1/bug425.cvc
index 5b6464c32..5b6464c32 100644
--- a/test/regress/regress0/bug425.cvc
+++ b/test/regress/regress1/bug425.cvc
diff --git a/test/regress/regress0/bug519.smt2 b/test/regress/regress1/bug519.smt2
index 72ec634a8..72ec634a8 100644
--- a/test/regress/regress0/bug519.smt2
+++ b/test/regress/regress1/bug519.smt2
diff --git a/test/regress/regress0/bug521.smt2 b/test/regress/regress1/bug521.smt2
index 8f840a1f6..8f840a1f6 100644
--- a/test/regress/regress0/bug521.smt2
+++ b/test/regress/regress1/bug521.smt2
diff --git a/test/regress/regress0/bv/bv-proof00.smt b/test/regress/regress1/bv/bv-proof00.smt
index adfebf58e..adfebf58e 100644
--- a/test/regress/regress0/bv/bv-proof00.smt
+++ b/test/regress/regress1/bv/bv-proof00.smt
diff --git a/test/regress/regress0/bv/fuzz34.smt b/test/regress/regress1/bv/fuzz34.smt
index 200bed99f..200bed99f 100644
--- a/test/regress/regress0/bv/fuzz34.smt
+++ b/test/regress/regress1/bv/fuzz34.smt
diff --git a/test/regress/regress0/bv/fuzz38.smt b/test/regress/regress1/bv/fuzz38.smt
index 39ebe9e42..39ebe9e42 100644
--- a/test/regress/regress0/bv/fuzz38.smt
+++ b/test/regress/regress1/bv/fuzz38.smt
diff --git a/test/regress/regress0/datatypes/manos-model.smt2 b/test/regress/regress1/datatypes/manos-model.smt2
index 4ade71151..4ade71151 100644
--- a/test/regress/regress0/datatypes/manos-model.smt2
+++ b/test/regress/regress1/datatypes/manos-model.smt2
diff --git a/test/regress/regress0/decision/error3.smt b/test/regress/regress1/decision/error3.smt
index 36c409f3f..36c409f3f 100644
--- a/test/regress/regress0/decision/error3.smt
+++ b/test/regress/regress1/decision/error3.smt
diff --git a/test/regress/regress0/fmf/ForElimination-scala-9.smt2 b/test/regress/regress1/fmf/ForElimination-scala-9.smt2
index 36bb915f4..36bb915f4 100644
--- a/test/regress/regress0/fmf/ForElimination-scala-9.smt2
+++ b/test/regress/regress1/fmf/ForElimination-scala-9.smt2
diff --git a/test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt b/test/regress/regress1/lemmas/clocksynchro_5clocks.main_invar.base.smt
index 92cc1b080..92cc1b080 100644
--- a/test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt
+++ b/test/regress/regress1/lemmas/clocksynchro_5clocks.main_invar.base.smt
diff --git a/test/regress/regress0/lemmas/pursuit-safety-8.smt b/test/regress/regress1/lemmas/pursuit-safety-8.smt
index 5985c500b..5985c500b 100644
--- a/test/regress/regress0/lemmas/pursuit-safety-8.smt
+++ b/test/regress/regress1/lemmas/pursuit-safety-8.smt
diff --git a/test/regress/regress0/lemmas/simple_startup_9nodes.abstract.base.smt b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt
index 506b99b46..506b99b46 100644
--- a/test/regress/regress0/lemmas/simple_startup_9nodes.abstract.base.smt
+++ b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt
diff --git a/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2 b/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2
index 13f7234e9..13f7234e9 100644
--- a/test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2
+++ b/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2
diff --git a/test/regress/regress0/rewriterules/read5.smt2 b/test/regress/regress1/rewriterules/read5.smt2
index e66df7c7e..e66df7c7e 100644
--- a/test/regress/regress0/rewriterules/read5.smt2
+++ b/test/regress/regress1/rewriterules/read5.smt2
diff --git a/test/regress/regress0/sep/loop-1220.smt2 b/test/regress/regress1/sep/loop-1220.smt2
index b857aec2a..b857aec2a 100644
--- a/test/regress/regress0/sep/loop-1220.smt2
+++ b/test/regress/regress1/sep/loop-1220.smt2
diff --git a/test/regress/regress0/sep/sep-simp-unc.smt2 b/test/regress/regress1/sep/sep-simp-unc.smt2
index cedbb53eb..cedbb53eb 100755
--- a/test/regress/regress0/sep/sep-simp-unc.smt2
+++ b/test/regress/regress1/sep/sep-simp-unc.smt2
diff --git a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2
index 10e509e05..10e509e05 100644
--- a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2
+++ b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2
diff --git a/test/regress/regress0/sep/split-find-unsat.smt2 b/test/regress/regress1/sep/split-find-unsat.smt2
index 1a9e76a8a..1a9e76a8a 100644
--- a/test/regress/regress0/sep/split-find-unsat.smt2
+++ b/test/regress/regress1/sep/split-find-unsat.smt2
diff --git a/test/regress/regress0/sets/card-vc6-minimized.smt2 b/test/regress/regress1/sets/card-vc6-minimized.smt2
index d7f4bdf1e..d7f4bdf1e 100644
--- a/test/regress/regress0/sets/card-vc6-minimized.smt2
+++ b/test/regress/regress1/sets/card-vc6-minimized.smt2
diff --git a/test/regress/regress0/sets/sets-disequal.smt2 b/test/regress/regress1/sets/sets-disequal.smt2
index 3acf77108..3acf77108 100644
--- a/test/regress/regress0/sets/sets-disequal.smt2
+++ b/test/regress/regress1/sets/sets-disequal.smt2
diff --git a/test/regress/regress0/strings/cmu-5042-0707-2.smt2 b/test/regress/regress1/strings/cmu-5042-0707-2.smt2
index 637142dfb..637142dfb 100644
--- a/test/regress/regress0/strings/cmu-5042-0707-2.smt2
+++ b/test/regress/regress1/strings/cmu-5042-0707-2.smt2
diff --git a/test/regress/regress0/strings/cmu-dis-0707-3.smt2 b/test/regress/regress1/strings/cmu-dis-0707-3.smt2
index 209cbb3f9..209cbb3f9 100644
--- a/test/regress/regress0/strings/cmu-dis-0707-3.smt2
+++ b/test/regress/regress1/strings/cmu-dis-0707-3.smt2
diff --git a/test/regress/regress0/sygus/hd-sdiv.sy b/test/regress/regress1/sygus/hd-sdiv.sy
index 019b48a1c..019b48a1c 100644
--- a/test/regress/regress0/sygus/hd-sdiv.sy
+++ b/test/regress/regress1/sygus/hd-sdiv.sy
diff --git a/test/regress/regress1/DTP_k2_n35_c175_s15.smt2 b/test/regress/regress2/DTP_k2_n35_c175_s15.smt2
index 20f4bf5a9..20f4bf5a9 100644
--- a/test/regress/regress1/DTP_k2_n35_c175_s15.smt2
+++ b/test/regress/regress2/DTP_k2_n35_c175_s15.smt2
diff --git a/test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 b/test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2
index 25f006d30..25f006d30 100644
--- a/test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2
+++ b/test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2
diff --git a/test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect b/test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect
index 7cb6ba8c2..7cb6ba8c2 100644
--- a/test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect
+++ b/test/regress/regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect
diff --git a/test/regress/regress1/GEO123+1.minimized.smt2 b/test/regress/regress2/GEO123+1.minimized.smt2
index 764c41699..764c41699 100644
--- a/test/regress/regress1/GEO123+1.minimized.smt2
+++ b/test/regress/regress2/GEO123+1.minimized.smt2
diff --git a/test/regress/regress2/Makefile b/test/regress/regress2/Makefile
index 5a9aa63be..b720980f1 100644
--- a/test/regress/regress2/Makefile
+++ b/test/regress/regress2/Makefile
@@ -1,5 +1,5 @@
 topdir = ../../..
-srcdir = test/regress/regress2
+srcdir = test/regress/regress1
 
 include $(topdir)/Makefile.subdir
 
diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am
index 9deb1f37b..c47d5840c 100644
--- a/test/regress/regress2/Makefile.am
+++ b/test/regress/regress2/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = .
+SUBDIRS = . arith
 
 # don't override a BINARY imported from a personal.mk
 @mk_if@eq ($(BINARY),)
@@ -20,21 +20,35 @@ MAKEFLAGS = -k
 # These are run for all build profiles.
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
-TESTS =	bmc-ibm-1.smt \
-	bmc-ibm-2.smt \
-	bmc-ibm-5.smt \
-	bmc-ibm-7.smt \
-	friedman_n6_i4.smt \
-	hole9.cvc \
-	qwh.35.405.shuffled-as.sat03-1651.smt \
-	eq_diamond14.smt \
-	incorrect1.smt \
-	incorrect2.smt \
-	bug497.cvc \
-	pp-regfile.smt
+TESTS =	bug136.smt \
+	bug148.smt \
+	bug394.smt2 \
+	DTP_k2_n35_c175_s15.smt2 \
+	GEO123+1.minimized.smt2 \
+	error1.smt \
+	friedman_n4_i5.smt \
+	hole7.cvc \
+	hole8.cvc \
+	instance_1444.smt \
+	fuzz_2.smt \
+	hash_sat_10_09.smt2 \
+	hash_sat_07_17.smt2 \
+	ooo.tag10.smt2 \
+	hash_sat_06_19.smt2 \
+	hash_sat_09_09.smt2 \
+	ooo.rf6.smt2 \
+	auflia-fuzz06.smt \
+	piVC_5581bd.smt2 \
+	typed_v1l50016-simp.cvc \
+	FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 \
+	xs-09-16-3-4-1-5.smt \
+	xs-09-16-3-4-1-5.decn.smt \
+	uflia-error0.smt2
 
 EXTRA_DIST = $(TESTS) \
-	pp-regfile.smt.expect
+	FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect \
+	uflia-error0.smt2.expect \
+	xs-09-16-3-4-1-5.decn.smt.expect
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
@@ -51,5 +65,5 @@ EXTRA_DIST = $(TESTS) \
 regress regress2 test: check
 
 # do nothing in this subdir
-.PHONY: regress0 regress1 regress3
-regress0 regress1 regress3:
+.PHONY: regress0 regress1 regress3 regress4
+regress0 regress1 regress3 regress4:
diff --git a/test/regress/regress1/arith/Makefile b/test/regress/regress2/arith/Makefile
index 481d240e4..481d240e4 100644
--- a/test/regress/regress1/arith/Makefile
+++ b/test/regress/regress2/arith/Makefile
diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress2/arith/Makefile.am
index fff5372c6..fff5372c6 100644
--- a/test/regress/regress1/arith/Makefile.am
+++ b/test/regress/regress2/arith/Makefile.am
diff --git a/test/regress/regress1/arith/abz5_1400.smt b/test/regress/regress2/arith/abz5_1400.smt
index 662b39859..662b39859 100644
--- a/test/regress/regress1/arith/abz5_1400.smt
+++ b/test/regress/regress2/arith/abz5_1400.smt
diff --git a/test/regress/regress1/arith/lpsat-goal-9.smt2 b/test/regress/regress2/arith/lpsat-goal-9.smt2
index d71fc1340..d71fc1340 100644
--- a/test/regress/regress1/arith/lpsat-goal-9.smt2
+++ b/test/regress/regress2/arith/lpsat-goal-9.smt2
diff --git a/test/regress/regress1/arith/prp-13-24.smt2 b/test/regress/regress2/arith/prp-13-24.smt2
index b3b8e69b1..b3b8e69b1 100644
--- a/test/regress/regress1/arith/prp-13-24.smt2
+++ b/test/regress/regress2/arith/prp-13-24.smt2
diff --git a/test/regress/regress1/arith/pursuit-safety-11.smt b/test/regress/regress2/arith/pursuit-safety-11.smt
index 1c12e0770..1c12e0770 100644
--- a/test/regress/regress1/arith/pursuit-safety-11.smt
+++ b/test/regress/regress2/arith/pursuit-safety-11.smt
diff --git a/test/regress/regress1/arith/pursuit-safety-12.smt b/test/regress/regress2/arith/pursuit-safety-12.smt
index 8f79b3d92..8f79b3d92 100644
--- a/test/regress/regress1/arith/pursuit-safety-12.smt
+++ b/test/regress/regress2/arith/pursuit-safety-12.smt
diff --git a/test/regress/regress1/arith/qlock-4-10-9.base.cvc.smt2 b/test/regress/regress2/arith/qlock-4-10-9.base.cvc.smt2
index d71fc1340..d71fc1340 100644
--- a/test/regress/regress1/arith/qlock-4-10-9.base.cvc.smt2
+++ b/test/regress/regress2/arith/qlock-4-10-9.base.cvc.smt2
diff --git a/test/regress/regress1/arith/sc-7.base.cvc.smt b/test/regress/regress2/arith/sc-7.base.cvc.smt
index 72a561593..72a561593 100644
--- a/test/regress/regress1/arith/sc-7.base.cvc.smt
+++ b/test/regress/regress2/arith/sc-7.base.cvc.smt
diff --git a/test/regress/regress1/arith/uart-8.base.cvc.smt b/test/regress/regress2/arith/uart-8.base.cvc.smt
index a64a0cdbe..a64a0cdbe 100644
--- a/test/regress/regress1/arith/uart-8.base.cvc.smt
+++ b/test/regress/regress2/arith/uart-8.base.cvc.smt
diff --git a/test/regress/regress1/auflia-fuzz06.smt b/test/regress/regress2/auflia-fuzz06.smt
index 88c2a9d5c..88c2a9d5c 100644
--- a/test/regress/regress1/auflia-fuzz06.smt
+++ b/test/regress/regress2/auflia-fuzz06.smt
diff --git a/test/regress/regress1/bug136.smt b/test/regress/regress2/bug136.smt
index 08fb3cb6c..08fb3cb6c 100644
--- a/test/regress/regress1/bug136.smt
+++ b/test/regress/regress2/bug136.smt
diff --git a/test/regress/regress1/bug148.smt b/test/regress/regress2/bug148.smt
index a07dc1bf0..a07dc1bf0 100644
--- a/test/regress/regress1/bug148.smt
+++ b/test/regress/regress2/bug148.smt
diff --git a/test/regress/regress1/bug394.smt2 b/test/regress/regress2/bug394.smt2
index 99e19e7fb..99e19e7fb 100644
--- a/test/regress/regress1/bug394.smt2
+++ b/test/regress/regress2/bug394.smt2
diff --git a/test/regress/regress1/error0.smt2 b/test/regress/regress2/error0.smt2
index 73177a252..73177a252 100644
--- a/test/regress/regress1/error0.smt2
+++ b/test/regress/regress2/error0.smt2
diff --git a/test/regress/regress1/error1.smt b/test/regress/regress2/error1.smt
index 9b2cabedf..9b2cabedf 100644
--- a/test/regress/regress1/error1.smt
+++ b/test/regress/regress2/error1.smt
diff --git a/test/regress/regress1/friedman_n4_i5.smt b/test/regress/regress2/friedman_n4_i5.smt
index ff5c75735..ff5c75735 100644
--- a/test/regress/regress1/friedman_n4_i5.smt
+++ b/test/regress/regress2/friedman_n4_i5.smt
diff --git a/test/regress/regress1/fuzz_2.smt b/test/regress/regress2/fuzz_2.smt
index 1dc2f619d..1dc2f619d 100644
--- a/test/regress/regress1/fuzz_2.smt
+++ b/test/regress/regress2/fuzz_2.smt
diff --git a/test/regress/regress1/hash_sat_06_19.smt2 b/test/regress/regress2/hash_sat_06_19.smt2
index b565a4b57..b565a4b57 100644
--- a/test/regress/regress1/hash_sat_06_19.smt2
+++ b/test/regress/regress2/hash_sat_06_19.smt2
diff --git a/test/regress/regress1/hash_sat_07_17.smt2 b/test/regress/regress2/hash_sat_07_17.smt2
index 0bb49801a..0bb49801a 100644
--- a/test/regress/regress1/hash_sat_07_17.smt2
+++ b/test/regress/regress2/hash_sat_07_17.smt2
diff --git a/test/regress/regress1/hash_sat_09_09.smt2 b/test/regress/regress2/hash_sat_09_09.smt2
index 6dc26542e..6dc26542e 100644
--- a/test/regress/regress1/hash_sat_09_09.smt2
+++ b/test/regress/regress2/hash_sat_09_09.smt2
diff --git a/test/regress/regress1/hash_sat_10_09.smt2 b/test/regress/regress2/hash_sat_10_09.smt2
index 20cff8b1b..20cff8b1b 100644
--- a/test/regress/regress1/hash_sat_10_09.smt2
+++ b/test/regress/regress2/hash_sat_10_09.smt2
diff --git a/test/regress/regress1/hole7.cvc b/test/regress/regress2/hole7.cvc
index 1f762477a..1f762477a 100644
--- a/test/regress/regress1/hole7.cvc
+++ b/test/regress/regress2/hole7.cvc
diff --git a/test/regress/regress1/hole8.cvc b/test/regress/regress2/hole8.cvc
index 705c95ea6..705c95ea6 100644
--- a/test/regress/regress1/hole8.cvc
+++ b/test/regress/regress2/hole8.cvc
diff --git a/test/regress/regress1/instance_1444.smt b/test/regress/regress2/instance_1444.smt
index 1bed83467..1bed83467 100644
--- a/test/regress/regress1/instance_1444.smt
+++ b/test/regress/regress2/instance_1444.smt
diff --git a/test/regress/regress1/ooo.rf6.smt2 b/test/regress/regress2/ooo.rf6.smt2
index 4860a3428..4860a3428 100644
--- a/test/regress/regress1/ooo.rf6.smt2
+++ b/test/regress/regress2/ooo.rf6.smt2
diff --git a/test/regress/regress1/ooo.tag10.smt2 b/test/regress/regress2/ooo.tag10.smt2
index ef8e2244c..ef8e2244c 100644
--- a/test/regress/regress1/ooo.tag10.smt2
+++ b/test/regress/regress2/ooo.tag10.smt2
diff --git a/test/regress/regress1/piVC_5581bd.smt2 b/test/regress/regress2/piVC_5581bd.smt2
index 78baeea84..78baeea84 100644
--- a/test/regress/regress1/piVC_5581bd.smt2
+++ b/test/regress/regress2/piVC_5581bd.smt2
diff --git a/test/regress/regress1/typed_v1l50016-simp.cvc b/test/regress/regress2/typed_v1l50016-simp.cvc
index b4a1e4b32..b4a1e4b32 100644
--- a/test/regress/regress1/typed_v1l50016-simp.cvc
+++ b/test/regress/regress2/typed_v1l50016-simp.cvc
diff --git a/test/regress/regress1/uflia-error0.smt2 b/test/regress/regress2/uflia-error0.smt2
index 73177a252..73177a252 100644
--- a/test/regress/regress1/uflia-error0.smt2
+++ b/test/regress/regress2/uflia-error0.smt2
diff --git a/test/regress/regress1/uflia-error0.smt2.expect b/test/regress/regress2/uflia-error0.smt2.expect
index 7fd1d5a98..7fd1d5a98 100644
--- a/test/regress/regress1/uflia-error0.smt2.expect
+++ b/test/regress/regress2/uflia-error0.smt2.expect
diff --git a/test/regress/regress1/xs-09-16-3-4-1-5.decn.smt b/test/regress/regress2/xs-09-16-3-4-1-5.decn.smt
index 549306c5b..549306c5b 100644
--- a/test/regress/regress1/xs-09-16-3-4-1-5.decn.smt
+++ b/test/regress/regress2/xs-09-16-3-4-1-5.decn.smt
diff --git a/test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect b/test/regress/regress2/xs-09-16-3-4-1-5.decn.smt.expect
index 7fd1d5a98..7fd1d5a98 100644
--- a/test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect
+++ b/test/regress/regress2/xs-09-16-3-4-1-5.decn.smt.expect
diff --git a/test/regress/regress1/xs-09-16-3-4-1-5.smt b/test/regress/regress2/xs-09-16-3-4-1-5.smt
index 549306c5b..549306c5b 100644
--- a/test/regress/regress1/xs-09-16-3-4-1-5.smt
+++ b/test/regress/regress2/xs-09-16-3-4-1-5.smt
diff --git a/test/regress/regress1/xs-11-20-5-2-5-3.smt b/test/regress/regress2/xs-11-20-5-2-5-3.smt
index 00ca325e1..00ca325e1 100644
--- a/test/regress/regress1/xs-11-20-5-2-5-3.smt
+++ b/test/regress/regress2/xs-11-20-5-2-5-3.smt
diff --git a/test/regress/regress1/xs-11-20-5-2-5-3.smt2 b/test/regress/regress2/xs-11-20-5-2-5-3.smt2
index bdf0d25ab..bdf0d25ab 100644
--- a/test/regress/regress1/xs-11-20-5-2-5-3.smt2
+++ b/test/regress/regress2/xs-11-20-5-2-5-3.smt2
diff --git a/test/regress/regress3/Makefile b/test/regress/regress3/Makefile
index 223547305..5a9aa63be 100644
--- a/test/regress/regress3/Makefile
+++ b/test/regress/regress3/Makefile
@@ -1,5 +1,5 @@
 topdir = ../../..
-srcdir = test/regress/regress3
+srcdir = test/regress/regress2
 
 include $(topdir)/Makefile.subdir
 
diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am
index 3fb798bcc..f45c5bd64 100644
--- a/test/regress/regress3/Makefile.am
+++ b/test/regress/regress3/Makefile.am
@@ -20,14 +20,21 @@ MAKEFLAGS = -k
 # These are run for all build profiles.
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
-TESTS =	bug143.smt \
-	C880mul.miter.shuffled-as.sat03-348.smt \
-	comb2.shuffled-as.sat03-420.smt \
-	hole10.cvc \
-	instance_1151.smt \
-	NEQ016_size5.smt
-
-EXTRA_DIST = $(TESTS)
+TESTS =	bmc-ibm-1.smt \
+	bmc-ibm-2.smt \
+	bmc-ibm-5.smt \
+	bmc-ibm-7.smt \
+	friedman_n6_i4.smt \
+	hole9.cvc \
+	qwh.35.405.shuffled-as.sat03-1651.smt \
+	eq_diamond14.smt \
+	incorrect1.smt \
+	incorrect2.smt \
+	bug497.cvc \
+	pp-regfile.smt
+
+EXTRA_DIST = $(TESTS) \
+	pp-regfile.smt.expect
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
@@ -44,5 +51,5 @@ EXTRA_DIST = $(TESTS)
 regress regress3 test: check
 
 # do nothing in this subdir
-.PHONY: regress0 regress1 regress2
-regress0 regress1 regress2:
+.PHONY: regress0 regress1 regress2 regress4
+regress0 regress1 regress2 regress4:
diff --git a/test/regress/regress2/bmc-ibm-1.smt b/test/regress/regress3/bmc-ibm-1.smt
index 9c210e3a1..9c210e3a1 100644
--- a/test/regress/regress2/bmc-ibm-1.smt
+++ b/test/regress/regress3/bmc-ibm-1.smt
diff --git a/test/regress/regress2/bmc-ibm-2.smt b/test/regress/regress3/bmc-ibm-2.smt
index 5f90bc620..5f90bc620 100644
--- a/test/regress/regress2/bmc-ibm-2.smt
+++ b/test/regress/regress3/bmc-ibm-2.smt
diff --git a/test/regress/regress2/bmc-ibm-5.smt b/test/regress/regress3/bmc-ibm-5.smt
index ba9020762..ba9020762 100644
--- a/test/regress/regress2/bmc-ibm-5.smt
+++ b/test/regress/regress3/bmc-ibm-5.smt
diff --git a/test/regress/regress2/bmc-ibm-7.smt b/test/regress/regress3/bmc-ibm-7.smt
index 3e8fd9321..3e8fd9321 100644
--- a/test/regress/regress2/bmc-ibm-7.smt
+++ b/test/regress/regress3/bmc-ibm-7.smt
diff --git a/test/regress/regress2/bug497.cvc b/test/regress/regress3/bug497.cvc
index 8af568459..8af568459 100644
--- a/test/regress/regress2/bug497.cvc
+++ b/test/regress/regress3/bug497.cvc
diff --git a/test/regress/regress2/eq_diamond14.smt b/test/regress/regress3/eq_diamond14.smt
index f89d0e3b7..f89d0e3b7 100644
--- a/test/regress/regress2/eq_diamond14.smt
+++ b/test/regress/regress3/eq_diamond14.smt
diff --git a/test/regress/regress2/friedman_n6_i4.smt b/test/regress/regress3/friedman_n6_i4.smt
index 113877982..113877982 100644
--- a/test/regress/regress2/friedman_n6_i4.smt
+++ b/test/regress/regress3/friedman_n6_i4.smt
diff --git a/test/regress/regress2/hole9.cvc b/test/regress/regress3/hole9.cvc
index e60839f7b..e60839f7b 100644
--- a/test/regress/regress2/hole9.cvc
+++ b/test/regress/regress3/hole9.cvc
diff --git a/test/regress/regress2/incorrect1.smt b/test/regress/regress3/incorrect1.smt
index 23425d462..23425d462 100644
--- a/test/regress/regress2/incorrect1.smt
+++ b/test/regress/regress3/incorrect1.smt
diff --git a/test/regress/regress2/incorrect2.smt b/test/regress/regress3/incorrect2.smt
index 23425d462..23425d462 100644
--- a/test/regress/regress2/incorrect2.smt
+++ b/test/regress/regress3/incorrect2.smt
diff --git a/test/regress/regress2/pp-regfile.smt b/test/regress/regress3/pp-regfile.smt
index e60be055a..e60be055a 100644
--- a/test/regress/regress2/pp-regfile.smt
+++ b/test/regress/regress3/pp-regfile.smt
diff --git a/test/regress/regress2/pp-regfile.smt.expect b/test/regress/regress3/pp-regfile.smt.expect
index 7fd1d5a98..7fd1d5a98 100644
--- a/test/regress/regress2/pp-regfile.smt.expect
+++ b/test/regress/regress3/pp-regfile.smt.expect
diff --git a/test/regress/regress2/qwh.35.405.shuffled-as.sat03-1651.smt b/test/regress/regress3/qwh.35.405.shuffled-as.sat03-1651.smt
index 7c09b58aa..7c09b58aa 100644
--- a/test/regress/regress2/qwh.35.405.shuffled-as.sat03-1651.smt
+++ b/test/regress/regress3/qwh.35.405.shuffled-as.sat03-1651.smt
diff --git a/test/regress/regress3/C880mul.miter.shuffled-as.sat03-348.smt b/test/regress/regress4/C880mul.miter.shuffled-as.sat03-348.smt
index 0cce52b17..0cce52b17 100644
--- a/test/regress/regress3/C880mul.miter.shuffled-as.sat03-348.smt
+++ b/test/regress/regress4/C880mul.miter.shuffled-as.sat03-348.smt
diff --git a/test/regress/regress1/Makefile b/test/regress/regress4/Makefile
index b720980f1..223547305 100644
--- a/test/regress/regress1/Makefile
+++ b/test/regress/regress4/Makefile
@@ -1,5 +1,5 @@
 topdir = ../../..
-srcdir = test/regress/regress1
+srcdir = test/regress/regress3
 
 include $(topdir)/Makefile.subdir
 
diff --git a/test/regress/regress4/Makefile.am b/test/regress/regress4/Makefile.am
new file mode 100644
index 000000000..5a31fb24e
--- /dev/null
+++ b/test/regress/regress4/Makefile.am
@@ -0,0 +1,48 @@
+SUBDIRS = .
+
+# don't override a BINARY imported from a personal.mk
+@mk_if@eq ($(BINARY),)
+@mk_empty@BINARY = cvc4
+end@mk_if@
+
+LOG_COMPILER = @srcdir@/../run_regression
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT)
+
+if AUTOMAKE_1_11
+# old-style (pre-automake 1.12) test harness
+TESTS_ENVIRONMENT = \
+	$(LOG_COMPILER) \
+	$(AM_LOG_FLAGS) $(LOG_FLAGS)
+endif
+
+MAKEFLAGS = -k
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	bug143.smt \
+	C880mul.miter.shuffled-as.sat03-348.smt \
+	comb2.shuffled-as.sat03-420.smt \
+	hole10.cvc \
+	instance_1151.smt \
+	NEQ016_size5.smt
+
+EXTRA_DIST = $(TESTS)
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+#	error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+#	error.cvc
+
+# synonyms for "check" in this directory
+.PHONY: regress regress4 test
+regress regress4 test: check
+
+# do nothing in this subdir
+.PHONY: regress0 regress1 regress2 regress3
+regress0 regress1 regress2 regress3:
diff --git a/test/regress/regress3/NEQ016_size5.smt b/test/regress/regress4/NEQ016_size5.smt
index ec56385f6..ec56385f6 100644
--- a/test/regress/regress3/NEQ016_size5.smt
+++ b/test/regress/regress4/NEQ016_size5.smt
diff --git a/test/regress/regress3/bug143.smt b/test/regress/regress4/bug143.smt
index 21c588ad3..21c588ad3 100644
--- a/test/regress/regress3/bug143.smt
+++ b/test/regress/regress4/bug143.smt
diff --git a/test/regress/regress3/comb2.shuffled-as.sat03-420.smt b/test/regress/regress4/comb2.shuffled-as.sat03-420.smt
index b1d9309a3..b1d9309a3 100644
--- a/test/regress/regress3/comb2.shuffled-as.sat03-420.smt
+++ b/test/regress/regress4/comb2.shuffled-as.sat03-420.smt
diff --git a/test/regress/regress3/hole10.cvc b/test/regress/regress4/hole10.cvc
index ebc8279d3..ebc8279d3 100644
--- a/test/regress/regress3/hole10.cvc
+++ b/test/regress/regress4/hole10.cvc
diff --git a/test/regress/regress3/instance_1151.smt b/test/regress/regress4/instance_1151.smt
index 0d5bd0beb..0d5bd0beb 100644
--- a/test/regress/regress3/instance_1151.smt
+++ b/test/regress/regress4/instance_1151.smt