diff options
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: |