diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-03-21 13:10:24 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-21 13:10:24 -0700 |
| commit | b8db52f9bad5b1053810c93f0067de8423349da3 (patch) | |
| tree | bd937d795052073645a87032eaf8ecf0be2e11cb /test/regress/regress0 | |
| parent | be2702490d684c100ba6abe76ee156078a9aa621 (diff) | |
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.
Diffstat (limited to 'test/regress/regress0')
61 files changed, 0 insertions, 2542 deletions
diff --git a/test/regress/regress0/Makefile b/test/regress/regress0/Makefile deleted file mode 100644 index 894759aa3..000000000 --- a/test/regress/regress0/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../.. -srcdir = test/regress/regress0 - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am deleted file mode 100644 index 7127c5739..000000000 --- a/test/regress/regress0/Makefile.am +++ /dev/null @@ -1,196 +0,0 @@ -SUBDIRS = . expect arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets rels parser sygus sep nl ho -DIST_SUBDIRS = $(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 +=" - -# Regression tests for SMT inputs -SMT_TESTS = \ - distinct.smt \ - flet.smt \ - flet2.smt \ - fuzz_1.smt \ - fuzz_3.smt \ - ineq_basic.smt \ - ineq_slack.smt \ - ite_real_int_type.smt \ - ite_real_valid.smt \ - let.smt \ - let2.smt \ - simplification_bug.smt \ - simplification_bug2.smt \ - simple.smt \ - simple2.smt \ - simple-lra.smt \ - simple-rdl.smt \ - simple-uf.smt \ - constant-rewrite.smt - -# Regression tests for SMT2 inputs -SMT2_TESTS = \ - arrayinuf_declare.smt2 \ - boolean-terms-kernel1.smt2 \ - boolean-terms-bug-array.smt2 \ - chained-equality.smt2 \ - ite2.smt2 \ - ite3.smt2 \ - ite4.smt2 \ - simple-lra.smt2 \ - simple-rdl.smt2 \ - simple-uf.smt2 \ - parallel-let.smt2 \ - get-value-incremental.smt2 \ - get-value-reals.smt2 \ - get-value-ints.smt2 \ - get-value-reals-ints.smt2 \ - hung13sdk_output1.smt2 \ - hung10_itesdk_output2.smt2 \ - hung10_itesdk_output1.smt2 \ - hung13sdk_output2.smt2 \ - declare-funs.smt2 \ - declare-fun-is-match.smt2 \ - issue1063-overloading-dt-cons.smt2 \ - issue1063-overloading-dt-sel.smt2 \ - issue1063-overloading-dt-fun.smt2 \ - reset-assertions.smt2 \ - rec-fun-const-parse-bug.smt2 - -# Regression tests for PL inputs -CVC_TESTS = \ - boolean-prec.cvc \ - boolean-terms.cvc \ - ite.cvc \ - let.cvc \ - logops.01.cvc \ - logops.02.cvc \ - logops.03.cvc \ - logops.04.cvc \ - logops.05.cvc \ - simple.cvc \ - smallcnf.cvc \ - test9.cvc \ - test11.cvc \ - uf20-03.cvc \ - wiki.01.cvc \ - wiki.02.cvc \ - wiki.03.cvc \ - wiki.04.cvc \ - wiki.05.cvc \ - wiki.06.cvc \ - wiki.07.cvc \ - wiki.08.cvc \ - wiki.09.cvc \ - wiki.10.cvc \ - wiki.11.cvc \ - wiki.12.cvc \ - wiki.13.cvc \ - wiki.14.cvc \ - wiki.15.cvc \ - wiki.16.cvc \ - wiki.17.cvc \ - wiki.18.cvc \ - wiki.19.cvc \ - wiki.20.cvc \ - wiki.21.cvc \ - queries0.cvc \ - print_lambda.cvc \ - cvc3.userdoc.01.cvc \ - cvc3.userdoc.02.cvc \ - cvc3.userdoc.03.cvc \ - cvc3.userdoc.04.cvc \ - cvc3.userdoc.05.cvc \ - cvc3.userdoc.06.cvc - -# Regression tests for TPTP inputs -TPTP_TESTS = - -# Regression tests derived from bug reports -BUG_TESTS = \ - smt2output.smt2 \ - bug32.cvc \ - bug49.smt \ - bug161.smt \ - bug164.smt \ - bug167.smt \ - bug168.smt \ - bug187.smt2 \ - bug217.smt2 \ - bug220.smt2 \ - bug239.smt \ - bug274.cvc \ - bug288.smt \ - bug288b.smt \ - bug288c.smt \ - buggy-ite.smt2 \ - bug303.smt2 \ - bug310.cvc \ - bug322.cvc \ - bug322b.cvc \ - bug339.smt2 \ - bug365.smt2 \ - bug382.smt2 \ - bug383.smt2 \ - bug398.smt2 \ - bug421.smt2 \ - bug421b.smt2 \ - bug480.smt2 \ - bug484.smt2 \ - bug486.cvc \ - bug512.minimized.smt2 \ - bug521.minimized.smt2 \ - bug522.smt2 \ - bug528a.smt2 \ - bug541.smt2 \ - bug544.smt2 \ - bug548a.smt2 \ - bug576.smt2 \ - bug576a.smt2 \ - bug578.smt2 \ - bug586.cvc \ - bug595.cvc \ - bug596.cvc \ - bug596b.cvc \ - bug605.cvc \ - bug639.smt2 \ - bt-test-00.smt2 \ - bt-test-01.smt2 \ - bug1247.smt2 - -TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) - -# bug512 -- taking too long, --time-per not working perhaps? in any case, -# we have a minimized version still getting tested -# bug639 -- still fails, reopened bug -# bug585 -- contains subrange type (not supported) - - -EXTRA_DIST = $(TESTS) - -# and make sure to distribute it -EXTRA_DIST += $(DISABLED_TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/arith/Makefile b/test/regress/regress0/arith/Makefile deleted file mode 100644 index 6b570d785..000000000 --- a/test/regress/regress0/arith/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/arith - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am deleted file mode 100644 index 8a12d7d13..000000000 --- a/test/regress/regress0/arith/Makefile.am +++ /dev/null @@ -1,68 +0,0 @@ -SUBDIRS = . integers - -# 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 = \ - arith.01.cvc \ - arith.02.cvc \ - arith.03.cvc \ - delta-minimized-row-vector-bug.smt \ - fuzz_3-eq.smt \ - leq.01.smt \ - mod.01.smt2 \ - div.01.smt2 \ - div.02.smt2 \ - div.04.smt2 \ - div.05.smt2 \ - div.07.smt2 \ - mult.01.smt2 \ - bug443.delta01.smt \ - miplib.cvc \ - miplib2.cvc \ - miplib4.cvc \ - miplibtrick.smt \ - bug547.2.smt2 \ - bug569.smt2 \ - mod-simp.smt2 - -EXTRA_DIST = $(TESTS) \ - miplib-opt1217--27.smt \ - miplib-pp08a-3000.smt \ - miplib-opt1217--27.smt.expect \ - miplib-pp08a-3000.smt.expect - -#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 regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/arith/integers/Makefile b/test/regress/regress0/arith/integers/Makefile deleted file mode 100644 index 4144299bd..000000000 --- a/test/regress/regress0/arith/integers/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../../.. -srcdir = test/regress/regress0/arith/integers - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am deleted file mode 100644 index 203598490..000000000 --- a/test/regress/regress0/arith/integers/Makefile.am +++ /dev/null @@ -1,53 +0,0 @@ -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 = \ - arith-int-042.cvc \ - arith-int-042.min.cvc - -EXTRA_DIST = $(TESTS) \ - arith-int-014.cvc \ - arith-int-015.cvc \ - arith-int-021.cvc \ - arith-int-023.cvc \ - arith-int-025.cvc \ - arith-int-079.cvc - -#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 regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/arrays/Makefile b/test/regress/regress0/arrays/Makefile deleted file mode 100644 index 1f480a4ad..000000000 --- a/test/regress/regress0/arrays/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/arrays - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am deleted file mode 100644 index bdc7352f5..000000000 --- a/test/regress/regress0/arrays/Makefile.am +++ /dev/null @@ -1,70 +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 = \ - arrays0.smt2 \ - arrays1.smt2 \ - arrays2.smt2 \ - arrays3.smt2 \ - arrays4.smt2 \ - incorrect1.smt \ - incorrect2.smt \ - incorrect2.minimized.smt \ - incorrect3.smt \ - incorrect4.smt \ - incorrect5.smt \ - incorrect6.smt \ - incorrect7.smt \ - incorrect8.smt \ - incorrect8.minimized.smt \ - incorrect9.smt \ - incorrect10.smt \ - incorrect11.smt \ - swap_t1_np_nf_ai_00005_007.cvc.smt \ - x2.smt \ - x3.smt \ - bug272.smt \ - bug272.minimized.smt \ - constarr.smt2 \ - constarr2.smt2 \ - constarr.cvc \ - constarr2.cvc \ - bug637.delta.smt2 \ - bool-array.smt2 - -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" -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/aufbv/Makefile b/test/regress/regress0/aufbv/Makefile deleted file mode 100644 index 7dd17882f..000000000 --- a/test/regress/regress0/aufbv/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/aufbv - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am deleted file mode 100644 index 8fda89ad7..000000000 --- a/test/regress/regress0/aufbv/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 - -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 = \ - bug00.smt \ - bug338.smt2 \ - bug347.smt \ - bug451.smt \ - bug509.smt \ - bug580.delta.smt2 \ - try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \ - try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smt \ - diseqprop.01.smt \ - wchains010ue.delta01.smt \ - wchains010ue.delta02.smt \ - dubreva005ue.delta01.smt \ - fuzz00.smt \ - fuzz01.smt \ - fuzz01.delta01.smt \ - fuzz02.delta01.smt \ - fuzz02.smt \ - fuzz03.delta01.smt \ - fuzz03.smt \ - fuzz04.delta01.smt \ - fuzz04.smt \ - fuzz05.delta01.smt \ - fuzz05.smt \ - fuzz06.delta01.smt \ - fuzz06.smt \ - fuzz07.smt \ - fuzz08.smt \ - fuzz09.smt \ - fuzz11.smt \ - fuzz12.smt \ - fuzz13.smt \ - fuzz14.smt \ - fuzz15.smt \ - fifo32bc06k08.delta01.smt \ - rewrite_bug.smt \ - array_rewrite_bug.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" -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/auflia/Makefile b/test/regress/regress0/auflia/Makefile deleted file mode 100644 index da859f7e3..000000000 --- a/test/regress/regress0/auflia/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/auflia - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am deleted file mode 100644 index 8ce7ae134..000000000 --- a/test/regress/regress0/auflia/Makefile.am +++ /dev/null @@ -1,52 +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 = \ - bug336.smt2 \ - fuzz01.delta01.smt \ - fuzz02.smt \ - fuzz03.smt \ - fuzz04.smt \ - fuzz05.smt \ - fuzz-error232.smt \ - fuzz-error1099.smt \ - a17.smt \ - error72.delta2.smt \ - x2.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" -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/bv/Makefile b/test/regress/regress0/bv/Makefile deleted file mode 100644 index c9ec3204c..000000000 --- a/test/regress/regress0/bv/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/bv - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am deleted file mode 100644 index eeeff7391..000000000 --- a/test/regress/regress0/bv/Makefile.am +++ /dev/null @@ -1,130 +0,0 @@ -SUBDIRS = . core - -# 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 +=" - -# FIXME: Proof checking takes too long. Add this back. -# fuzz15.delta01.smt - -# Regression tests for SMT inputs -SMT_TESTS = \ - fuzz01.smt \ - fuzz02.delta01.smt \ - fuzz02.smt \ - fuzz03.smt \ - fuzz04.smt \ - fuzz05.smt \ - fuzz06.smt \ - fuzz07.smt \ - fuzz08.smt \ - fuzz09.smt \ - fuzz10.smt \ - fuzz11.smt \ - fuzz12.smt \ - fuzz13.smt \ - fuzz14.smt \ - fuzz16.delta01.smt \ - fuzz17.delta01.smt \ - fuzz18.delta01.smt \ - fuzz18.delta02.smt \ - fuzz18.delta03.smt \ - fuzz18.smt \ - fuzz19.delta01.smt \ - fuzz19.smt \ - fuzz20.delta01.smt \ - fuzz20.smt \ - fuzz21.delta01.smt \ - fuzz21.smt \ - fuzz22.delta01.smt \ - fuzz22.smt \ - fuzz23.delta01.smt \ - fuzz23.smt \ - fuzz24.delta01.smt \ - fuzz24.smt \ - fuzz25.delta01.smt \ - fuzz25.smt \ - fuzz26.delta01.smt \ - fuzz26.smt \ - fuzz27.delta01.smt \ - fuzz27.smt \ - fuzz28.delta01.smt \ - fuzz28.smt \ - fuzz29.delta01.smt \ - fuzz29.smt \ - fuzz30.delta01.smt \ - fuzz30.smt \ - fuzz31.delta01.smt \ - fuzz31.smt \ - fuzz32.delta01.smt \ - fuzz32.smt \ - fuzz33.delta01.smt \ - fuzz33.smt \ - fuzz34.delta01.smt \ - fuzz35.delta01.smt \ - fuzz35.smt \ - fuzz36.delta01.smt \ - fuzz36.smt \ - fuzz37.delta01.smt \ - fuzz37.smt \ - fuzz38.delta01.smt \ - fuzz39.delta01.smt \ - fuzz39.smt \ - fuzz40.delta01.smt \ - fuzz40.smt \ - fuzz41.smt \ - calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt \ - smtcompbug.smt \ - unsound1-reduced.smt2 \ - bv2nat-ground-c.smt2 \ - bv2nat-simp-range.smt2 \ - bv-int-collapse1.smt2 \ - bv-int-collapse2.smt2 \ - divtest_2_5.smt2 \ - divtest_2_6.smt2 \ - mul-neg-unsat.smt2 \ - mul-negpow2.smt2 \ - bvmul-pow2-only.smt2 \ - mult-pow2-negative.smt2 - -# Regression tests for PL inputs -CVC_TESTS = bvsimple.cvc sizecheck.cvc - -# Regression tests derived from bug reports -BUG_TESTS = \ - bug260a.smt \ - bug260b.smt \ - bug440.smt \ - bug733.smt2 \ - bug734.smt2 - -TESTS = $(SMT_TESTS) $(CVC_TESTS) $(BUG_TESTS) - -EXTRA_DIST = $(TESTS) \ - test00.smt \ - bvcomp.cvc - -# synonyms for "check" in this directory -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/bv/core/Makefile b/test/regress/regress0/bv/core/Makefile deleted file mode 100644 index 15e8e6220..000000000 --- a/test/regress/regress0/bv/core/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../../.. -srcdir = test/regress/regress0/bv/core - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am deleted file mode 100644 index ce65bcaf6..000000000 --- a/test/regress/regress0/bv/core/Makefile.am +++ /dev/null @@ -1,96 +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 = \ - concat-merge-0.smt \ - concat-merge-1.smt \ - concat-merge-2.smt \ - concat-merge-3.smt \ - extract-concat-0.smt \ - extract-concat-1.smt \ - extract-concat-2.smt \ - extract-concat-3.smt \ - extract-concat-4.smt \ - extract-concat-5.smt \ - extract-concat-6.smt \ - extract-concat-7.smt \ - extract-concat-8.smt \ - extract-concat-9.smt \ - extract-concat-10.smt \ - extract-concat-11.smt \ - extract-constant.smt \ - extract-extract-0.smt \ - extract-extract-1.smt \ - extract-extract-2.smt \ - extract-extract-3.smt \ - extract-extract-4.smt \ - extract-extract-5.smt \ - extract-extract-6.smt \ - extract-extract-7.smt \ - extract-extract-8.smt \ - extract-extract-9.smt \ - extract-extract-10.smt \ - extract-extract-11.smt \ - extract-whole-0.smt \ - extract-whole-1.smt \ - extract-whole-2.smt \ - extract-whole-3.smt \ - extract-whole-4.smt \ - equality-00.smt \ - equality-01.smt \ - equality-02.smt \ - equality-05.smt \ - bv_eq_diamond10.smt \ - slice-01.smt \ - slice-02.smt \ - slice-03.smt \ - slice-04.smt \ - slice-05.smt \ - slice-06.smt \ - slice-07.smt \ - slice-08.smt \ - slice-09.smt \ - slice-10.smt \ - slice-11.smt \ - slice-12.smt \ - slice-13.smt \ - slice-14.smt \ - slice-15.smt \ - slice-16.smt \ - slice-17.smt \ - slice-18.smt \ - slice-19.smt \ - slice-20.smt \ - a78test0002.smt \ - a95test0002.smt \ - bitvec0.smt \ - bitvec2.smt \ - bitvec5.smt \ - bitvec7.smt - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/datatypes/Makefile b/test/regress/regress0/datatypes/Makefile deleted file mode 100644 index dc577ad8b..000000000 --- a/test/regress/regress0/datatypes/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/datatypes - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am deleted file mode 100644 index 55956abaa..000000000 --- a/test/regress/regress0/datatypes/Makefile.am +++ /dev/null @@ -1,105 +0,0 @@ -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 = \ - tuple.cvc \ - tuple-model.cvc \ - tuple-record-bug.cvc \ - rec1.cvc \ - rec2.cvc \ - rec4.cvc \ - datatype.cvc \ - datatype0.cvc \ - datatype1.cvc \ - datatype2.cvc \ - datatype3.cvc \ - datatype4.cvc \ - datatype13.cvc \ - empty_tuprec.cvc \ - mutually-recursive.cvc \ - pair-real-bool.smt2 \ - pair-bool-bool.cvc \ - rewriter.cvc \ - typed_v10l30054.cvc \ - typed_v1l80005.cvc \ - typed_v2l30079.cvc \ - typed_v3l20092.cvc \ - typed_v5l30069.cvc \ - boolean-equality.cvc \ - boolean-terms-datatype.cvc \ - boolean-terms-parametric-datatype-1.cvc \ - boolean-terms-parametric-datatype-2.cvc \ - boolean-terms-tuple.cvc \ - boolean-terms-record.cvc \ - boolean-terms-rewrite.cvc \ - some-boolean-tests.cvc \ - v10l40099.cvc \ - v2l40025.cvc \ - v3l60006.cvc \ - v5l30058.cvc \ - bug286.cvc \ - bug438.cvc \ - bug438b.cvc \ - wrong-sel-simp.cvc \ - tenum-bug.smt2 \ - cdt-non-canon-stream.smt2 \ - stream-singleton.smt2 \ - is_test.smt2 \ - bug625.smt2 \ - cdt-model-cade15.smt2 \ - sc-cdt1.smt2 \ - conqueue-dt-enum-iloop.smt2 \ - coda_simp_model.smt2 \ - Test1-tup-mp.cvc \ - dt-param-card4-bool-sat.smt2 \ - bug604.smt2 \ - bug597-rbt.smt2 \ - example-dailler-min.smt2 \ - dt-2.6.smt2 \ - dt-sel-2.6.smt2 \ - dt-param-2.6.smt2 \ - dt-match-pat-param-2.6.smt2 \ - tuple-no-clash.cvc \ - jsat-2.6.smt2 \ - model-subterms-min.smt2 \ - issue1433.smt2 \ - tuples-empty.smt2 \ - tuples-multitype.smt2 \ - datatype-dump.cvc - -# rec5 -- no longer support subrange types -FAILING_TESTS = \ - datatype-dump.cvc - -EXTRA_DIST = $(TESTS) - -# and make sure to distribute it -EXTRA_DIST += \ - $(FAILING_TESTS) - -# synonyms for "check" -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/decision/Makefile b/test/regress/regress0/decision/Makefile deleted file mode 100644 index 734d863c9..000000000 --- a/test/regress/regress0/decision/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/decision - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am deleted file mode 100644 index b70ee1575..000000000 --- a/test/regress/regress0/decision/Makefile.am +++ /dev/null @@ -1,73 +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 = \ - wchains010ue.delta02.smt \ - bitvec0.smt \ - bitvec0.delta01.smt \ - bitvec5.smt \ - quant-ex1.smt2 \ - uflia-xs-09-16-3-4-1-5.delta03.smt \ - aufbv-fuzz01.smt \ - bug347.smt \ - bug374a.smt \ - bug374b.smt2 \ - error20.smt \ - error20.delta01.smt \ - error122.smt \ - error122.delta01.smt \ - error3.delta01.smt \ - pp-regfile.delta01.smt \ - pp-regfile.delta02.smt - -EXTRA_DIST = $(TESTS) \ - aufbv-fuzz01.smt.expect \ - pp-regfile.delta01.smt.expect \ - bitvec0.delta01.smt.expect \ - pp-regfile.delta02.smt.expect \ - uflia-xs-09-16-3-4-1-5.delta03.smt.expect \ - bitvec0.smt.expect \ - bitvec5.smt.expect \ - wchains010ue.delta02.smt.expect \ - bug347.smt.expect \ - bug374a.smt.expect \ - bug374b.smt2.expect \ - wchains010ue.smt.expect \ - just_sat.expect \ - quant-ex1.smt2.expect \ - just_unsat.expect - -#if CVC4_BUILD_PROFILE_COMPETITION -#else -#TESTS += \ -# error.cvc -#endif -# -# and make sure to distribute it -#EXTRA_DIST += \ -# error.cvc - -# synonyms for "check" -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/expect/Makefile.am b/test/regress/regress0/expect/Makefile.am deleted file mode 100644 index e1518d84d..000000000 --- a/test/regress/regress0/expect/Makefile.am +++ /dev/null @@ -1,44 +0,0 @@ -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 = \ - scrub.01.smt \ - scrub.02.smt \ - scrub.03.smt2 \ - scrub.04.smt2 \ - scrub.06.cvc \ - scrub.07.sy \ - scrub.08.sy \ - scrub.09.p - -EXTRA_DIST = $(TESTS) \ - scrub.01.smt.expect \ - scrub.03.smt2.expect \ - scrub.07.sy.expect - -# synonyms for "check" in this directory -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/fmf/Makefile b/test/regress/regress0/fmf/Makefile deleted file mode 100644 index 1e68a1e9e..000000000 --- a/test/regress/regress0/fmf/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/fmf - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am deleted file mode 100644 index 297cdfaf3..000000000 --- a/test/regress/regress0/fmf/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 - -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 = \ - array_card.smt2 \ - QEpres-uf.855035.smt \ - Arrow_Order-smtlib.778341.smt \ - fc-simple.smt2 \ - fc-unsat-tot-2.smt2 \ - fc-unsat-pent.smt2 \ - Hoare-z3.931718.smt \ - syn002-si-real-int.smt2 \ - krs-sat.smt2 \ - forall_unit_data2.smt2 \ - sc_bad_model_1221.smt2 \ - fd-false.smt2 \ - tail_rec.smt2 \ - fmc_unsound_model.smt2 \ - bounded_sets.smt2 \ - fmf-strange-bounds-2.smt2 \ - bug652.smt2 \ - bug782.smt2 \ - quant_real_univ.cvc \ - bug-041417-set-options.cvc \ - cruanes-no-minimal-unk.smt2 \ - no-minimal-sat.smt2 \ - sat-logic.smt2 - -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 regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/ho/Makefile.am b/test/regress/regress0/ho/Makefile.am deleted file mode 100644 index d0903094e..000000000 --- a/test/regress/regress0/ho/Makefile.am +++ /dev/null @@ -1,50 +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 = \ - cong.smt2 \ - ext-ho-nested-lambda-model.smt2 \ - declare-fun-variants.smt2 \ - ext-ho.smt2 \ - trans.smt2 \ - ext-finite-unsat.smt2 \ - ext-sat.smt2 \ - cong-full-apply.smt2 \ - def-fun-flatten.smt2 \ - lambda-equality-non-canon.smt2 \ - ite-apply-eq.smt2 \ - apply-collapse-unsat.smt2 \ - apply-collapse-sat.smt2 \ - ext-sat-partial-eval.smt2 \ - modulo-func-equality.smt2 \ - ho-matching-enum.smt2 \ - ho-matching-nested-app.smt2 \ - simple-matching.smt2 \ - simple-matching-partial.smt2 - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/lemmas/Makefile b/test/regress/regress0/lemmas/Makefile deleted file mode 100644 index 96e24225b..000000000 --- a/test/regress/regress0/lemmas/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/lemmas - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/lemmas/Makefile.am b/test/regress/regress0/lemmas/Makefile.am deleted file mode 100644 index 89f9d83a3..000000000 --- a/test/regress/regress0/lemmas/Makefile.am +++ /dev/null @@ -1,41 +0,0 @@ -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 +=" - -# Regression tests for SMT inputs -SMT_TESTS = \ - clocksynchro_5clocks.main_invar.base.model.smt \ - sc_init_frame_gap.induction.smt \ - mode_cntrl.induction.smt \ - fs_not_sc_seen.induction.smt - -TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/nl/Makefile b/test/regress/regress0/nl/Makefile deleted file mode 100644 index 627bdbde9..000000000 --- a/test/regress/regress0/nl/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/nl - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am deleted file mode 100644 index 0347dbd8b..000000000 --- a/test/regress/regress0/nl/Makefile.am +++ /dev/null @@ -1,52 +0,0 @@ -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 = \ - coeff-sat.smt2 \ - magnitude-wrong-1020-m.smt2 \ - mult-po.smt2 \ - very-simple-unsat.smt2 \ - subs0-unsat-confirm.smt2 \ - very-easy-sat.smt2 \ - nia-wrong-tl.smt2 \ - real-div-ufnra.smt2 \ - real-as-int.smt2 \ - nta/cos-sig-value.smt2 \ - nta/sin-sym.smt2 \ - nta/tan-rewrite.smt2 \ - nta/exp1-ub.smt2 \ - nta/exp-n0.5-ub.smt2 \ - nta/exp-n0.5-lb.smt2 \ - nta/real-pi.smt2 \ - nta/sqrt-simple.smt2 - -# unsolved : garbage_collect.cvc - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/parser/Makefile b/test/regress/regress0/parser/Makefile deleted file mode 100644 index be157f57a..000000000 --- a/test/regress/regress0/parser/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/parser - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/parser/Makefile.am b/test/regress/regress0/parser/Makefile.am deleted file mode 100644 index c1b80b5ff..000000000 --- a/test/regress/regress0/parser/Makefile.am +++ /dev/null @@ -1,46 +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) @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 = \ - declarefun-emptyset-uf.smt2 \ - constraint.smt2 \ - strings20.smt2 \ - strings25.smt2 \ - as.smt2 - -EXTRA_DIST = $(TESTS) - -#if CVC4_BUILD_PROFILE_COMPETITION -#else -#TESTS += \ -# error.cvc -#endif - -# disabled tests, yet distribute -#EXTRA_DIST += \ -# setofsets-disequal.smt2 - -# synonyms for "check" -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/precedence/Makefile b/test/regress/regress0/precedence/Makefile deleted file mode 100644 index a77d94db1..000000000 --- a/test/regress/regress0/precedence/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/precedence - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am deleted file mode 100644 index 096237106..000000000 --- a/test/regress/regress0/precedence/Makefile.am +++ /dev/null @@ -1,59 +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 = \ - and-xor.cvc \ - and-not.cvc \ - bool-cmp.cvc \ - cmp-plus.cvc \ - eq-fun.cvc \ - iff-assoc.cvc \ - iff-implies.cvc \ - implies-assoc.cvc \ - implies-iff.cvc \ - implies-or.cvc \ - not-and.cvc \ - not-eq.cvc \ - plus-mult.cvc \ - or-implies.cvc \ - or-xor.cvc \ - xor-or.cvc \ - xor-and.cvc \ - xor-assoc.cvc - -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 regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/preprocess/Makefile b/test/regress/regress0/preprocess/Makefile deleted file mode 100644 index c5843db5f..000000000 --- a/test/regress/regress0/preprocess/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/preprocess - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am deleted file mode 100644 index 8ec5e35f6..000000000 --- a/test/regress/regress0/preprocess/Makefile.am +++ /dev/null @@ -1,62 +0,0 @@ -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 +=" - -# Regression tests for SMT inputs -SMT_TESTS = - -# Regression tests for SMT2 inputs -SMT2_TESTS = - -# Regression tests for PL inputs -CVC_TESTS = \ - preprocess_00.cvc \ - preprocess_01.cvc \ - preprocess_02.cvc \ - preprocess_03.cvc \ - preprocess_04.cvc \ - preprocess_05.cvc \ - preprocess_06.cvc \ - preprocess_07.cvc \ - preprocess_08.cvc \ - preprocess_09.cvc \ - preprocess_10.cvc \ - preprocess_11.cvc \ - preprocess_12.cvc \ - preprocess_13.cvc \ - preprocess_14.cvc \ - preprocess_15.cvc - -# Regression tests derived from bug reports -BUG_TESTS = - -TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/push-pop/Makefile b/test/regress/regress0/push-pop/Makefile deleted file mode 100644 index 823a14011..000000000 --- a/test/regress/regress0/push-pop/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/push-pop - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am deleted file mode 100644 index b78c48549..000000000 --- a/test/regress/regress0/push-pop/Makefile.am +++ /dev/null @@ -1,55 +0,0 @@ -SUBDIRS = boolean . - -# 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 +=" - -# Regression tests for SMT inputs -CVC_TESTS = \ - test.00.cvc \ - test.01.cvc \ - units.cvc \ - incremental-subst-bug.cvc - -SMT2_TESTS = \ - tiny_bug.smt2 - -BUG_TESTS = \ - bug233.cvc \ - quant-fun-proc-unfd.smt2 \ - bug654-dd.smt2 \ - inc-double-u.smt2 \ - inc-define.smt2 \ - bug691.smt2 \ - simple_unsat_cores.smt2 \ - bug821.smt2 \ - bug821-check_sat_assuming.smt2 - -TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/push-pop/boolean/Makefile b/test/regress/regress0/push-pop/boolean/Makefile deleted file mode 100644 index 45ab9cda0..000000000 --- a/test/regress/regress0/push-pop/boolean/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../../.. -srcdir = test/regress/regress0/push-pop/boolean - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/push-pop/boolean/Makefile.am b/test/regress/regress0/push-pop/boolean/Makefile.am deleted file mode 100644 index 56a27c527..000000000 --- a/test/regress/regress0/push-pop/boolean/Makefile.am +++ /dev/null @@ -1,63 +0,0 @@ -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 +=" - -# Regression tests for SMT inputs -CVC_TESTS = - -SMT2_TESTS = \ - fuzz_2.smt2 \ - fuzz_3.smt2 \ - fuzz_12.smt2 \ - fuzz_13.smt2 \ - fuzz_14.smt2 \ - fuzz_18.smt2 \ - fuzz_21.smt2 \ - fuzz_22.smt2 \ - fuzz_27.smt2 \ - fuzz_31.smt2 \ - fuzz_33.smt2 \ - fuzz_36.smt2 \ - fuzz_38.smt2 \ - fuzz_46.smt2 \ - fuzz_47.smt2 \ - fuzz_48.smt2 \ - fuzz_49.smt2 \ - fuzz_50.smt2 - -# Disabled because they take too long -# fuzz_1_to_52_merged.smt2 \ -# - -BUG_TESTS = - -TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/quantifiers/Makefile b/test/regress/regress0/quantifiers/Makefile deleted file mode 100644 index b96f2a283..000000000 --- a/test/regress/regress0/quantifiers/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/quantifiers - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am deleted file mode 100644 index 809297863..000000000 --- a/test/regress/regress0/quantifiers/Makefile.am +++ /dev/null @@ -1,97 +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 = \ - bug269.smt2 \ - bug290.smt2 \ - bug291.smt2 \ - bug269.smt2 \ - ex3.smt2 \ - ex6.smt2 \ - ARI176e1.smt2 \ - simp-typ-test.smt2 \ - macros-int-real.smt2 \ - simp-len.smt2 \ - is-even-pred.smt2 \ - delta-simp.smt2 \ - nested-delta.smt2 \ - nested-inf.smt2 \ - clock-3.smt2 \ - cbqi-lia-dt-simp.smt2 \ - is-int.smt2 \ - floor.smt2 \ - mix-simp.smt2 \ - mix-match.smt2 \ - ari056.smt2 \ - matching-lia-1arg.smt2 \ - agg-rew-test.smt2 \ - agg-rew-test-cf.smt2 \ - rew-to-scala.smt2 \ - macros-real-arg.smt2 \ - pure_dt_cbqi.smt2 \ - double-pattern.smt2 \ - qcf-rel-dom-opt.smt2 \ - partial-trigger.smt2 \ - bug749-rounding.smt2 \ - mix-complete-strat.smt2 \ - qbv-simp.smt2 \ - qbv-inequality2.smt2 \ - qbv-test-invert-bvadd-neq.smt2 \ - qbv-test-invert-bvand.smt2 \ - qbv-test-invert-bvand-neq.smt2 \ - qbv-test-invert-bvashr-0-neq.smt2 \ - qbv-test-invert-bvashr-1-neq.smt2 \ - qbv-test-invert-bvlshr-0.smt2 \ - qbv-test-invert-bvlshr-0-neq.smt2 \ - qbv-test-invert-bvlshr-1-neq.smt2 \ - qbv-test-invert-bvor.smt2 \ - qbv-test-invert-bvor-neq.smt2 \ - qbv-test-invert-bvshl-0.smt2 \ - qbv-test-invert-bvult-1.smt2 \ - qbv-test-invert-bvxor.smt2 \ - qbv-test-invert-bvxor-neq.smt2 \ - qbv-test-invert-concat-0.smt2 \ - qbv-test-invert-concat-1.smt2 \ - qbv-test-invert-sign-extend.smt2 \ - clock-10.smt2 \ - lra-triv-gn.smt2 \ - cegqi-nl-simp.cvc \ - cegqi-nl-sq.smt2 - -EXTRA_DIST = $(TESTS) \ - bug291.smt2.expect - -#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 regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/rels/Makefile b/test/regress/regress0/rels/Makefile deleted file mode 100644 index bd7dc8797..000000000 --- a/test/regress/regress0/rels/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/rels - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am deleted file mode 100644 index 9cdfa5b7b..000000000 --- a/test/regress/regress0/rels/Makefile.am +++ /dev/null @@ -1,91 +0,0 @@ -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 = \ - addr_book_0.cvc \ - oneLoc_no_quant-int_0_1.cvc \ - rel_join_3_1.cvc \ - rel_product_0_1.cvc \ - rel_transpose_1_1.cvc \ - rel_conflict_0.cvc \ - rel_join_3.cvc \ - rel_product_0.cvc \ - rel_tc_11.cvc \ - rel_tc_7.cvc \ - rel_tp_join_2.cvc \ - rel_transpose_1.cvc \ - rel_join_0_1.cvc \ - rel_join_4.cvc \ - rel_product_1_1.cvc \ - rel_tc_2_1.cvc \ - rel_tp_join_3.cvc \ - rel_transpose_3.cvc \ - rel_1tup_0.cvc \ - rel_join_0.cvc \ - rel_join_5.cvc \ - rel_product_1.cvc \ - rel_tc_3_1.cvc \ - rel_tp_join_eq_0.cvc \ - rel_transpose_4.cvc \ - rel_complex_0.cvc \ - rel_join_1_1.cvc \ - rel_join_6.cvc \ - rel_symbolic_1_1.cvc \ - rel_tc_3.cvc \ - rel_tp_join_int_0.cvc \ - rel_transpose_5.cvc \ - join-eq-u.cvc \ - rel_complex_1.cvc \ - rel_join_1.cvc \ - rel_join_7.cvc \ - rel_symbolic_1.cvc \ - rel_tp_3_1.cvc \ - rel_tp_join_pro_0.cvc \ - rel_transpose_6.cvc \ - join-eq-u-sat.cvc \ - rel_join_2_1.cvc \ - rel_symbolic_2_1.cvc \ - rel_tp_join_0.cvc \ - rel_tp_join_var_0.cvc \ - rel_transpose_7.cvc \ - rel_join_2.cvc \ - rel_symbolic_3_1.cvc \ - rel_tp_join_1.cvc \ - rel_transpose_0.cvc \ - rel_tc_8.cvc \ - atom_univ2.cvc \ - rels-sharing-simp.cvc \ - iden_0.cvc \ - iden_1.cvc \ - joinImg_0.cvc \ - card_transpose.cvc \ - relations-ops.smt2 - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/rewriterules/Makefile b/test/regress/regress0/rewriterules/Makefile deleted file mode 100644 index 82da93d37..000000000 --- a/test/regress/regress0/rewriterules/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/rewriterules - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am deleted file mode 100644 index 179398c9d..000000000 --- a/test/regress/regress0/rewriterules/Makefile.am +++ /dev/null @@ -1,48 +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 = \ - length_trick.smt2 \ - datatypes.smt2 \ - relation.smt2 \ - simulate_rewriting.smt2 \ - native_arrays.smt2 - -# length_trick2.smt2 reachability_bbttf_eT_arrays.smt2 - -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 regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am deleted file mode 100644 index 9b6c44fa5..000000000 --- a/test/regress/regress0/sep/Makefile.am +++ /dev/null @@ -1,53 +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 = \ - pto-01.smt2 \ - pto-02.smt2 \ - sep-01.smt2 \ - sep-plus1.smt2 \ - nspatial-simp.smt2 \ - sep-simp-unsat-emp.smt2 \ - nemp.smt2 \ - wand-crash.smt2 \ - trees-1.smt2 \ - dup-nemp.smt2 \ - dispose-1.smt2 \ - nil-no-elim.smt2 - - -FAILING_TESTS = -# loop-1220.smt2 (slow) - -EXTRA_DIST = $(TESTS) - -# slow after changes on Nov 20 : artemis-0512-nonterm.smt2 -# slow after decision engine respects requirePhase: type003.smt2 loop007.smt2 - -# and make sure to distribute it -EXTRA_DIST += - -# synonyms for "check" -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/sets/Makefile b/test/regress/regress0/sets/Makefile deleted file mode 100644 index 67ae35206..000000000 --- a/test/regress/regress0/sets/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/sets - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am deleted file mode 100644 index afcae32fe..000000000 --- a/test/regress/regress0/sets/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) @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 = \ - jan24/deepmeas0.hs.fqout.cvc4.47.smt2 \ - jan24/deepmeas0.hs.fqout.small.smt2 \ - jan27/ListConcat.hs.fqout.cvc4.177.smt2 \ - jan27/ListConcat.hs.fqout.177minimized.smt2 \ - jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \ - jan30/UniqueZipper.hs.fqout.minimized10.smt2 \ - jan30/UniqueZipper.hs.fqout.minimized1832.smt2 \ - mar2014/sharing-preregister.smt2 \ - mar2014/small.smt2 \ - mar2014/smaller.smt2 \ - cvc-sample.cvc \ - emptyset.smt2 \ - error1.smt2 \ - error2.smt2 \ - eqtest.smt2 \ - insert.smt2 \ - rec_copy_loop_check_heap_access_43_4.smt2 \ - sets-equal.smt2 \ - sets-inter.smt2 \ - sets-sample.smt2 \ - sets-sharing.smt2 \ - sets-testlemma.smt2 \ - sets-union.smt2 \ - union-1a-flip.smt2 \ - union-1a.smt2 \ - union-1b-flip.smt2 \ - union-1b.smt2 \ - union-2.smt2 \ - dt-simp-mem.smt2 \ - card3-ground.smt2 \ - card-3sets.cvc \ - card.smt2 \ - card-2.smt2 \ - abt-min.smt2 \ - abt-te-exh.smt2 \ - abt-te-exh2.smt2 \ - univset-simp.smt2 \ - complement.cvc \ - complement2.cvc \ - complement3.cvc \ - sharing-simp.smt2 \ - pre-proc-univ.smt2 \ - nonvar-univ.smt2 \ - sets-poly-int-real.smt2 \ - sets-poly-nonint.smt2 \ - int-real-univ.smt2 \ - int-real-univ-unsat.smt2 - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/strings/Makefile b/test/regress/regress0/strings/Makefile deleted file mode 100644 index 1c399b3e4..000000000 --- a/test/regress/regress0/strings/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/strings - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am deleted file mode 100644 index df4e8b84b..000000000 --- a/test/regress/regress0/strings/Makefile.am +++ /dev/null @@ -1,62 +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 = \ - bug001.smt2 \ - bug002.smt2 \ - escchar.smt2 \ - escchar_25.smt2 \ - str003.smt2 \ - str004.smt2 \ - str005.smt2 \ - type001.smt2 \ - model001.smt2 \ - leadingzero001.smt2 \ - loop001.smt2 \ - unsound-0908.smt2 \ - ilc-like.smt2 \ - indexof-sym-simp.smt2 \ - bug613.smt2 \ - norn-simp-rew.smt2 \ - bug612.smt2 \ - idof-rewrites.smt2 \ - norn-31.smt2 \ - strings-native-simple.cvc \ - strings-charat.cvc \ - issue1189.smt2 \ - rewrites-v2.smt2 \ - substr-rewrites.smt2 \ - repl-rewrites2.smt2 \ - idof-sem.smt2 - -FAILING_TESTS = - -EXTRA_DIST = $(TESTS) - -# and make sure to distribute it -EXTRA_DIST += - -# synonyms for "check" -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/sygus/Makefile b/test/regress/regress0/sygus/Makefile deleted file mode 100644 index cc09c6091..000000000 --- a/test/regress/regress0/sygus/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/sygus - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am deleted file mode 100644 index fef4546e9..000000000 --- a/test/regress/regress0/sygus/Makefile.am +++ /dev/null @@ -1,48 +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) @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 = \ - parity-AIG-d0.sy \ - const-var-test.sy \ - no-syntax-test.sy \ - let-ringer.sy \ - let-simp.sy \ - no-syntax-test-bool.sy \ - uminus_one.sy \ - dt-no-syntax.sy \ - strings-unconstrained.sy \ - General_plus10.sy \ - parse-bv-let.sy \ - ccp16.lus.sy \ - real-si-all.sy \ - c100.sy \ - check-generic-red.sy - -# sygus tests currently taking too long for make regress -EXTRA_DIST = $(TESTS) \ - sygus-uf.sl - -# synonyms for "check" -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/tptp/Makefile b/test/regress/regress0/tptp/Makefile deleted file mode 100644 index 8c3909592..000000000 --- a/test/regress/regress0/tptp/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/tptp - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/tptp/Makefile.am b/test/regress/regress0/tptp/Makefile.am deleted file mode 100644 index a6444c3cb..000000000 --- a/test/regress/regress0/tptp/Makefile.am +++ /dev/null @@ -1,85 +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 - -# escape the `=' in file names -equals = = - -# 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 = \ - tptp_parser.p \ - tptp_parser2.p \ - tptp_parser3.p \ - tptp_parser4.p \ - tptp_parser5.p \ - tptp_parser6.p \ - tptp_parser7.p \ - tptp_parser8.p \ - tptp_parser9.p \ - tptp_parser10.p \ - tff0.p \ - tff0-arith.p \ - ARI086$(equals)1.p \ - DAT001$(equals)1.p \ - KRS018+1.p \ - KRS063+1.p \ - MGT019+2.p \ - MGT041-2.p \ - PUZ131_1.p \ - SYN000+1.p \ - SYN000+2.p \ - SYN000-1.p \ - SYN000-2.p \ - SYN000$(equals)2.p \ - SYN000_1.p \ - SYN000_2.p \ - SYN075-1.p - -# axiom files required for the above tests -TEST_DEPS_DIST = \ - Axioms/BOO004-0.ax \ - Axioms/SYN000_0.ax \ - Axioms/SYN000-0.ax \ - Axioms/SYN000+0.ax - -# these take too long at present -EXTRA_DIST = $(TESTS) \ - $(TEST_DEPS_DIST) \ - BOO027-1.p \ - BOO003-4.p \ - MGT031-1.p \ - NLP114-1.p \ - SYN075+1.p - -#if CVC4_BUILD_PROFILE_COMPETITION -#else -#TESTS += \ -# error.cvc -#endif -# -# and make sure to distribute it -#EXTRA_DIST += \ -# error.cvc - -# synonyms for "check" -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/uf/Makefile b/test/regress/regress0/uf/Makefile deleted file mode 100644 index d3d426749..000000000 --- a/test/regress/regress0/uf/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/uf - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am deleted file mode 100644 index 65f96f469..000000000 --- a/test/regress/regress0/uf/Makefile.am +++ /dev/null @@ -1,74 +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 = \ - euf_simp01.smt \ - euf_simp02.smt \ - euf_simp03.smt \ - euf_simp04.smt \ - euf_simp05.smt \ - euf_simp06.smt \ - euf_simp08.smt \ - euf_simp09.smt \ - euf_simp10.smt \ - euf_simp11.smt \ - euf_simp12.smt \ - euf_simp13.smt \ - eq_diamond1.smt \ - eq_diamond14.reduced.smt \ - eq_diamond14.reduced2.smt \ - eq_diamond23.smt \ - NEQ016_size5_reduced2a.smt \ - NEQ016_size5_reduced2b.smt \ - ccredesign-fuzz.smt \ - dead_dnd002.smt \ - iso_brn001.smt \ - simple.01.cvc \ - simple.02.cvc \ - simple.03.cvc \ - simple.04.cvc \ - cnf-iff.smt2 \ - cnf-iff-base.smt2 \ - cnf-ite.smt2 \ - cnf-and-neg.smt2 \ - cnf_abc.smt2 \ - bool-pred-nested.smt2 \ - pred.smt - -EXTRA_DIST = $(TESTS) \ - mkpidgeon - -#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 regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/uflia/Makefile b/test/regress/regress0/uflia/Makefile deleted file mode 100644 index f25747d29..000000000 --- a/test/regress/regress0/uflia/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/uflia - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am deleted file mode 100644 index e40a28608..000000000 --- a/test/regress/regress0/uflia/Makefile.am +++ /dev/null @@ -1,64 +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 +=" - -# Regression tests for SMT inputs -SMT_TESTS = \ - xs-09-16-3-4-1-5.delta01.smt \ - xs-09-16-3-4-1-5.delta02.smt \ - xs-09-16-3-4-1-5.delta03.smt \ - xs-09-16-3-4-1-5.delta04.smt \ - error1.smt \ - error0.delta01.smt \ - error30.smt - -# Regression tests for SMT2 inputs -SMT2_TESTS = \ - check01.smt2 \ - check02.smt2 \ - check03.smt2 \ - check04.smt2 \ - stalmark_e7_27_e7_31.ec.minimized.smt2 \ - tiny.smt2 - -# Regression tests for PL inputs -CVC_TESTS = - -# Regression tests derived from bug reports -BUG_TESTS = - -TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) - -# Necessary to get automake's attention when splitting TESTS into -# SMT_TESTS, SMT2_TESTS, etc.. -EXTRA_DIST = $(TESTS) \ - check02.smt2.expect \ - check03.smt2.expect \ - check04.smt2.expect \ - stalmark_e7_27_e7_31.ec.minimized.smt2.expect \ - tiny.smt2.expect - -# synonyms for "check" in this directory -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/uflra/Makefile b/test/regress/regress0/uflra/Makefile deleted file mode 100644 index 119c530f8..000000000 --- a/test/regress/regress0/uflra/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/uflra - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am deleted file mode 100644 index d8c14b37e..000000000 --- a/test/regress/regress0/uflra/Makefile.am +++ /dev/null @@ -1,62 +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 +=" - -# Regression tests for SMT inputs -SMT_TESTS = \ - constants0.smt \ - simple.01.cvc \ - simple.02.cvc \ - simple.03.cvc \ - simple.04.cvc \ - bug293.cvc \ - bug449.smt \ - pb_real_10_0100_10_10.smt \ - pb_real_10_0100_10_11.smt \ - pb_real_10_0100_10_15.smt \ - pb_real_10_0100_10_16.smt \ - pb_real_10_0100_10_19.smt \ - pb_real_10_0200_10_22.smt \ - pb_real_10_0200_10_26.smt \ - pb_real_10_0200_10_29.smt \ - incorrect1.delta01.smt \ - incorrect1.delta02.smt \ - neq-deltacomp.smt \ - fuzz01.smt - -# Regression tests for PL inputs -CVC_TESTS = - -# Regression tests derived from bug reports -BUG_TESTS = - -TESTS = $(SMT_TESTS) $(CVC_TESTS) $(BUG_TESTS) - -# Necessary to get automake's attention when splitting TESTS into -# SMT_TESTS, SMT2_TESTS, etc.. -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: diff --git a/test/regress/regress0/unconstrained/Makefile b/test/regress/regress0/unconstrained/Makefile deleted file mode 100644 index 594b10e3c..000000000 --- a/test/regress/regress0/unconstrained/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress0/unconstrained - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am deleted file mode 100644 index 7a8577677..000000000 --- a/test/regress/regress0/unconstrained/Makefile.am +++ /dev/null @@ -1,89 +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 +=" -# dejan: disable arith2.smt2, arith7.smt2 it's mixed arithmetic and it doesn't go well when changing theoryof -# lianah: disabled bvdiv.smt2, bvconcat.smt2 as the unconstrained terms are no longer recognized after implementing -# the divide-by-zero semantics for bv division. -TESTS = \ - arith3.smt2 \ - arith4.smt2 \ - arith5.smt2 \ - arith6.smt2 \ - arith.smt2 \ - array1.smt2 \ - bvbool3.smt2 \ - bvbool2.smt2 \ - bvbool.smt2 \ - bvcmp.smt2 \ - bvconcat2.smt2 \ - bvext.smt2 \ - bvite.smt2 \ - bvmul2.smt2 \ - bvmul3.smt2 \ - bvmul.smt2 \ - bvnot.smt2 \ - bvsle2.smt2 \ - bvsle3.smt2 \ - bvsle4.smt2 \ - bvsle5.smt2 \ - bvsle.smt2 \ - bvslt2.smt2 \ - bvslt3.smt2 \ - bvslt4.smt2 \ - bvslt5.smt2 \ - bvslt.smt2 \ - bvule2.smt2 \ - bvule3.smt2 \ - bvule4.smt2 \ - bvule5.smt2 \ - bvule.smt2 \ - bvult2.smt2 \ - bvult3.smt2 \ - bvult4.smt2 \ - bvult5.smt2 \ - bvult.smt2 \ - geq.smt2 \ - gt.smt2 \ - ite.smt2 \ - leq.smt2 \ - lt.smt2 \ - uf1.smt2 \ - xor.smt2 \ - mult1.smt2 - -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 regress0 test -regress regress0 test: check - -# do nothing in this subdir -.PHONY: regress1 regress2 regress3 regress4 -regress1 regress2 regress3 regress4: |