diff options
Diffstat (limited to 'test/regress/regress1')
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: |