Move regression tests to single Makefile.am (#1658)

Until now, regression tests were split across tens of different
Makefile.am, which required a lot of code duplication and does not
really seem to be in the spirit of automake. If we want to change the
LOG_COMPILER/LOG_DRIVER for example, we have to change every single
Makefile.am, which is cumbersome (I was able to get something
semi-working by exporting those variables but it didn't seem very
clean). Additionally, it made the output of the regression tests fairly
verbose and split the output across multiple log files. Finally
it also limited parallelism when running the regression tests (this fix lowers
the time it takes to run regression level 1 from 3m to 1m45s on my
machine with 16 threads).

This commit moves all the regression tests into
test/regress/Makefile.tests and changes test/regress/Makefile.am to deal
with this new structure. Finally, it changes how the test summary in
test/Makefile.am is produced: instead of relying on the log files for
the subdirectories, it greps for the test results in the log files of
the individual tests. Not the most elegant solution but we should
probably anyway delegate that task to a Python script at some point.

34 files changed, 0 insertions, 1357 deletions

diff --git a/test/regress/regress1/Makefile b/test/regress/regress1/Makefile
deleted file mode 100644
index b720980f1..000000000
--- a/test/regress/regress1/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../../..
-srcdir = test/regress/regress1
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
deleted file mode 100644
index af3f65370..000000000
--- a/test/regress/regress1/Makefile.am
+++ /dev/null
@@ -1,78 +0,0 @@
-SUBDIRS = . arith bv aufbv auflia datatypes rewriterules lemmas decision fmf ho nl push-pop quantifiers rels strings sets sygus sep uflia
-
-# 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 =	\
-	bug425.cvc \
-	bug519.smt2 \
-	bug521.smt2 \
-	bug694-Unapply1.scala-0.smt2 \
-	fmf-fun-dbu.smt2 \
-	bug296.smt2 \
-	bug507.smt2 \
-	gensys_brn001.smt2 \
-	simplification_bug4.smt2 \
-	trim.cvc \
-	constarr3.cvc \
-	constarr3.smt2 \
-	parsing_ringer.cvc \
-	arrayinuf_error.smt2 \
-	boolean-terms-kernel2.smt2 \
-	boolean.cvc \
-	bug216.smt2 \
-	bug512.smt2 \
-	bug516.smt2 \
-	bug520.smt2 \
-	bug543.smt2 \
-	bug567.smt2 \
-	bug593.smt2 \
-	bug681.smt2 \
-	bug800.smt2 \
-	bvdiv2.smt2 \
-	error.cvc \
-	errorcrash.smt2 \
-	hole6.cvc \
-	ite5.smt2 \
-	non-fatal-errors.smt2 \
-	proof00.smt2 \
-	sqrt2-sort-inf-unk.smt2 \
-	test12.cvc \
-	uf2.smt2
-	
-EXTRA_DIST = $(TESTS) \
-	simplification_bug4.smt2.expect \
-	bug590.smt2.expect \
-	bug216.smt2.expect \
-	bug590.smt2 \
-	bug585.cvc \
-	crash_burn_locusts.smt2 \
-	bug472.smt2 \
-	simple-rdl-definefun.smt2
-	
-# issue1048-arrays-int-real.smt2 -- different errors on debug and production
-
-# synonyms for "check" in this directory
-.PHONY: regress regress1 test
-regress regress1 test: check
-
-# do nothing in this subdir
-.PHONY: regress0 regress2 regress3 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress1/arith/Makefile.am
deleted file mode 100644
index e2b0e93d9..000000000
--- a/test/regress/regress1/arith/Makefile.am
+++ /dev/null
@@ -1,139 +0,0 @@
-# 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
-
-# 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 =	\
-	arith-int-004.cvc \
-	arith-int-011.cvc \
-	arith-int-048.cvc \
-	arith-int-050.cvc \
-	arith-int-084.cvc \
-	arith-int-085.cvc \
-	arith-int-097.cvc \
-	bug716.0.smt2 \
-	problem__003.smt2 \
-	bug547.1.smt2 \
-	bug716.1.cvc \
-	div.03.smt2 \
-	div.06.smt2 \
-	div.08.smt2 \
-	div.09.smt2 \
-	miplib3.cvc \
-	mod.02.smt2 \
-	mod.03.smt2 \
-	mult.02.smt2 \
-	arith-int-012.cvc \
-	arith-int-013.cvc \
-	arith-int-022.cvc \
-	arith-int-024.cvc \
-	arith-int-047.cvc
-
-EXTRA_DIST = $(TESTS) \
-	arith-int-008.cvc \
-	arith-int-018.cvc \
-	arith-int-020.cvc \
-	arith-int-026.cvc \
-	arith-int-029.cvc \
-	arith-int-030.cvc \
-	arith-int-043.cvc \
-	arith-int-044.cvc \
-	arith-int-049.cvc \
-	arith-int-061.cvc \
-	arith-int-062.cvc \
-	arith-int-064.cvc \
-	arith-int-065.cvc \
-	arith-int-081.cvc \
-	arith-int-083.cvc \
-	arith-int-090.cvc \
-	arith-int-091.cvc \
-	arith-int-092.cvc \
-	arith-int-094.cvc \
-	arith-int-096.cvc \
-	arith-int-098.cvc \
-	arith-int-001.cvc \
-	arith-int-002.cvc \
-	arith-int-003.cvc \
-	arith-int-005.cvc \
-	arith-int-006.cvc \
-	arith-int-009.cvc \
-	arith-int-010.cvc \
-	arith-int-016.cvc \
-	arith-int-017.cvc \
-	arith-int-019.cvc \
-	arith-int-027.cvc \
-	arith-int-028.cvc \
-	arith-int-031.cvc \
-	arith-int-032.cvc \
-	arith-int-033.cvc \
-	arith-int-034.cvc \
-	arith-int-035.cvc \
-	arith-int-036.cvc \
-	arith-int-037.cvc \
-	arith-int-038.cvc \
-	arith-int-039.cvc \
-	arith-int-040.cvc \
-	arith-int-041.cvc \
-	arith-int-045.cvc \
-	arith-int-046.cvc \
-	arith-int-051.cvc \
-	arith-int-052.cvc \
-	arith-int-053.cvc \
-	arith-int-054.cvc \
-	arith-int-055.cvc \
-	arith-int-056.cvc \
-	arith-int-057.cvc \
-	arith-int-058.cvc \
-	arith-int-059.cvc \
-	arith-int-060.cvc \
-	arith-int-063.cvc \
-	arith-int-066.cvc \
-	arith-int-067.cvc \
-	arith-int-068.cvc \
-	arith-int-069.cvc \
-	arith-int-070.cvc \
-	arith-int-071.cvc \
-	arith-int-072.cvc \
-	arith-int-073.cvc \
-	arith-int-074.cvc \
-	arith-int-075.cvc \
-	arith-int-076.cvc \
-	arith-int-077.cvc \
-	arith-int-078.cvc \
-	arith-int-080.cvc \
-	arith-int-086.cvc \
-	arith-int-087.cvc \
-	arith-int-088.cvc \
-	arith-int-089.cvc \
-	arith-int-093.cvc \
-	arith-int-095.cvc \
-	arith-int-099.cvc \
-	arith-int-100.cvc
-	
-FAILING_TESTS = \
-	arith-int-007.cvc \
-	arith-int-082.cvc \
-	arith-int-098.cvc
-
-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 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/aufbv/Makefile b/test/regress/regress1/aufbv/Makefile
deleted file mode 100644
index 197a840e1..000000000
--- a/test/regress/regress1/aufbv/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../../../..
-srcdir = test/regress/regress1/aufbv
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/regress/regress1/aufbv/Makefile.am b/test/regress/regress1/aufbv/Makefile.am
deleted file mode 100644
index 019e7f23a..000000000
--- a/test/regress/regress1/aufbv/Makefile.am
+++ /dev/null
@@ -1,31 +0,0 @@
-# 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
-
-# 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 =	\
-	fuzz10.smt \
-	bug580.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 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/auflia/Makefile b/test/regress/regress1/auflia/Makefile
deleted file mode 100644
index 46e7ebe17..000000000
--- a/test/regress/regress1/auflia/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../../../..
-srcdir = test/regress/regress1/auflia
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/regress/regress1/auflia/Makefile.am b/test/regress/regress1/auflia/Makefile.am
deleted file mode 100644
index 25a0d89e0..000000000
--- a/test/regress/regress1/auflia/Makefile.am
+++ /dev/null
@@ -1,31 +0,0 @@
-# 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
-
-# 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 =	\
-	bug330.smt2
-
-EXTRA_DIST = $(TESTS)  \
-	bug337.smt2
-
-# synonyms for "check" in this directory
-.PHONY: regress regress1 test
-regress regress1 test: check
-
-# do nothing in this subdir
-.PHONY: regress0 regress2 regress3 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/bv/Makefile b/test/regress/regress1/bv/Makefile
deleted file mode 100644
index 1ddea736f..000000000
--- a/test/regress/regress1/bv/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../../../..
-srcdir = test/regress/regress1/bv
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/regress/regress1/bv/Makefile.am b/test/regress/regress1/bv/Makefile.am
deleted file mode 100644
index b144a0507..000000000
--- a/test/regress/regress1/bv/Makefile.am
+++ /dev/null
@@ -1,44 +0,0 @@
-# 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
-
-# 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 =	\
-	bv-proof00.smt \
-	fuzz34.smt \
-	fuzz38.smt \
-	bug_extract_mult_leading_bit.smt2 \
-	bug787.smt2 \
-	bv-int-collapse2-sat.smt2 \
-	cmu-rdk-3.smt2 \
-	decision-weight00.smt2 \
-	divtest.smt2 \
-	bv2nat-ground.smt2 \
-	bv2nat-simp-range-sat.smt2 \
-	unsound1.smt2
-
-EXTRA_DIST = $(TESTS)
-
-# This benchmark is currently disabled as it uses --check-proof
-# bench_38.delta.smt2
-
-# synonyms for "check" in this directory
-.PHONY: regress regress1 test
-regress regress1 test: check
-
-# do nothing in this subdir
-.PHONY: regress0 regress2 regress3 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/datatypes/Makefile b/test/regress/regress1/datatypes/Makefile
deleted file mode 100644
index 1e40da253..000000000
--- a/test/regress/regress1/datatypes/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../../../..
-srcdir = test/regress/regress1/datatypes
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/regress/regress1/datatypes/Makefile.am b/test/regress/regress1/datatypes/Makefile.am
deleted file mode 100644
index 036b8df00..000000000
--- a/test/regress/regress1/datatypes/Makefile.am
+++ /dev/null
@@ -1,34 +0,0 @@
-# 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
-
-# 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 =	\
-	manos-model.smt2 \
-	acyclicity-sr-ground096.smt2 \
-	dt-color-2.6.smt2 \
-	dt-param-card4-unsat.smt2 \
-	error.cvc
-
-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 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/decision/Makefile b/test/regress/regress1/decision/Makefile
deleted file mode 100644
index 92798c450..000000000
--- a/test/regress/regress1/decision/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../../../..
-srcdir = test/regress/regress1/decision
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/regress/regress1/decision/Makefile.am b/test/regress/regress1/decision/Makefile.am
deleted file mode 100644
index 102c99e01..000000000
--- a/test/regress/regress1/decision/Makefile.am
+++ /dev/null
@@ -1,34 +0,0 @@
-# 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
-
-# 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 =	\
-	error3.smt \
-	quant-symmetric_unsat_7.smt2 \
-	quant-Arrays_Q1-noinfer.smt2
-
-EXTRA_DIST = $(TESTS) \
-	quant-symmetric_unsat_7.smt2.expect \
-	quant-Arrays_Q1-noinfer.smt2.expect
-
-# synonyms for "check" in this directory
-.PHONY: regress regress1 test
-regress regress1 test: check
-
-# do nothing in this subdir
-.PHONY: regress0 regress2 regress3 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/fmf/Makefile b/test/regress/regress1/fmf/Makefile
deleted file mode 100644
index 400ad9d0d..000000000
--- a/test/regress/regress1/fmf/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../../../..
-srcdir = test/regress/regress1/fmf
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/regress/regress1/fmf/Makefile.am b/test/regress/regress1/fmf/Makefile.am
deleted file mode 100644
index dc07f6ca4..000000000
--- a/test/regress/regress1/fmf/Makefile.am
+++ /dev/null
@@ -1,68 +0,0 @@
-# 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
-
-# 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 =	\
-	agree466.smt2 \
-	ALG008-1.smt2 \
-	bug0909.smt2 \
-	bug764.smt2 \
-	datatypes-ufinite.smt2 \
-	datatypes-ufinite-nested.smt2 \
-	fc-pigeonhole19.smt2 \
-	fib-core.smt2 \
-	fmf-bound-2dim.smt2 \
-	fmf-fun-no-elim-ext-arith2.smt2 \
-	fmf-strange-bounds.smt2 \
-	issue916-fmf-or.smt2 \
-	jasmin-cdt-crash.smt2 \
-	LeftistHeap.scala-8-ncm.smt2 \
-	lst-no-self-rev-exp.smt2 \
-	nun-0208-to.smt2 \
-	pow2-bool.smt2 \
-	with-ind-104-core.smt2 \
-	agree467.smt2 \
-	alg202+1.smt2 \
-	am-bad-model.cvc \
-	bound-int-alt.smt2 \
-	bug651.smt2 \
-	bug723-irrelevant-funs.smt2 \
-	cons-sets-bounds.smt2 \
-	constr-ground-to.smt2 \
-	dt-proper-model.smt2 \
-	fmf-bound-int.smt2 \
-	fmf-fun-no-elim-ext-arith.smt2 \
-	forall_unit_data.smt2 \
-	fore19-exp2-core.smt2 \
-	german169.smt2 \
-	german73.smt2 \
-	ko-bound-set.cvc \
-	loopy_coda.smt2 \
-	memory_model-R_cpp-dd.cvc \
-	PUZ001+1.smt2 \
-	refcount24.cvc.smt2 \
-	sc-crash-052316.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 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/ho/Makefile.am b/test/regress/regress1/ho/Makefile.am
deleted file mode 100644
index 6ae3a116f..000000000
--- a/test/regress/regress1/ho/Makefile.am
+++ /dev/null
@@ -1,35 +0,0 @@
-# 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
-
-# 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 =	\
-	auth0068.smt2 \
-	fta0409.smt2 \
-	ho-exponential-model.smt2 \
-	ho-matching-enum-2.smt2 \
-	ho-std-fmf.smt2
-	
-EXTRA_DIST = $(TESTS) \
-	hoa0102.smt2
-
-# synonyms for "check" in this directory
-.PHONY: regress regress1 test
-regress regress1 test: check
-
-# do nothing in this subdir
-.PHONY: regress0 regress2 regress3 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/lemmas/Makefile b/test/regress/regress1/lemmas/Makefile
deleted file mode 100644
index 46d254aef..000000000
--- a/test/regress/regress1/lemmas/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../../../..
-srcdir = test/regress/regress1/lemmas
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/regress/regress1/lemmas/Makefile.am b/test/regress/regress1/lemmas/Makefile.am
deleted file mode 100644
index d22553d64..000000000
--- a/test/regress/regress1/lemmas/Makefile.am
+++ /dev/null
@@ -1,32 +0,0 @@
-# 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
-
-# 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 =	\
-	clocksynchro_5clocks.main_invar.base.smt \
-	pursuit-safety-8.smt \
-	simple_startup_9nodes.abstract.base.smt
-
-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 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/nl/Makefile.am b/test/regress/regress1/nl/Makefile.am
deleted file mode 100644
index a008e4df1..000000000
--- a/test/regress/regress1/nl/Makefile.am
+++ /dev/null
@@ -1,78 +0,0 @@
-# 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
-
-# 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 =	\
-	mirko-050417.smt2 \
-	arrowsmith-050317.smt2 \
-	bug698.smt2 \
-	dist-big.smt2 \
-	dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 \
-	exp-4.5-lt.smt2 \
-	metitarski_3_4_2e.smt2 \
-	metitarski-3-4.smt2 \
-	nl-help-unsat-quant.smt2 \
-	poly-1025.smt2 \
-	quant-nl.smt2 \
-	red-exp.smt2 \
-	rewriting-sums.smt2 \
-	simple-mono.smt2 \
-	sin1-sat.smt2 \
-	sin-compare.smt2 \
-	sin-compare-across-phase.smt2 \
-	sqrt-problem-1.smt2 \
-	sugar-ident-2.smt2 \
-	sugar-ident-3.smt2 \
-	tan-rewrite2.smt2 \
-	bad-050217.smt2 \
-	coeff-unsat-base.smt2 \
-	coeff-unsat.smt2 \
-	combine.smt2 \
-	cos-bound.smt2 \
-	cos1-tc.smt2 \
-	disj-eval.smt2 \
-	div-mod-partial.smt2 \
-	exp_monotone.smt2 \
-	exp1-lb.smt2 \
-	metitarski-1025.smt2 \
-	NAVIGATION2.smt2 \
-	nl-unk-quant.smt2 \
-	ones.smt2 \
-	shifting.smt2 \
-	shifting2.smt2 \
-	simple-mono-unsat.smt2 \
-	sin-init-tangents.smt2 \
-	sin-sign.smt2 \
-	sin-sym2.smt2 \
-	sin1-lb.smt2 \
-	sin1-ub.smt2 \
-	sin2-lb.smt2 \
-	sin2-ub.smt2 \
-	sugar-ident.smt2 \
-	zero-subset.smt2 \
-	sin1-deq-sat.smt2 \
-	nl-eq-infer.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 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/push-pop/Makefile.am b/test/regress/regress1/push-pop/Makefile.am
deleted file mode 100644
index d1fe52984..000000000
--- a/test/regress/regress1/push-pop/Makefile.am
+++ /dev/null
@@ -1,92 +0,0 @@
-# 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
-
-# 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 =	\
-	arith_lra_01.smt2 \
-	arith_lra_02.smt2 \
-	bug-fmf-fun-skolem.smt2 \
-	bug216.smt2 \
-	bug326.smt2 \
-	fuzz_1_to_52_merged.smt2 \
-	fuzz_1.smt2 \
-	fuzz_10.smt2 \
-	fuzz_11.smt2 \
-	fuzz_15.smt2 \
-	fuzz_16.smt2 \
-	fuzz_19.smt2 \
-	fuzz_20.smt2 \
-	fuzz_23.smt2 \
-	fuzz_24.smt2 \
-	fuzz_25.smt2 \
-	fuzz_26.smt2 \
-	fuzz_28.smt2 \
-	fuzz_29.smt2 \
-	fuzz_3_1.smt2 \
-	fuzz_3_10.smt2 \
-	fuzz_3_11.smt2 \
-	fuzz_3_12.smt2 \
-	fuzz_3_13.smt2 \
-	fuzz_3_14.smt2 \
-	fuzz_3_15.smt2 \
-	fuzz_3_2.smt2 \
-	fuzz_3_3.smt2 \
-	fuzz_3_4.smt2 \
-	fuzz_3_5.smt2 \
-	fuzz_3_6.smt2 \
-	fuzz_3_7.smt2 \
-	fuzz_3_8.smt2 \
-	fuzz_3_9.smt2 \
-	fuzz_30.smt2 \
-	fuzz_32.smt2 \
-	fuzz_34.smt2 \
-	fuzz_35.smt2 \
-	fuzz_37.smt2 \
-	fuzz_39.smt2 \
-	fuzz_4.smt2 \
-	fuzz_40.smt2 \
-	fuzz_41.smt2 \
-	fuzz_42.smt2 \
-	fuzz_43.smt2 \
-	fuzz_44.smt2 \
-	fuzz_45.smt2 \
-	fuzz_5_1.smt2 \
-	fuzz_5_2.smt2 \
-	fuzz_5_3.smt2 \
-	fuzz_5_4.smt2 \
-	fuzz_5_5.smt2 \
-	fuzz_5_6.smt2 \
-	fuzz_5.smt2 \
-	fuzz_51.smt2 \
-	fuzz_52.smt2 \
-	fuzz_6.smt2 \
-	fuzz_7.smt2 \
-	fuzz_8.smt2 \
-	fuzz_9.smt2 \
-	quant-fun-proc-unmacro.smt2 \
-	quant-fun-proc.smt2
-	
-EXTRA_DIST = $(TESTS) \
-	bug216.smt2.expect
-
-# synonyms for "check" in this directory
-.PHONY: regress regress1 test
-regress regress1 test: check
-
-# do nothing in this subdir
-.PHONY: regress0 regress2 regress3 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/quantifiers/Makefile b/test/regress/regress1/quantifiers/Makefile
deleted file mode 100644
index fcd888f99..000000000
--- a/test/regress/regress1/quantifiers/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../../../..
-srcdir = test/regress/regress1/quantifiers
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/regress/regress1/quantifiers/Makefile.am b/test/regress/regress1/quantifiers/Makefile.am
deleted file mode 100644
index af277af90..000000000
--- a/test/regress/regress1/quantifiers/Makefile.am
+++ /dev/null
@@ -1,103 +0,0 @@
-# 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
-
-# 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 =	\
-	bug802.smt2 \
-	006-cbqi-ite.smt2 \
-	AdditiveMethods_OwnedResults.Mz.smt2 \
-	ari118-bv-2occ-x.smt2 \
-	array-unsat-simp3.smt2 \
-	bignum_quant.smt2 \
-	bug_743.smt2 \
-	bug822.smt2 \
-	cdt-0208-to.smt2 \
-	gauss_init_0030.fof.smt2 \
-	inst-max-level-segf.smt2 \
-	intersection-example-onelane.proof-node22337.smt2 \
-	javafe.ast.StmtVec.009.smt2 \
-	model_6_1_bv.smt2 \
-	nested9_true-unreach-call.i_575.smt2 \
-	NUM878.smt2 \
-	opisavailable-12.smt2 \
-	psyco-107-bv.smt2 \
-	psyco-196.smt2 \
-	qbv-simple-2vars-vo.smt2 \
-	qbv-test-invert-bvcomp.smt2 \
-	qbv-test-invert-bvudiv-0.smt2 \
-	qbv-test-invert-bvudiv-1.smt2 \
-	qbv-test-invert-bvurem-1.smt2 \
-	qcft-javafe.filespace.TreeWalker.006.smt2 \
-	qcft-smtlib3dbc51.smt2 \
-	quaternion_ds1_symm_0428.fof.smt2 \
-	rew-to-0211-dd.smt2 \
-	ricart-agrawala6.smt2 \
-	RND_4_16.smt2 \
-	small-pipeline-fixpoint-3.smt2 \
-	smtlib384a03.smt2 \
-	smtlib46f14a.smt2 \
-	smtlibf957ea.smt2 \
-	stream-x2014-09-18-unsat.smt2 \
-	symmetric_unsat_7.smt2 \
-	anti-sk-simp.smt2 \
-	Arrays_Q1-noinfer.smt2 \
-	bi-artm-s.smt2 \
-	burns13.smt2 \
-	burns4.smt2 \
-	cbqi-sdlx-fixpoint-3-dd.smt2 \
-	ext-ex-deq-trigger.smt2 \
-	extract-nproc.smt2 \
-	florian-case-ax.smt2 \
-	is-even.smt2 \
-	mix-coeff.smt2 \
-	parametric-lists.smt2 \
-	psyco-001-bv.smt2 \
-	qbv-disequality3.smt2 \
-	qbv-test-invert-bvashr-0.smt2 \
-	qbv-test-invert-bvashr-1.smt2 \
-	qbv-test-invert-bvlshr-1.smt2 \
-	qbv-test-invert-bvmul-neq.smt2 \
-	qbv-test-invert-bvmul.smt2 \
-	qbv-test-invert-bvudiv-0-neq.smt2 \
-	qbv-test-invert-bvudiv-1-neq.smt2 \
-	qbv-test-invert-bvurem-1-neq.smt2 \
-	qbv-test-urem-rewrite.smt2 \
-	RND-small.smt2 \
-	RNDPRE_4_1-dd-nqe.smt2 \
-	set8.smt2 \
-	z3.620661-no-fv-trigger.smt2 \
-	arith-rec-fun.smt2 \
-	set3.smt2
-
-# removed because they take more than 20s
-#		javafe.ast.ArrayInit.35.smt2
-
-# FIXME: I've disabled these since they give different error messages on production and debug
-#	macro-subtype-param.smt2
-#	subtype-param-unk.smt2 
-#	subtype-param.smt2
-
-EXTRA_DIST = $(TESTS) \
-	set3.smt2
-
-# synonyms for "check" in this directory
-.PHONY: regress regress1 test
-regress regress1 test: check
-
-# do nothing in this subdir
-.PHONY: regress0 regress2 regress3 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/rels/Makefile.am b/test/regress/regress1/rels/Makefile.am
deleted file mode 100644
index c35ea2914..000000000
--- a/test/regress/regress1/rels/Makefile.am
+++ /dev/null
@@ -1,66 +0,0 @@
-# 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
-
-# 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 =	\
-	bv1p.cvc \
-	rel_pressure_0.cvc \
-	rel_tc_5_1.cvc \
-	set-strat.cvc \
-	addr_book_1_1.cvc \
-	addr_book_1.cvc \
-	bv1-unit.cvc \
-	bv1-unitb.cvc \
-	bv1.cvc \
-	bv1p-sat.cvc \
-	bv2.cvc \
-	iden_1_1.cvc \
-	join-eq-structure_0_1.cvc \
-	join-eq-structure-and.cvc \
-	join-eq-structure.cvc \
-	joinImg_0_1.cvc \
-	joinImg_0_2.cvc \
-	joinImg_1_1.cvc \
-	joinImg_1.cvc \
-	joinImg_2_1.cvc \
-	joinImg_2.cvc \
-	prod-mod-eq.cvc \
-	prod-mod-eq2.cvc \
-	rel_complex_3.cvc \
-	rel_complex_4.cvc \
-	rel_complex_5.cvc \
-	rel_mix_0_1.cvc \
-	rel_tc_10_1.cvc \
-	rel_tc_4_1.cvc \
-	rel_tc_4.cvc \
-	rel_tc_6.cvc \
-	rel_tc_9_1.cvc \
-	rel_tp_2.cvc \
-	rel_tp_join_2_1.cvc \
-	strat_0_1.cvc \
-	strat.cvc
-
-EXTRA_DIST = $(TESTS) \
-	garbage_collect.cvc 
-
-# synonyms for "check" in this directory
-.PHONY: regress regress1 test
-regress regress1 test: check
-
-# do nothing in this subdir
-.PHONY: regress0 regress2 regress3 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/rewriterules/Makefile b/test/regress/regress1/rewriterules/Makefile
deleted file mode 100644
index 0eb938072..000000000
--- a/test/regress/regress1/rewriterules/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../../../..
-srcdir = test/regress/regress1/rewriterules
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/regress/regress1/rewriterules/Makefile.am b/test/regress/regress1/rewriterules/Makefile.am
deleted file mode 100644
index 6c5ce19fb..000000000
--- a/test/regress/regress1/rewriterules/Makefile.am
+++ /dev/null
@@ -1,55 +0,0 @@
-# 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 =	\
-	reachability_back_to_the_future.smt2 \
-	read5.smt2 \
-	length_gen.smt2 \
-	length_gen_020.smt2 \
-	length_gen_020_sat.smt2 \
-	length_gen_040.smt2 \
-	length_gen_040_lemma.smt2 \
-	length_gen_040_lemma_trigger.smt2 \
-	datatypes_sat.smt2
-
-
-EXTRA_DIST = $(TESTS) \
-	datatypes_clark_quantification.smt2 \
-	datatypes2.smt2 \
-	datatypes3.smt2 \
-	length_gen_010_lemma.smt2 \
-	length_gen_010.smt2 \
-	length_gen_080.smt2 \
-	length_gen_160_lemma.smt2 \
-	length_gen_inv_160.smt2 \
-	length_trick3_int.smt2 \
-	length_trick3.smt2 \
-	set_A_new_fast_tableau-base_sat.smt2 \
-	set_A_new_fast_tableau-base.smt2 \
-	test_guards.smt2 \
-	why3_vstte10_max_sum_harness2.smt2
-
-# synonyms for "check" in this directory
-.PHONY: regress regress1 test
-regress regress1 test: check
-
-# do nothing in this subdir
-.PHONY: regress0 regress2 regress3 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/sep/Makefile b/test/regress/regress1/sep/Makefile
deleted file mode 100644
index 5733b5526..000000000
--- a/test/regress/regress1/sep/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../../../..
-srcdir = test/regress/regress1/sep
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/regress/regress1/sep/Makefile.am b/test/regress/regress1/sep/Makefile.am
deleted file mode 100644
index bda7e4484..000000000
--- a/test/regress/regress1/sep/Makefile.am
+++ /dev/null
@@ -1,60 +0,0 @@
-# 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
-
-# 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 =	\
-	loop-1220.smt2 \
-	sep-simp-unc.smt2 \
-	split-find-unsat.smt2 \
-	split-find-unsat-w-emp.smt2 \
-	dispose-list-4-init.smt2 \
-	finite-witness-sat.smt2 \
-	sep-find2.smt2 \
-	sep-fmf-priority.smt2 \
-	sep-neg-1refine.smt2 \
-	sep-nterm-again.smt2 \
-	chain-int.smt2 \
-	crash1220.smt2 \
-	emp2-quant-unsat.smt2 \
-	fmf-nemp-2.smt2 \
-	pto-04.smt2 \
-	quant_wand.smt2 \
-	sep-02.smt2 \
-	sep-03.smt2 \
-	sep-neg-nstrict.smt2 \
-	sep-neg-nstrict2.smt2 \
-	sep-neg-simple.smt2 \
-	sep-neg-swap.smt2 \
-	sep-nterm-val-model.smt2 \
-	simple-neg-sat.smt2 \
-	wand-0526-sat.smt2 \
-	wand-false.smt2 \
-	wand-nterm-simp.smt2 \
-	wand-nterm-simp2.smt2 \
-	wand-simp-sat.smt2 \
-	wand-simp-sat2.smt2 \
-	wand-simp-unsat.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 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/sets/Makefile b/test/regress/regress1/sets/Makefile
deleted file mode 100644
index e78e958ad..000000000
--- a/test/regress/regress1/sets/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../../../..
-srcdir = test/regress/regress1/sets
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/regress/regress1/sets/Makefile.am b/test/regress/regress1/sets/Makefile.am
deleted file mode 100644
index f52ab44e7..000000000
--- a/test/regress/regress1/sets/Makefile.am
+++ /dev/null
@@ -1,56 +0,0 @@
-# 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
-
-# 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 =	\
-	sets-disequal.smt2 \
-	card-vc6-minimized.smt2 \
-	card-4.smt2 \
-	fuzz15201.smt2 \
-	insert_invariant_37_2.smt2 \
-	remove_check_free_31_6.smt2 \
-	TalkingAboutSets.hs.fqout.cvc4.3577.smt2 \
-	arjun-set-univ.cvc \
-	card-3.smt2 \
-	card-5.smt2 \
-	card-6.smt2 \
-	card-7.smt2 \
-	copy_check_heap_access_33_4.smt2 \
-	deepmeas0.hs.fqout.cvc4.41.smt2 \
-	fuzz14418.smt2 \
-	fuzz31811.smt2 \
-	lemmabug-ListElts317minimized.smt2 \
-	ListElem.hs.fqout.cvc4.38.smt2 \
-	ListElts.hs.fqout.cvc4.317.smt2 \
-	sets-tuple-poly.cvc \
-	sharingbug.smt2 \
-	UniqueZipper.hs.1030minimized.cvc4.smt2 \
-	UniqueZipper.hs.1030minimized2.cvc4.smt2 \
-	UniqueZipper.hs.fqout.cvc4.10.smt2 \
-	UniqueZipper.hs.fqout.cvc4.1832.smt2 \
-	univ-set-uf-elim.smt2
-	
-EXTRA_DIST = $(TESTS) \
-	setofsets-disequal.smt2 
-
-# synonyms for "check" in this directory
-.PHONY: regress regress1 test
-regress regress1 test: check
-
-# do nothing in this subdir
-.PHONY: regress0 regress2 regress3 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/strings/Makefile b/test/regress/regress1/strings/Makefile
deleted file mode 100644
index b4a9df5b2..000000000
--- a/test/regress/regress1/strings/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../../../..
-srcdir = test/regress/regress1/strings
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/regress/regress1/strings/Makefile.am b/test/regress/regress1/strings/Makefile.am
deleted file mode 100644
index 7e9242e73..000000000
--- a/test/regress/regress1/strings/Makefile.am
+++ /dev/null
@@ -1,87 +0,0 @@
-# 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
-
-# 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 =	\
-	cmu-5042-0707-2.smt2 \
-	artemis-0512-nonterm.smt2 \
-	bug615.smt2 \
-	bug682.smt2 \
-	bug686dd.smt2 \
-	bug768.smt2 \
-	bug799-min.smt2 \
-	chapman150408.smt2 \
-	cmu-inc-nlpp-071516.smt2 \
-	cmu-substr-rw.smt2 \
-	crash-1019.smt2 \
-	csp-prefix-exp-bug.smt2 \
-	fmf001.smt2 \
-	fmf002.smt2 \
-	idof-nconst-index.smt2 \
-	kaluza-fl.smt2 \
-	loop007.smt2 \
-	loop008.smt2 \
-	loop009.smt2 \
-	nf-ff-contains-abs.smt2 \
-	norn-360.smt2 \
-	norn-ab.smt2 \
-	norn-nel-bug-052116.smt2 \
-	pierre150331.smt2 \
-	regexp001.smt2 \
-	regexp002.smt2 \
-	reloop.smt2 \
-	str006.smt2 \
-	strings-index-empty.smt2 \
-	strip-endpt-sound.smt2 \
-	substr001.smt2 \
-	type002.smt2 \
-	type003.smt2 \
-	username_checker_min.smt2 \
-	at001.smt2 \
-	cmu-2db2-extf-reg.smt2 \
-	gm-inc-071516-2.smt2 \
-	idof-handg.smt2 \
-	idof-neg-index.smt2 \
-	idof-triv.smt2 \
-	ilc-l-nt.smt2 \
-	issue1105.smt2 \
-	loop002.smt2 \
-	loop003.smt2 \
-	loop004.smt2 \
-	loop005.smt2 \
-	loop006.smt2 \
-	norn-simp-rew-sat.smt2 \
-	regexp003.smt2 \
-	repl-empty-sem.smt2 \
-	repl-soundness-sem.smt2 \
-	str001.smt2 \
-	str002.smt2 \
-	str007.smt2 \
-	rew-020618.smt2 \
-	double-replace.smt2 \
-	string-unsound-sem.smt2 \
-	goodAI.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 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/sygus/Makefile b/test/regress/regress1/sygus/Makefile
deleted file mode 100644
index c8dc4fdf7..000000000
--- a/test/regress/regress1/sygus/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-topdir = ../../../..
-srcdir = test/regress/regress1/sygus
-
-include $(topdir)/Makefile.subdir
-
-# synonyms for "check"
-.PHONY: test
-test: check
diff --git a/test/regress/regress1/sygus/Makefile.am b/test/regress/regress1/sygus/Makefile.am
deleted file mode 100644
index c44c5034d..000000000
--- a/test/regress/regress1/sygus/Makefile.am
+++ /dev/null
@@ -1,81 +0,0 @@
-# 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
-
-# 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 = \
-	hd-sdiv.sy \
-	stopwatch-bt.sy \
-	VC22_a.sy \
-	unbdd_inv_gen_ex7.sy \
-	real-grammar.sy \
-	cegar1.sy \
-	cggmp.sy \
-	clock-inc-tuple.sy \
-	dup-op.sy \
-	fg_polynomial3.sy \
-	hd-01-d1-prog.sy \
-	icfp_14.12.sy \
-	icfp_14.12-flip-args.sy \
-	icfp_28_10.sy \
-	icfp_easy-ite.sy \
-	inv-example.sy \
-	inv-unused.sy \
-	multi-fun-polynomial2.sy \
-	no-flat-simp.sy \
-	process-10-vars.sy \
-	tl-type.sy \
-	tl-type-4x.sy \
-	twolets2-orig.sy \
-	unbdd_inv_gen_winf1.sy \
-	array_search_2.sy \
-	array_sum_2_5.sy \
-	commutative.sy \
-	constant.sy \
-	dt-test-ns.sy \
-	hd-19-d1-prog-dup-op.sy \
-	list-head-x.sy \
-	max.sy \
-	nflat-fwd-3.sy \
-	nflat-fwd.sy \
-	nia-max-square-ns.sy \
-	no-mention.sy \
-	qe.sy \
-	strings-concat-3-args.sy \
-	strings-double-rec.sy \
-	strings-small.sy \
-	strings-template-infer-unused.sy \
-	strings-template-infer.sy \
-	strings-trivial-simp.sy \
-	strings-trivial-two-type.sy \
-	strings-trivial.sy \
-	sygus-dt.sy \
-	tl-type-0.sy \
-	triv-type-mismatch-si.sy \
-	twolets1.sy
-
-EXTRA_DIST = $(TESTS) \
-	enum-test.sy 
-
-# Base16_1.sy
-
-# synonyms for "check" in this directory
-.PHONY: regress regress1 test
-regress regress1 test: check
-
-# do nothing in this subdir
-.PHONY: regress0 regress2 regress3 regress4
-regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/uflia/Makefile.am b/test/regress/regress1/uflia/Makefile.am
deleted file mode 100644
index c9a5ee372..000000000
--- a/test/regress/regress1/uflia/Makefile.am
+++ /dev/null
@@ -1,41 +0,0 @@
-# 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
-
-# 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 = \
-	FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 \
-	microwave21.ec.minimized.smt2 \
-	simple_cyclic2.smt2 \
-	DRAGON_11_e1_2450.ec.minimized.smt2 \
-	FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 \
-	speed2_e8_449_e8_517.ec.smt2 \
-	stalmark_e7_27_e7_31.ec.smt2
-
-
-EXTRA_DIST = $(TESTS) \
-	DRAGON_11_e1_2450.ec.minimized.smt2.expect \
-	FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect \
-	speed2_e8_449_e8_517.ec.smt2.expect \
-	stalmark_e7_27_e7_31.ec.smt2.expect
-
-# synonyms for "check" in this directory
-.PHONY: regress regress1 test
-regress regress1 test: check
-
-# do nothing in this subdir
-.PHONY: regress0 regress2 regress3 regress4
-regress0 regress2 regress3 regress4: