diff options
Diffstat (limited to 'test')
111 files changed, 2012 insertions, 4394 deletions
diff --git a/test/Makefile.am b/test/Makefile.am index 65dd601b1..e87427dc6 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -29,65 +29,6 @@ test "X$(AM_COLOR_TESTS)" != Xno \ } subdirs_to_check = \ - regress/regress0 \ - regress/regress0/arith \ - regress/regress0/arith/integers \ - regress/regress0/arrays \ - regress/regress0/aufbv \ - regress/regress0/auflia \ - regress/regress0/bv \ - regress/regress0/bv/core \ - regress/regress0/datatypes \ - regress/regress0/decision \ - regress/regress0/expect \ - regress/regress0/fmf \ - regress/regress0/ho \ - regress/regress0/lemmas \ - regress/regress0/nl \ - regress/regress0/parser \ - regress/regress0/precedence \ - regress/regress0/preprocess \ - regress/regress0/push-pop \ - regress/regress0/push-pop/boolean \ - regress/regress0/quantifiers \ - regress/regress0/rels \ - regress/regress0/rewriterules \ - regress/regress0/sep \ - regress/regress0/sets \ - regress/regress0/strings \ - regress/regress0/sygus \ - regress/regress0/tptp \ - regress/regress0/uf \ - regress/regress0/uflia \ - regress/regress0/uflra \ - regress/regress0/unconstrained \ - regress/regress1 \ - regress/regress1/aufbv \ - regress/regress1/auflia \ - regress/regress1/bv \ - regress/regress1/datatypes \ - regress/regress1/decision \ - regress/regress1/fmf \ - regress/regress1/ho \ - regress/regress1/lemmas \ - regress/regress1/nl \ - regress/regress1/push-pop \ - regress/regress1/rels \ - regress/regress1/rewriterules \ - regress/regress1/sep \ - regress/regress1/sets \ - regress/regress1/strings \ - regress/regress1/sygus \ - regress/regress1/quantifiers \ - regress/regress1/uflia \ - regress/regress2 \ - regress/regress2/arith \ - regress/regress2/nl \ - regress/regress2/quantifiers \ - regress/regress2/strings \ - regress/regress2/sygus \ - regress/regress3 \ - regress/regress4 \ system \ unit @@ -95,6 +36,7 @@ check-recursive: check-pre .PHONY: check-pre check-pre: @rm -f $(subdirs_to_check:=/test-suite.log) + @find regress -name '*.trs' -exec rm {} \; if HAVE_CXXTESTGEN HANDLE_UNIT_TEST_SUMMARY = \ @@ -116,18 +58,7 @@ check-local: if test -s "system/test-suite.log"; then :; else \ echo "$${red}System tests did not run; maybe there were compilation problems ?$$std"; \ fi; \ - for dir in $(subdirs_to_check); do \ - log=$$dir/test-suite.log; \ - if test -s "$$log"; then \ - status="`head -n 5 $$log | tail -1`"; \ - if echo "$$status" | grep -q failed; then \ - echo "$$red$$status"; \ - echo " @abs_builddir@/$$log$$std"; \ - else \ - printf "$$grn%-30s in $$dir$$std\\n" "$$status"; \ - fi; \ - fi; \ - done; \ + echo $${red}Upgrade to a newer version of Automake to get a more detailed summary; \ echo $${blu}=============================== TESTING SUMMARY =============================$$std else # automake 1.12 version @@ -154,5 +85,33 @@ check-local: fi; \ fi; \ done; \ + for dir in `find regress -not -empty -type d`; do \ + status_info=`grep -d skip ":test-result: " $$dir/*`; \ + total=`echo "$$status_info" | grep ":test-result: " | wc -l`; \ + if [ $$total -ne 0 ]; then \ + status="$${std}$$total TOTAL"; \ + pass=`echo "$$status_info" | grep " PASS" | wc -l`; \ + if [ $$pass -ne 0 ]; then \ + status="$$status $${grn}$$pass PASS"; \ + fi; \ + fail=`echo "$$status_info" | grep " FAIL" | wc -l`; \ + if [ $$fail -ne 0 ]; then \ + status="$$status $${red}$$fail FAIL"; \ + fi; \ + xpass=`echo "$$status_info" | grep " XPASS" | wc -l`; \ + if [ $$xpass -ne 0 ]; then \ + status="$$status $${red}$$xpass XPASS"; \ + fi; \ + error=`echo "$$status_info" | grep " ERROR" | wc -l`; \ + if [ $$error -ne 0 ]; then \ + status="$$status $${red}$$error ERROR"; \ + fi; \ + skip=`echo "$$status_info" | grep " SKIP" | wc -l`; \ + if [ $$skip -ne 0 ]; then \ + status="$$status $${blu}$$skip SKIP"; \ + fi; \ + printf "$$grn%-30s in $$dir\\n" "$$status"; \ + fi; \ + done; \ echo $${blu}=============================== TESTING SUMMARY =============================$$std endif diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index 0c2c8a565..cd245f3e6 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -1,29 +1,57 @@ -SUBDIRS = regress0 regress1 -DIST_SUBDIRS = regress0 regress1 regress2 regress3 regress4 +include Makefile.tests + +TESTS = $(REG0_TESTS) $(REG1_TESTS) $(REG2_TESTS) $(REG3_TESTS) $(REG4_TESTS) @mk_include@ @srcdir@/Makefile.levels +# don't override a BINARY imported from a personal.mk +@mk_if@eq ($(BINARY),) +@mk_empty@BINARY = cvc4 +end@mk_if@ + +LOG_COMPILER = $(top_srcdir)/test/regress/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 export VERBOSE = 1 - .PHONY: regress0 regress1 regress2 regress3 regress4 -regress1: regress0 -regress2: regress0 regress1 -regress3: regress0 regress1 regress2 -regress4: regress0 regress1 regress2 regress3 -regress0 regress1 regress2 regress3 regress4: - -cd $@ && $(MAKE) check -# synonyms for "check" in this directory -.PHONY: regress test -regress test: check +regress0: + REGRESSION_LEVEL=0 $(MAKE) check + +regress1: + REGRESSION_LEVEL=1 $(MAKE) check + +regress2: + REGRESSION_LEVEL=2 $(MAKE) check + +regress3: + REGRESSION_LEVEL=3 $(MAKE) check -# no-ops here -.PHONY: units systemtests -units systemtests: +regress4: + REGRESSION_LEVEL=4 $(MAKE) check EXTRA_DIST = \ + $(REG0_TESTS) \ + $(REG1_TESTS) \ + $(REG2_TESTS) \ + $(REG3_TESTS) \ + $(REG4_TESTS) \ + $(TESTS_EXPECT) \ + regress0/uf/mkpidgeon \ + regress0/tptp/Axioms/BOO004-0.ax \ + regress0/tptp/Axioms/SYN000+0.ax \ + regress0/tptp/Axioms/SYN000-0.ax \ + regress0/tptp/Axioms/SYN000_0.ax \ Makefile.levels \ + Makefile.tests \ run_regression \ README diff --git a/test/regress/Makefile.levels b/test/regress/Makefile.levels index 30bf4ca09..9e4d3fa20 100644 --- a/test/regress/Makefile.levels +++ b/test/regress/Makefile.levels @@ -1,17 +1,18 @@ # This Makefile fragment allows one to use "make check" but also specify # a regression level. + +# Regression level 1 is the default +TESTS = $(REG0_TESTS) $(REG1_TESTS) + ifeq ($(REGRESSION_LEVEL),0) -SUBDIRS = regress0 -endif -ifeq ($(REGRESSION_LEVEL),1) -SUBDIRS += regress1 +TESTS = $(REG0_TESTS) endif ifeq ($(REGRESSION_LEVEL),2) -SUBDIRS += regress1 regress2 +TESTS = $(REG0_TESTS) $(REG1_TESTS) $(REG2_TESTS) endif ifeq ($(REGRESSION_LEVEL),3) -SUBDIRS += regress1 regress2 regress3 +TESTS = $(REG0_TESTS) $(REG1_TESTS) $(REG2_TESTS) $(REG3_TESTS) endif ifeq ($(REGRESSION_LEVEL),4) -SUBDIRS += regress1 regress2 regress3 regress4 +TESTS = $(REG0_TESTS) $(REG1_TESTS) $(REG2_TESTS) $(REG3_TESTS) $(REG4_TESTS) endif diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests new file mode 100644 index 000000000..80e99a8cf --- /dev/null +++ b/test/regress/Makefile.tests @@ -0,0 +1,1931 @@ +# escape the `=' in file names +equals = = + +REG0_TESTS = \ + regress0/arith/arith.01.cvc \ + regress0/arith/arith.02.cvc \ + regress0/arith/arith.03.cvc \ + regress0/arith/bug443.delta01.smt \ + regress0/arith/bug547.2.smt2 \ + regress0/arith/bug569.smt2 \ + regress0/arith/delta-minimized-row-vector-bug.smt \ + regress0/arith/div.01.smt2 \ + regress0/arith/div.02.smt2 \ + regress0/arith/div.04.smt2 \ + regress0/arith/div.05.smt2 \ + regress0/arith/div.07.smt2 \ + regress0/arith/fuzz_3-eq.smt \ + regress0/arith/integers/arith-int-042.cvc \ + regress0/arith/integers/arith-int-042.min.cvc \ + regress0/arith/leq.01.smt \ + regress0/arith/miplib.cvc \ + regress0/arith/miplib2.cvc \ + regress0/arith/miplib4.cvc \ + regress0/arith/miplibtrick.smt \ + regress0/arith/mod-simp.smt2 \ + regress0/arith/mod.01.smt2 \ + regress0/arith/mult.01.smt2 \ + regress0/arrayinuf_declare.smt2 \ + regress0/arrays/arrays0.smt2 \ + regress0/arrays/arrays1.smt2 \ + regress0/arrays/arrays2.smt2 \ + regress0/arrays/arrays3.smt2 \ + regress0/arrays/arrays4.smt2 \ + regress0/arrays/bool-array.smt2 \ + regress0/arrays/bug272.minimized.smt \ + regress0/arrays/bug272.smt \ + regress0/arrays/bug637.delta.smt2 \ + regress0/arrays/constarr.cvc \ + regress0/arrays/constarr.smt2 \ + regress0/arrays/constarr2.cvc \ + regress0/arrays/constarr2.smt2 \ + regress0/arrays/incorrect1.smt \ + regress0/arrays/incorrect10.smt \ + regress0/arrays/incorrect11.smt \ + regress0/arrays/incorrect2.minimized.smt \ + regress0/arrays/incorrect2.smt \ + regress0/arrays/incorrect3.smt \ + regress0/arrays/incorrect4.smt \ + regress0/arrays/incorrect5.smt \ + regress0/arrays/incorrect6.smt \ + regress0/arrays/incorrect7.smt \ + regress0/arrays/incorrect8.minimized.smt \ + regress0/arrays/incorrect8.smt \ + regress0/arrays/incorrect9.smt \ + regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt \ + regress0/arrays/x2.smt \ + regress0/arrays/x3.smt \ + regress0/aufbv/array_rewrite_bug.smt \ + regress0/aufbv/bug00.smt \ + regress0/aufbv/bug338.smt2 \ + regress0/aufbv/bug347.smt \ + regress0/aufbv/bug451.smt \ + regress0/aufbv/bug509.smt \ + regress0/aufbv/bug580.delta.smt2 \ + regress0/aufbv/diseqprop.01.smt \ + regress0/aufbv/dubreva005ue.delta01.smt \ + regress0/aufbv/fifo32bc06k08.delta01.smt \ + regress0/aufbv/fuzz00.smt \ + regress0/aufbv/fuzz01.delta01.smt \ + regress0/aufbv/fuzz01.smt \ + regress0/aufbv/fuzz02.delta01.smt \ + regress0/aufbv/fuzz02.smt \ + regress0/aufbv/fuzz03.delta01.smt \ + regress0/aufbv/fuzz03.smt \ + regress0/aufbv/fuzz04.delta01.smt \ + regress0/aufbv/fuzz04.smt \ + regress0/aufbv/fuzz05.delta01.smt \ + regress0/aufbv/fuzz05.smt \ + regress0/aufbv/fuzz06.delta01.smt \ + regress0/aufbv/fuzz06.smt \ + regress0/aufbv/fuzz07.smt \ + regress0/aufbv/fuzz08.smt \ + regress0/aufbv/fuzz09.smt \ + regress0/aufbv/fuzz11.smt \ + regress0/aufbv/fuzz12.smt \ + regress0/aufbv/fuzz13.smt \ + regress0/aufbv/fuzz14.smt \ + regress0/aufbv/fuzz15.smt \ + regress0/aufbv/rewrite_bug.smt \ + regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smt \ + regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \ + regress0/aufbv/wchains010ue.delta01.smt \ + regress0/aufbv/wchains010ue.delta02.smt \ + regress0/auflia/a17.smt \ + regress0/auflia/bug336.smt2 \ + regress0/auflia/error72.delta2.smt \ + regress0/auflia/fuzz-error1099.smt \ + regress0/auflia/fuzz-error232.smt \ + regress0/auflia/fuzz01.delta01.smt \ + regress0/auflia/fuzz02.smt \ + regress0/auflia/fuzz03.smt \ + regress0/auflia/fuzz04.smt \ + regress0/auflia/fuzz05.smt \ + regress0/auflia/x2.smt \ + regress0/boolean-prec.cvc \ + regress0/boolean-terms-bug-array.smt2 \ + regress0/boolean-terms-kernel1.smt2 \ + regress0/boolean-terms.cvc \ + regress0/bt-test-00.smt2 \ + regress0/bt-test-01.smt2 \ + regress0/bug1247.smt2 \ + regress0/bug161.smt \ + regress0/bug164.smt \ + regress0/bug167.smt \ + regress0/bug168.smt \ + regress0/bug187.smt2 \ + regress0/bug217.smt2 \ + regress0/bug220.smt2 \ + regress0/bug239.smt \ + regress0/bug274.cvc \ + regress0/bug288.smt \ + regress0/bug288b.smt \ + regress0/bug288c.smt \ + regress0/bug303.smt2 \ + regress0/bug310.cvc \ + regress0/bug32.cvc \ + regress0/bug322.cvc \ + regress0/bug322b.cvc \ + regress0/bug339.smt2 \ + regress0/bug365.smt2 \ + regress0/bug382.smt2 \ + regress0/bug383.smt2 \ + regress0/bug398.smt2 \ + regress0/bug421.smt2 \ + regress0/bug421b.smt2 \ + regress0/bug480.smt2 \ + regress0/bug484.smt2 \ + regress0/bug486.cvc \ + regress0/bug49.smt \ + regress0/bug512.minimized.smt2 \ + regress0/bug521.minimized.smt2 \ + regress0/bug522.smt2 \ + regress0/bug528a.smt2 \ + regress0/bug541.smt2 \ + regress0/bug544.smt2 \ + regress0/bug548a.smt2 \ + regress0/bug576.smt2 \ + regress0/bug576a.smt2 \ + regress0/bug578.smt2 \ + regress0/bug586.cvc \ + regress0/bug595.cvc \ + regress0/bug596.cvc \ + regress0/bug596b.cvc \ + regress0/bug605.cvc \ + regress0/bug639.smt2 \ + regress0/buggy-ite.smt2 \ + regress0/bv/bug260a.smt \ + regress0/bv/bug260b.smt \ + regress0/bv/bug440.smt \ + regress0/bv/bug733.smt2 \ + regress0/bv/bug734.smt2 \ + regress0/bv/bv-int-collapse1.smt2 \ + regress0/bv/bv-int-collapse2.smt2 \ + regress0/bv/bv2nat-ground-c.smt2 \ + regress0/bv/bv2nat-simp-range.smt2 \ + regress0/bv/bvmul-pow2-only.smt2 \ + regress0/bv/bvsimple.cvc \ + regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt \ + regress0/bv/core/a78test0002.smt \ + regress0/bv/core/a95test0002.smt \ + regress0/bv/core/bitvec0.smt \ + regress0/bv/core/bitvec2.smt \ + regress0/bv/core/bitvec5.smt \ + regress0/bv/core/bitvec7.smt \ + regress0/bv/core/bv_eq_diamond10.smt \ + regress0/bv/core/concat-merge-0.smt \ + regress0/bv/core/concat-merge-1.smt \ + regress0/bv/core/concat-merge-2.smt \ + regress0/bv/core/concat-merge-3.smt \ + regress0/bv/core/equality-00.smt \ + regress0/bv/core/equality-01.smt \ + regress0/bv/core/equality-02.smt \ + regress0/bv/core/equality-05.smt \ + regress0/bv/core/extract-concat-0.smt \ + regress0/bv/core/extract-concat-1.smt \ + regress0/bv/core/extract-concat-10.smt \ + regress0/bv/core/extract-concat-11.smt \ + regress0/bv/core/extract-concat-2.smt \ + regress0/bv/core/extract-concat-3.smt \ + regress0/bv/core/extract-concat-4.smt \ + regress0/bv/core/extract-concat-5.smt \ + regress0/bv/core/extract-concat-6.smt \ + regress0/bv/core/extract-concat-7.smt \ + regress0/bv/core/extract-concat-8.smt \ + regress0/bv/core/extract-concat-9.smt \ + regress0/bv/core/extract-constant.smt \ + regress0/bv/core/extract-extract-0.smt \ + regress0/bv/core/extract-extract-1.smt \ + regress0/bv/core/extract-extract-10.smt \ + regress0/bv/core/extract-extract-11.smt \ + regress0/bv/core/extract-extract-2.smt \ + regress0/bv/core/extract-extract-3.smt \ + regress0/bv/core/extract-extract-4.smt \ + regress0/bv/core/extract-extract-5.smt \ + regress0/bv/core/extract-extract-6.smt \ + regress0/bv/core/extract-extract-7.smt \ + regress0/bv/core/extract-extract-8.smt \ + regress0/bv/core/extract-extract-9.smt \ + regress0/bv/core/extract-whole-0.smt \ + regress0/bv/core/extract-whole-1.smt \ + regress0/bv/core/extract-whole-2.smt \ + regress0/bv/core/extract-whole-3.smt \ + regress0/bv/core/extract-whole-4.smt \ + regress0/bv/core/slice-01.smt \ + regress0/bv/core/slice-02.smt \ + regress0/bv/core/slice-03.smt \ + regress0/bv/core/slice-04.smt \ + regress0/bv/core/slice-05.smt \ + regress0/bv/core/slice-06.smt \ + regress0/bv/core/slice-07.smt \ + regress0/bv/core/slice-08.smt \ + regress0/bv/core/slice-09.smt \ + regress0/bv/core/slice-10.smt \ + regress0/bv/core/slice-11.smt \ + regress0/bv/core/slice-12.smt \ + regress0/bv/core/slice-13.smt \ + regress0/bv/core/slice-14.smt \ + regress0/bv/core/slice-15.smt \ + regress0/bv/core/slice-16.smt \ + regress0/bv/core/slice-17.smt \ + regress0/bv/core/slice-18.smt \ + regress0/bv/core/slice-19.smt \ + regress0/bv/core/slice-20.smt \ + regress0/bv/divtest_2_5.smt2 \ + regress0/bv/divtest_2_6.smt2 \ + regress0/bv/fuzz01.smt \ + regress0/bv/fuzz02.delta01.smt \ + regress0/bv/fuzz02.smt \ + regress0/bv/fuzz03.smt \ + regress0/bv/fuzz04.smt \ + regress0/bv/fuzz05.smt \ + regress0/bv/fuzz06.smt \ + regress0/bv/fuzz07.smt \ + regress0/bv/fuzz08.smt \ + regress0/bv/fuzz09.smt \ + regress0/bv/fuzz10.smt \ + regress0/bv/fuzz11.smt \ + regress0/bv/fuzz12.smt \ + regress0/bv/fuzz13.smt \ + regress0/bv/fuzz14.smt \ + regress0/bv/fuzz16.delta01.smt \ + regress0/bv/fuzz17.delta01.smt \ + regress0/bv/fuzz18.delta01.smt \ + regress0/bv/fuzz18.delta02.smt \ + regress0/bv/fuzz18.delta03.smt \ + regress0/bv/fuzz18.smt \ + regress0/bv/fuzz19.delta01.smt \ + regress0/bv/fuzz19.smt \ + regress0/bv/fuzz20.delta01.smt \ + regress0/bv/fuzz20.smt \ + regress0/bv/fuzz21.delta01.smt \ + regress0/bv/fuzz21.smt \ + regress0/bv/fuzz22.delta01.smt \ + regress0/bv/fuzz22.smt \ + regress0/bv/fuzz23.delta01.smt \ + regress0/bv/fuzz23.smt \ + regress0/bv/fuzz24.delta01.smt \ + regress0/bv/fuzz24.smt \ + regress0/bv/fuzz25.delta01.smt \ + regress0/bv/fuzz25.smt \ + regress0/bv/fuzz26.delta01.smt \ + regress0/bv/fuzz26.smt \ + regress0/bv/fuzz27.delta01.smt \ + regress0/bv/fuzz27.smt \ + regress0/bv/fuzz28.delta01.smt \ + regress0/bv/fuzz28.smt \ + regress0/bv/fuzz29.delta01.smt \ + regress0/bv/fuzz29.smt \ + regress0/bv/fuzz30.delta01.smt \ + regress0/bv/fuzz30.smt \ + regress0/bv/fuzz31.delta01.smt \ + regress0/bv/fuzz31.smt \ + regress0/bv/fuzz32.delta01.smt \ + regress0/bv/fuzz32.smt \ + regress0/bv/fuzz33.delta01.smt \ + regress0/bv/fuzz33.smt \ + regress0/bv/fuzz34.delta01.smt \ + regress0/bv/fuzz35.delta01.smt \ + regress0/bv/fuzz35.smt \ + regress0/bv/fuzz36.delta01.smt \ + regress0/bv/fuzz36.smt \ + regress0/bv/fuzz37.delta01.smt \ + regress0/bv/fuzz37.smt \ + regress0/bv/fuzz38.delta01.smt \ + regress0/bv/fuzz39.delta01.smt \ + regress0/bv/fuzz39.smt \ + regress0/bv/fuzz40.delta01.smt \ + regress0/bv/fuzz40.smt \ + regress0/bv/fuzz41.smt \ + regress0/bv/mul-neg-unsat.smt2 \ + regress0/bv/mul-negpow2.smt2 \ + regress0/bv/mult-pow2-negative.smt2 \ + regress0/bv/sizecheck.cvc \ + regress0/bv/smtcompbug.smt \ + regress0/bv/unsound1-reduced.smt2 \ + regress0/chained-equality.smt2 \ + regress0/constant-rewrite.smt \ + regress0/cvc3.userdoc.01.cvc \ + regress0/cvc3.userdoc.02.cvc \ + regress0/cvc3.userdoc.03.cvc \ + regress0/cvc3.userdoc.04.cvc \ + regress0/cvc3.userdoc.05.cvc \ + regress0/cvc3.userdoc.06.cvc \ + regress0/datatypes/Test1-tup-mp.cvc \ + regress0/datatypes/boolean-equality.cvc \ + regress0/datatypes/boolean-terms-datatype.cvc \ + regress0/datatypes/boolean-terms-parametric-datatype-1.cvc \ + regress0/datatypes/boolean-terms-parametric-datatype-2.cvc \ + regress0/datatypes/boolean-terms-record.cvc \ + regress0/datatypes/boolean-terms-rewrite.cvc \ + regress0/datatypes/boolean-terms-tuple.cvc \ + regress0/datatypes/bug286.cvc \ + regress0/datatypes/bug438.cvc \ + regress0/datatypes/bug438b.cvc \ + regress0/datatypes/bug597-rbt.smt2 \ + regress0/datatypes/bug604.smt2 \ + regress0/datatypes/bug625.smt2 \ + regress0/datatypes/cdt-model-cade15.smt2 \ + regress0/datatypes/cdt-non-canon-stream.smt2 \ + regress0/datatypes/coda_simp_model.smt2 \ + regress0/datatypes/conqueue-dt-enum-iloop.smt2 \ + regress0/datatypes/datatype-dump.cvc \ + regress0/datatypes/datatype.cvc \ + regress0/datatypes/datatype0.cvc \ + regress0/datatypes/datatype1.cvc \ + regress0/datatypes/datatype13.cvc \ + regress0/datatypes/datatype2.cvc \ + regress0/datatypes/datatype3.cvc \ + regress0/datatypes/datatype4.cvc \ + regress0/datatypes/dt-2.6.smt2 \ + regress0/datatypes/dt-match-pat-param-2.6.smt2 \ + regress0/datatypes/dt-param-2.6.smt2 \ + regress0/datatypes/dt-param-card4-bool-sat.smt2 \ + regress0/datatypes/dt-sel-2.6.smt2 \ + regress0/datatypes/empty_tuprec.cvc \ + regress0/datatypes/example-dailler-min.smt2 \ + regress0/datatypes/is_test.smt2 \ + regress0/datatypes/issue1433.smt2 \ + regress0/datatypes/jsat-2.6.smt2 \ + regress0/datatypes/model-subterms-min.smt2 \ + regress0/datatypes/mutually-recursive.cvc \ + regress0/datatypes/pair-bool-bool.cvc \ + regress0/datatypes/pair-real-bool.smt2 \ + regress0/datatypes/rec1.cvc \ + regress0/datatypes/rec2.cvc \ + regress0/datatypes/rec4.cvc \ + regress0/datatypes/rewriter.cvc \ + regress0/datatypes/sc-cdt1.smt2 \ + regress0/datatypes/some-boolean-tests.cvc \ + regress0/datatypes/stream-singleton.smt2 \ + regress0/datatypes/tenum-bug.smt2 \ + regress0/datatypes/tuple-model.cvc \ + regress0/datatypes/tuple-no-clash.cvc \ + regress0/datatypes/tuple-record-bug.cvc \ + regress0/datatypes/tuple.cvc \ + regress0/datatypes/tuples-empty.smt2 \ + regress0/datatypes/tuples-multitype.smt2 \ + regress0/datatypes/typed_v10l30054.cvc \ + regress0/datatypes/typed_v1l80005.cvc \ + regress0/datatypes/typed_v2l30079.cvc \ + regress0/datatypes/typed_v3l20092.cvc \ + regress0/datatypes/typed_v5l30069.cvc \ + regress0/datatypes/v10l40099.cvc \ + regress0/datatypes/v2l40025.cvc \ + regress0/datatypes/v3l60006.cvc \ + regress0/datatypes/v5l30058.cvc \ + regress0/datatypes/wrong-sel-simp.cvc \ + regress0/decision/aufbv-fuzz01.smt \ + regress0/decision/bitvec0.delta01.smt \ + regress0/decision/bitvec0.smt \ + regress0/decision/bitvec5.smt \ + regress0/decision/bug347.smt \ + regress0/decision/bug374a.smt \ + regress0/decision/bug374b.smt2 \ + regress0/decision/error122.delta01.smt \ + regress0/decision/error122.smt \ + regress0/decision/error20.delta01.smt \ + regress0/decision/error20.smt \ + regress0/decision/error3.delta01.smt \ + regress0/decision/pp-regfile.delta01.smt \ + regress0/decision/pp-regfile.delta02.smt \ + regress0/decision/quant-ex1.smt2 \ + regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt \ + regress0/decision/wchains010ue.delta02.smt \ + regress0/declare-fun-is-match.smt2 \ + regress0/declare-funs.smt2 \ + regress0/distinct.smt \ + regress0/expect/scrub.01.smt \ + regress0/expect/scrub.02.smt \ + regress0/expect/scrub.03.smt2 \ + regress0/expect/scrub.04.smt2 \ + regress0/expect/scrub.06.cvc \ + regress0/expect/scrub.07.sy \ + regress0/expect/scrub.08.sy \ + regress0/expect/scrub.09.p \ + regress0/flet.smt \ + regress0/flet2.smt \ + regress0/fmf/Arrow_Order-smtlib.778341.smt \ + regress0/fmf/Hoare-z3.931718.smt \ + regress0/fmf/QEpres-uf.855035.smt \ + regress0/fmf/array_card.smt2 \ + regress0/fmf/bounded_sets.smt2 \ + regress0/fmf/bug-041417-set-options.cvc \ + regress0/fmf/bug652.smt2 \ + regress0/fmf/bug782.smt2 \ + regress0/fmf/cruanes-no-minimal-unk.smt2 \ + regress0/fmf/fc-simple.smt2 \ + regress0/fmf/fc-unsat-pent.smt2 \ + regress0/fmf/fc-unsat-tot-2.smt2 \ + regress0/fmf/fd-false.smt2 \ + regress0/fmf/fmc_unsound_model.smt2 \ + regress0/fmf/fmf-strange-bounds-2.smt2 \ + regress0/fmf/forall_unit_data2.smt2 \ + regress0/fmf/krs-sat.smt2 \ + regress0/fmf/no-minimal-sat.smt2 \ + regress0/fmf/quant_real_univ.cvc \ + regress0/fmf/sat-logic.smt2 \ + regress0/fmf/sc_bad_model_1221.smt2 \ + regress0/fmf/syn002-si-real-int.smt2 \ + regress0/fmf/tail_rec.smt2 \ + regress0/fuzz_1.smt \ + regress0/fuzz_3.smt \ + regress0/get-value-incremental.smt2 \ + regress0/get-value-ints.smt2 \ + regress0/get-value-reals-ints.smt2 \ + regress0/get-value-reals.smt2 \ + regress0/ho/apply-collapse-sat.smt2 \ + regress0/ho/apply-collapse-unsat.smt2 \ + regress0/ho/cong-full-apply.smt2 \ + regress0/ho/cong.smt2 \ + regress0/ho/declare-fun-variants.smt2 \ + regress0/ho/def-fun-flatten.smt2 \ + regress0/ho/ext-finite-unsat.smt2 \ + regress0/ho/ext-ho-nested-lambda-model.smt2 \ + regress0/ho/ext-ho.smt2 \ + regress0/ho/ext-sat-partial-eval.smt2 \ + regress0/ho/ext-sat.smt2 \ + regress0/ho/ho-matching-enum.smt2 \ + regress0/ho/ho-matching-nested-app.smt2 \ + regress0/ho/ite-apply-eq.smt2 \ + regress0/ho/lambda-equality-non-canon.smt2 \ + regress0/ho/modulo-func-equality.smt2 \ + regress0/ho/simple-matching-partial.smt2 \ + regress0/ho/simple-matching.smt2 \ + regress0/ho/trans.smt2 \ + regress0/hung10_itesdk_output1.smt2 \ + regress0/hung10_itesdk_output2.smt2 \ + regress0/hung13sdk_output1.smt2 \ + regress0/hung13sdk_output2.smt2 \ + regress0/ineq_basic.smt \ + regress0/ineq_slack.smt \ + regress0/issue1063-overloading-dt-cons.smt2 \ + regress0/issue1063-overloading-dt-fun.smt2 \ + regress0/issue1063-overloading-dt-sel.smt2 \ + regress0/ite.cvc \ + regress0/ite2.smt2 \ + regress0/ite3.smt2 \ + regress0/ite4.smt2 \ + regress0/ite_real_int_type.smt \ + regress0/ite_real_valid.smt \ + regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smt \ + regress0/lemmas/fs_not_sc_seen.induction.smt \ + regress0/lemmas/mode_cntrl.induction.smt \ + regress0/lemmas/sc_init_frame_gap.induction.smt \ + regress0/let.cvc \ + regress0/let.smt \ + regress0/let2.smt \ + regress0/logops.01.cvc \ + regress0/logops.02.cvc \ + regress0/logops.03.cvc \ + regress0/logops.04.cvc \ + regress0/logops.05.cvc \ + regress0/nl/coeff-sat.smt2 \ + regress0/nl/magnitude-wrong-1020-m.smt2 \ + regress0/nl/mult-po.smt2 \ + regress0/nl/nia-wrong-tl.smt2 \ + regress0/nl/nta/cos-sig-value.smt2 \ + regress0/nl/nta/exp-n0.5-lb.smt2 \ + regress0/nl/nta/exp-n0.5-ub.smt2 \ + regress0/nl/nta/exp1-ub.smt2 \ + regress0/nl/nta/real-pi.smt2 \ + regress0/nl/nta/sin-sym.smt2 \ + regress0/nl/nta/sqrt-simple.smt2 \ + regress0/nl/nta/tan-rewrite.smt2 \ + regress0/nl/real-as-int.smt2 \ + regress0/nl/real-div-ufnra.smt2 \ + regress0/nl/subs0-unsat-confirm.smt2 \ + regress0/nl/very-easy-sat.smt2 \ + regress0/nl/very-simple-unsat.smt2 \ + regress0/parallel-let.smt2 \ + regress0/parser/as.smt2 \ + regress0/parser/constraint.smt2 \ + regress0/parser/declarefun-emptyset-uf.smt2 \ + regress0/parser/strings20.smt2 \ + regress0/parser/strings25.smt2 \ + regress0/precedence/and-not.cvc \ + regress0/precedence/and-xor.cvc \ + regress0/precedence/bool-cmp.cvc \ + regress0/precedence/cmp-plus.cvc \ + regress0/precedence/eq-fun.cvc \ + regress0/precedence/iff-assoc.cvc \ + regress0/precedence/iff-implies.cvc \ + regress0/precedence/implies-assoc.cvc \ + regress0/precedence/implies-iff.cvc \ + regress0/precedence/implies-or.cvc \ + regress0/precedence/not-and.cvc \ + regress0/precedence/not-eq.cvc \ + regress0/precedence/or-implies.cvc \ + regress0/precedence/or-xor.cvc \ + regress0/precedence/plus-mult.cvc \ + regress0/precedence/xor-and.cvc \ + regress0/precedence/xor-assoc.cvc \ + regress0/precedence/xor-or.cvc \ + regress0/preprocess/preprocess_00.cvc \ + regress0/preprocess/preprocess_01.cvc \ + regress0/preprocess/preprocess_02.cvc \ + regress0/preprocess/preprocess_03.cvc \ + regress0/preprocess/preprocess_04.cvc \ + regress0/preprocess/preprocess_05.cvc \ + regress0/preprocess/preprocess_06.cvc \ + regress0/preprocess/preprocess_07.cvc \ + regress0/preprocess/preprocess_08.cvc \ + regress0/preprocess/preprocess_09.cvc \ + regress0/preprocess/preprocess_10.cvc \ + regress0/preprocess/preprocess_11.cvc \ + regress0/preprocess/preprocess_12.cvc \ + regress0/preprocess/preprocess_13.cvc \ + regress0/preprocess/preprocess_14.cvc \ + regress0/preprocess/preprocess_15.cvc \ + regress0/print_lambda.cvc \ + regress0/push-pop/boolean/fuzz_12.smt2 \ + regress0/push-pop/boolean/fuzz_13.smt2 \ + regress0/push-pop/boolean/fuzz_14.smt2 \ + regress0/push-pop/boolean/fuzz_18.smt2 \ + regress0/push-pop/boolean/fuzz_2.smt2 \ + regress0/push-pop/boolean/fuzz_21.smt2 \ + regress0/push-pop/boolean/fuzz_22.smt2 \ + regress0/push-pop/boolean/fuzz_27.smt2 \ + regress0/push-pop/boolean/fuzz_3.smt2 \ + regress0/push-pop/boolean/fuzz_31.smt2 \ + regress0/push-pop/boolean/fuzz_33.smt2 \ + regress0/push-pop/boolean/fuzz_36.smt2 \ + regress0/push-pop/boolean/fuzz_38.smt2 \ + regress0/push-pop/boolean/fuzz_46.smt2 \ + regress0/push-pop/boolean/fuzz_47.smt2 \ + regress0/push-pop/boolean/fuzz_48.smt2 \ + regress0/push-pop/boolean/fuzz_49.smt2 \ + regress0/push-pop/boolean/fuzz_50.smt2 \ + regress0/push-pop/bug233.cvc \ + regress0/push-pop/bug654-dd.smt2 \ + regress0/push-pop/bug691.smt2 \ + regress0/push-pop/bug821-check_sat_assuming.smt2 \ + regress0/push-pop/bug821.smt2 \ + regress0/push-pop/inc-define.smt2 \ + regress0/push-pop/inc-double-u.smt2 \ + regress0/push-pop/incremental-subst-bug.cvc \ + regress0/push-pop/quant-fun-proc-unfd.smt2 \ + regress0/push-pop/simple_unsat_cores.smt2 \ + regress0/push-pop/test.00.cvc \ + regress0/push-pop/test.01.cvc \ + regress0/push-pop/tiny_bug.smt2 \ + regress0/push-pop/units.cvc \ + regress0/quantifiers/ARI176e1.smt2 \ + regress0/quantifiers/agg-rew-test-cf.smt2 \ + regress0/quantifiers/agg-rew-test.smt2 \ + regress0/quantifiers/ari056.smt2 \ + regress0/quantifiers/bug269.smt2 \ + regress0/quantifiers/bug290.smt2 \ + regress0/quantifiers/bug291.smt2 \ + regress0/quantifiers/bug749-rounding.smt2 \ + regress0/quantifiers/cbqi-lia-dt-simp.smt2 \ + regress0/quantifiers/cegqi-nl-simp.cvc \ + regress0/quantifiers/cegqi-nl-sq.smt2 \ + regress0/quantifiers/clock-10.smt2 \ + regress0/quantifiers/clock-3.smt2 \ + regress0/quantifiers/delta-simp.smt2 \ + regress0/quantifiers/double-pattern.smt2 \ + regress0/quantifiers/ex3.smt2 \ + regress0/quantifiers/ex6.smt2 \ + regress0/quantifiers/floor.smt2 \ + regress0/quantifiers/is-even-pred.smt2 \ + regress0/quantifiers/is-int.smt2 \ + regress0/quantifiers/lra-triv-gn.smt2 \ + regress0/quantifiers/macros-int-real.smt2 \ + regress0/quantifiers/macros-real-arg.smt2 \ + regress0/quantifiers/matching-lia-1arg.smt2 \ + regress0/quantifiers/mix-complete-strat.smt2 \ + regress0/quantifiers/mix-match.smt2 \ + regress0/quantifiers/mix-simp.smt2 \ + regress0/quantifiers/nested-delta.smt2 \ + regress0/quantifiers/nested-inf.smt2 \ + regress0/quantifiers/partial-trigger.smt2 \ + regress0/quantifiers/pure_dt_cbqi.smt2 \ + regress0/quantifiers/qbv-inequality2.smt2 \ + regress0/quantifiers/qbv-simp.smt2 \ + regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 \ + regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 \ + regress0/quantifiers/qbv-test-invert-bvand.smt2 \ + regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 \ + regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 \ + regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 \ + regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 \ + regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 \ + regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 \ + regress0/quantifiers/qbv-test-invert-bvor.smt2 \ + regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 \ + regress0/quantifiers/qbv-test-invert-bvult-1.smt2 \ + regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 \ + regress0/quantifiers/qbv-test-invert-bvxor.smt2 \ + regress0/quantifiers/qbv-test-invert-concat-0.smt2 \ + regress0/quantifiers/qbv-test-invert-concat-1.smt2 \ + regress0/quantifiers/qbv-test-invert-sign-extend.smt2 \ + regress0/quantifiers/qcf-rel-dom-opt.smt2 \ + regress0/quantifiers/rew-to-scala.smt2 \ + regress0/quantifiers/simp-len.smt2 \ + regress0/quantifiers/simp-typ-test.smt2 \ + regress0/queries0.cvc \ + regress0/rec-fun-const-parse-bug.smt2 \ + regress0/rels/addr_book_0.cvc \ + regress0/rels/atom_univ2.cvc \ + regress0/rels/card_transpose.cvc \ + regress0/rels/iden_0.cvc \ + regress0/rels/iden_1.cvc \ + regress0/rels/join-eq-u-sat.cvc \ + regress0/rels/join-eq-u.cvc \ + regress0/rels/joinImg_0.cvc \ + regress0/rels/oneLoc_no_quant-int_0_1.cvc \ + regress0/rels/rel_1tup_0.cvc \ + regress0/rels/rel_complex_0.cvc \ + regress0/rels/rel_complex_1.cvc \ + regress0/rels/rel_conflict_0.cvc \ + regress0/rels/rel_join_0.cvc \ + regress0/rels/rel_join_0_1.cvc \ + regress0/rels/rel_join_1.cvc \ + regress0/rels/rel_join_1_1.cvc \ + regress0/rels/rel_join_2.cvc \ + regress0/rels/rel_join_2_1.cvc \ + regress0/rels/rel_join_3.cvc \ + regress0/rels/rel_join_3_1.cvc \ + regress0/rels/rel_join_4.cvc \ + regress0/rels/rel_join_5.cvc \ + regress0/rels/rel_join_6.cvc \ + regress0/rels/rel_join_7.cvc \ + regress0/rels/rel_product_0.cvc \ + regress0/rels/rel_product_0_1.cvc \ + regress0/rels/rel_product_1.cvc \ + regress0/rels/rel_product_1_1.cvc \ + regress0/rels/rel_symbolic_1.cvc \ + regress0/rels/rel_symbolic_1_1.cvc \ + regress0/rels/rel_symbolic_2_1.cvc \ + regress0/rels/rel_symbolic_3_1.cvc \ + regress0/rels/rel_tc_11.cvc \ + regress0/rels/rel_tc_2_1.cvc \ + regress0/rels/rel_tc_3.cvc \ + regress0/rels/rel_tc_3_1.cvc \ + regress0/rels/rel_tc_7.cvc \ + regress0/rels/rel_tc_8.cvc \ + regress0/rels/rel_tp_3_1.cvc \ + regress0/rels/rel_tp_join_0.cvc \ + regress0/rels/rel_tp_join_1.cvc \ + regress0/rels/rel_tp_join_2.cvc \ + regress0/rels/rel_tp_join_3.cvc \ + regress0/rels/rel_tp_join_eq_0.cvc \ + regress0/rels/rel_tp_join_int_0.cvc \ + regress0/rels/rel_tp_join_pro_0.cvc \ + regress0/rels/rel_tp_join_var_0.cvc \ + regress0/rels/rel_transpose_0.cvc \ + regress0/rels/rel_transpose_1.cvc \ + regress0/rels/rel_transpose_1_1.cvc \ + regress0/rels/rel_transpose_3.cvc \ + regress0/rels/rel_transpose_4.cvc \ + regress0/rels/rel_transpose_5.cvc \ + regress0/rels/rel_transpose_6.cvc \ + regress0/rels/rel_transpose_7.cvc \ + regress0/rels/relations-ops.smt2 \ + regress0/rels/rels-sharing-simp.cvc \ + regress0/reset-assertions.smt2 \ + regress0/rewriterules/datatypes.smt2 \ + regress0/rewriterules/length_trick.smt2 \ + regress0/rewriterules/native_arrays.smt2 \ + regress0/rewriterules/relation.smt2 \ + regress0/rewriterules/simulate_rewriting.smt2 \ + regress0/sep/dispose-1.smt2 \ + regress0/sep/dup-nemp.smt2 \ + regress0/sep/nemp.smt2 \ + regress0/sep/nil-no-elim.smt2 \ + regress0/sep/nspatial-simp.smt2 \ + regress0/sep/pto-01.smt2 \ + regress0/sep/pto-02.smt2 \ + regress0/sep/sep-01.smt2 \ + regress0/sep/sep-plus1.smt2 \ + regress0/sep/sep-simp-unsat-emp.smt2 \ + regress0/sep/trees-1.smt2 \ + regress0/sep/wand-crash.smt2 \ + regress0/sets/abt-min.smt2 \ + regress0/sets/abt-te-exh.smt2 \ + regress0/sets/abt-te-exh2.smt2 \ + regress0/sets/card-2.smt2 \ + regress0/sets/card-3sets.cvc \ + regress0/sets/card.smt2 \ + regress0/sets/card3-ground.smt2 \ + regress0/sets/complement.cvc \ + regress0/sets/complement2.cvc \ + regress0/sets/complement3.cvc \ + regress0/sets/cvc-sample.cvc \ + regress0/sets/dt-simp-mem.smt2 \ + regress0/sets/emptyset.smt2 \ + regress0/sets/eqtest.smt2 \ + regress0/sets/error1.smt2 \ + regress0/sets/error2.smt2 \ + regress0/sets/insert.smt2 \ + regress0/sets/int-real-univ-unsat.smt2 \ + regress0/sets/int-real-univ.smt2 \ + regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 \ + regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 \ + regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 \ + regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 \ + regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \ + regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 \ + regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 \ + regress0/sets/mar2014/sharing-preregister.smt2 \ + regress0/sets/mar2014/small.smt2 \ + regress0/sets/mar2014/smaller.smt2 \ + regress0/sets/nonvar-univ.smt2 \ + regress0/sets/pre-proc-univ.smt2 \ + regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 \ + regress0/sets/sets-equal.smt2 \ + regress0/sets/sets-inter.smt2 \ + regress0/sets/sets-poly-int-real.smt2 \ + regress0/sets/sets-poly-nonint.smt2 \ + regress0/sets/sets-sample.smt2 \ + regress0/sets/sets-sharing.smt2 \ + regress0/sets/sets-testlemma.smt2 \ + regress0/sets/sets-union.smt2 \ + regress0/sets/sharing-simp.smt2 \ + regress0/sets/union-1a-flip.smt2 \ + regress0/sets/union-1a.smt2 \ + regress0/sets/union-1b-flip.smt2 \ + regress0/sets/union-1b.smt2 \ + regress0/sets/union-2.smt2 \ + regress0/sets/univset-simp.smt2 \ + regress0/simple-lra.smt \ + regress0/simple-lra.smt2 \ + regress0/simple-rdl.smt \ + regress0/simple-rdl.smt2 \ + regress0/simple-uf.smt \ + regress0/simple-uf.smt2 \ + regress0/simple.cvc \ + regress0/simple.smt \ + regress0/simple2.smt \ + regress0/simplification_bug.smt \ + regress0/simplification_bug2.smt \ + regress0/smallcnf.cvc \ + regress0/smt2output.smt2 \ + regress0/strings/bug001.smt2 \ + regress0/strings/bug002.smt2 \ + regress0/strings/bug612.smt2 \ + regress0/strings/bug613.smt2 \ + regress0/strings/escchar.smt2 \ + regress0/strings/escchar_25.smt2 \ + regress0/strings/idof-rewrites.smt2 \ + regress0/strings/idof-sem.smt2 \ + regress0/strings/ilc-like.smt2 \ + regress0/strings/indexof-sym-simp.smt2 \ + regress0/strings/issue1189.smt2 \ + regress0/strings/leadingzero001.smt2 \ + regress0/strings/loop001.smt2 \ + regress0/strings/model001.smt2 \ + regress0/strings/norn-31.smt2 \ + regress0/strings/norn-simp-rew.smt2 \ + regress0/strings/repl-rewrites2.smt2 \ + regress0/strings/rewrites-v2.smt2 \ + regress0/strings/str003.smt2 \ + regress0/strings/str004.smt2 \ + regress0/strings/str005.smt2 \ + regress0/strings/strings-charat.cvc \ + regress0/strings/strings-native-simple.cvc \ + regress0/strings/substr-rewrites.smt2 \ + regress0/strings/type001.smt2 \ + regress0/strings/unsound-0908.smt2 \ + regress0/sygus/General_plus10.sy \ + regress0/sygus/c100.sy \ + regress0/sygus/ccp16.lus.sy \ + regress0/sygus/check-generic-red.sy \ + regress0/sygus/const-var-test.sy \ + regress0/sygus/dt-no-syntax.sy \ + regress0/sygus/let-ringer.sy \ + regress0/sygus/let-simp.sy \ + regress0/sygus/no-syntax-test-bool.sy \ + regress0/sygus/no-syntax-test.sy \ + regress0/sygus/parity-AIG-d0.sy \ + regress0/sygus/parse-bv-let.sy \ + regress0/sygus/real-si-all.sy \ + regress0/sygus/strings-unconstrained.sy \ + regress0/sygus/uminus_one.sy \ + regress0/test11.cvc \ + regress0/test9.cvc \ + regress0/tptp/ARI086$(equals)1.p \ + regress0/tptp/DAT001$(equals)1.p \ + regress0/tptp/KRS018+1.p \ + regress0/tptp/KRS063+1.p \ + regress0/tptp/MGT019+2.p \ + regress0/tptp/MGT041-2.p \ + regress0/tptp/PUZ131_1.p \ + regress0/tptp/SYN000$(equals)2.p \ + regress0/tptp/SYN000+1.p \ + regress0/tptp/SYN000+2.p \ + regress0/tptp/SYN000-1.p \ + regress0/tptp/SYN000-2.p \ + regress0/tptp/SYN000_1.p \ + regress0/tptp/SYN000_2.p \ + regress0/tptp/SYN075-1.p \ + regress0/tptp/tff0-arith.p \ + regress0/tptp/tff0.p \ + regress0/tptp/tptp_parser.p \ + regress0/tptp/tptp_parser10.p \ + regress0/tptp/tptp_parser2.p \ + regress0/tptp/tptp_parser3.p \ + regress0/tptp/tptp_parser4.p \ + regress0/tptp/tptp_parser5.p \ + regress0/tptp/tptp_parser6.p \ + regress0/tptp/tptp_parser7.p \ + regress0/tptp/tptp_parser8.p \ + regress0/tptp/tptp_parser9.p \ + regress0/uf/NEQ016_size5_reduced2a.smt \ + regress0/uf/NEQ016_size5_reduced2b.smt \ + regress0/uf/bool-pred-nested.smt2 \ + regress0/uf/ccredesign-fuzz.smt \ + regress0/uf/cnf-and-neg.smt2 \ + regress0/uf/cnf-iff-base.smt2 \ + regress0/uf/cnf-iff.smt2 \ + regress0/uf/cnf-ite.smt2 \ + regress0/uf/cnf_abc.smt2 \ + regress0/uf/dead_dnd002.smt \ + regress0/uf/eq_diamond1.smt \ + regress0/uf/eq_diamond14.reduced.smt \ + regress0/uf/eq_diamond14.reduced2.smt \ + regress0/uf/eq_diamond23.smt \ + regress0/uf/euf_simp01.smt \ + regress0/uf/euf_simp02.smt \ + regress0/uf/euf_simp03.smt \ + regress0/uf/euf_simp04.smt \ + regress0/uf/euf_simp05.smt \ + regress0/uf/euf_simp06.smt \ + regress0/uf/euf_simp08.smt \ + regress0/uf/euf_simp09.smt \ + regress0/uf/euf_simp10.smt \ + regress0/uf/euf_simp11.smt \ + regress0/uf/euf_simp12.smt \ + regress0/uf/euf_simp13.smt \ + regress0/uf/iso_brn001.smt \ + regress0/uf/pred.smt \ + regress0/uf/simple.01.cvc \ + regress0/uf/simple.02.cvc \ + regress0/uf/simple.03.cvc \ + regress0/uf/simple.04.cvc \ + regress0/uf20-03.cvc \ + regress0/uflia/check01.smt2 \ + regress0/uflia/check02.smt2 \ + regress0/uflia/check03.smt2 \ + regress0/uflia/check04.smt2 \ + regress0/uflia/error0.delta01.smt \ + regress0/uflia/error1.smt \ + regress0/uflia/error30.smt \ + regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 \ + regress0/uflia/tiny.smt2 \ + regress0/uflia/xs-09-16-3-4-1-5.delta01.smt \ + regress0/uflia/xs-09-16-3-4-1-5.delta02.smt \ + regress0/uflia/xs-09-16-3-4-1-5.delta03.smt \ + regress0/uflia/xs-09-16-3-4-1-5.delta04.smt \ + regress0/uflra/bug293.cvc \ + regress0/uflra/bug449.smt \ + regress0/uflra/constants0.smt \ + regress0/uflra/fuzz01.smt \ + regress0/uflra/incorrect1.delta01.smt \ + regress0/uflra/incorrect1.delta02.smt \ + regress0/uflra/neq-deltacomp.smt \ + regress0/uflra/pb_real_10_0100_10_10.smt \ + regress0/uflra/pb_real_10_0100_10_11.smt \ + regress0/uflra/pb_real_10_0100_10_15.smt \ + regress0/uflra/pb_real_10_0100_10_16.smt \ + regress0/uflra/pb_real_10_0100_10_19.smt \ + regress0/uflra/pb_real_10_0200_10_22.smt \ + regress0/uflra/pb_real_10_0200_10_26.smt \ + regress0/uflra/pb_real_10_0200_10_29.smt \ + regress0/uflra/simple.01.cvc \ + regress0/uflra/simple.02.cvc \ + regress0/uflra/simple.03.cvc \ + regress0/uflra/simple.04.cvc \ + regress0/unconstrained/arith.smt2 \ + regress0/unconstrained/arith3.smt2 \ + regress0/unconstrained/arith4.smt2 \ + regress0/unconstrained/arith5.smt2 \ + regress0/unconstrained/arith6.smt2 \ + regress0/unconstrained/array1.smt2 \ + regress0/unconstrained/bvbool.smt2 \ + regress0/unconstrained/bvbool2.smt2 \ + regress0/unconstrained/bvbool3.smt2 \ + regress0/unconstrained/bvcmp.smt2 \ + regress0/unconstrained/bvconcat2.smt2 \ + regress0/unconstrained/bvext.smt2 \ + regress0/unconstrained/bvite.smt2 \ + regress0/unconstrained/bvmul.smt2 \ + regress0/unconstrained/bvmul2.smt2 \ + regress0/unconstrained/bvmul3.smt2 \ + regress0/unconstrained/bvnot.smt2 \ + regress0/unconstrained/bvsle.smt2 \ + regress0/unconstrained/bvsle2.smt2 \ + regress0/unconstrained/bvsle3.smt2 \ + regress0/unconstrained/bvsle4.smt2 \ + regress0/unconstrained/bvsle5.smt2 \ + regress0/unconstrained/bvslt.smt2 \ + regress0/unconstrained/bvslt2.smt2 \ + regress0/unconstrained/bvslt3.smt2 \ + regress0/unconstrained/bvslt4.smt2 \ + regress0/unconstrained/bvslt5.smt2 \ + regress0/unconstrained/bvule.smt2 \ + regress0/unconstrained/bvule2.smt2 \ + regress0/unconstrained/bvule3.smt2 \ + regress0/unconstrained/bvule4.smt2 \ + regress0/unconstrained/bvule5.smt2 \ + regress0/unconstrained/bvult.smt2 \ + regress0/unconstrained/bvult2.smt2 \ + regress0/unconstrained/bvult3.smt2 \ + regress0/unconstrained/bvult4.smt2 \ + regress0/unconstrained/bvult5.smt2 \ + regress0/unconstrained/geq.smt2 \ + regress0/unconstrained/gt.smt2 \ + regress0/unconstrained/ite.smt2 \ + regress0/unconstrained/leq.smt2 \ + regress0/unconstrained/lt.smt2 \ + regress0/unconstrained/mult1.smt2 \ + regress0/unconstrained/uf1.smt2 \ + regress0/unconstrained/xor.smt2 \ + regress0/wiki.01.cvc \ + regress0/wiki.02.cvc \ + regress0/wiki.03.cvc \ + regress0/wiki.04.cvc \ + regress0/wiki.05.cvc \ + regress0/wiki.06.cvc \ + regress0/wiki.07.cvc \ + regress0/wiki.08.cvc \ + regress0/wiki.09.cvc \ + regress0/wiki.10.cvc \ + regress0/wiki.11.cvc \ + regress0/wiki.12.cvc \ + regress0/wiki.13.cvc \ + regress0/wiki.14.cvc \ + regress0/wiki.15.cvc \ + regress0/wiki.16.cvc \ + regress0/wiki.17.cvc \ + regress0/wiki.18.cvc \ + regress0/wiki.19.cvc \ + regress0/wiki.20.cvc \ + regress0/wiki.21.cvc + +REG1_TESTS = \ + regress1/arith/arith-int-004.cvc \ + regress1/arith/arith-int-011.cvc \ + regress1/arith/arith-int-012.cvc \ + regress1/arith/arith-int-013.cvc \ + regress1/arith/arith-int-022.cvc \ + regress1/arith/arith-int-024.cvc \ + regress1/arith/arith-int-047.cvc \ + regress1/arith/arith-int-048.cvc \ + regress1/arith/arith-int-050.cvc \ + regress1/arith/arith-int-084.cvc \ + regress1/arith/arith-int-085.cvc \ + regress1/arith/arith-int-097.cvc \ + regress1/arith/bug547.1.smt2 \ + regress1/arith/bug716.0.smt2 \ + regress1/arith/bug716.1.cvc \ + regress1/arith/div.03.smt2 \ + regress1/arith/div.06.smt2 \ + regress1/arith/div.08.smt2 \ + regress1/arith/div.09.smt2 \ + regress1/arith/miplib3.cvc \ + regress1/arith/mod.02.smt2 \ + regress1/arith/mod.03.smt2 \ + regress1/arith/mult.02.smt2 \ + regress1/arith/problem__003.smt2 \ + regress1/arrayinuf_error.smt2 \ + regress1/aufbv/bug580.smt2 \ + regress1/aufbv/fuzz10.smt \ + regress1/auflia/bug330.smt2 \ + regress1/boolean-terms-kernel2.smt2 \ + regress1/boolean.cvc \ + regress1/bug216.smt2 \ + regress1/bug296.smt2 \ + regress1/bug425.cvc \ + regress1/bug507.smt2 \ + regress1/bug512.smt2 \ + regress1/bug516.smt2 \ + regress1/bug519.smt2 \ + regress1/bug520.smt2 \ + regress1/bug521.smt2 \ + regress1/bug543.smt2 \ + regress1/bug567.smt2 \ + regress1/bug593.smt2 \ + regress1/bug681.smt2 \ + regress1/bug694-Unapply1.scala-0.smt2 \ + regress1/bug800.smt2 \ + regress1/bv/bug787.smt2 \ + regress1/bv/bug_extract_mult_leading_bit.smt2 \ + regress1/bv/bv-int-collapse2-sat.smt2 \ + regress1/bv/bv-proof00.smt \ + regress1/bv/bv2nat-ground.smt2 \ + regress1/bv/bv2nat-simp-range-sat.smt2 \ + regress1/bv/cmu-rdk-3.smt2 \ + regress1/bv/decision-weight00.smt2 \ + regress1/bv/divtest.smt2 \ + regress1/bv/fuzz34.smt \ + regress1/bv/fuzz38.smt \ + regress1/bv/unsound1.smt2 \ + regress1/bvdiv2.smt2 \ + regress1/constarr3.cvc \ + regress1/constarr3.smt2 \ + regress1/datatypes/acyclicity-sr-ground096.smt2 \ + regress1/datatypes/dt-color-2.6.smt2 \ + regress1/datatypes/dt-param-card4-unsat.smt2 \ + regress1/datatypes/error.cvc \ + regress1/datatypes/manos-model.smt2 \ + regress1/decision/error3.smt \ + regress1/decision/quant-Arrays_Q1-noinfer.smt2 \ + regress1/decision/quant-symmetric_unsat_7.smt2 \ + regress1/error.cvc \ + regress1/errorcrash.smt2 \ + regress1/fmf-fun-dbu.smt2 \ + regress1/fmf/ALG008-1.smt2 \ + regress1/fmf/LeftistHeap.scala-8-ncm.smt2 \ + regress1/fmf/PUZ001+1.smt2 \ + regress1/fmf/agree466.smt2 \ + regress1/fmf/agree467.smt2 \ + regress1/fmf/alg202+1.smt2 \ + regress1/fmf/am-bad-model.cvc \ + regress1/fmf/bound-int-alt.smt2 \ + regress1/fmf/bug0909.smt2 \ + regress1/fmf/bug651.smt2 \ + regress1/fmf/bug723-irrelevant-funs.smt2 \ + regress1/fmf/bug764.smt2 \ + regress1/fmf/cons-sets-bounds.smt2 \ + regress1/fmf/constr-ground-to.smt2 \ + regress1/fmf/datatypes-ufinite-nested.smt2 \ + regress1/fmf/datatypes-ufinite.smt2 \ + regress1/fmf/dt-proper-model.smt2 \ + regress1/fmf/fc-pigeonhole19.smt2 \ + regress1/fmf/fib-core.smt2 \ + regress1/fmf/fmf-bound-2dim.smt2 \ + regress1/fmf/fmf-bound-int.smt2 \ + regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 \ + regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 \ + regress1/fmf/fmf-strange-bounds.smt2 \ + regress1/fmf/forall_unit_data.smt2 \ + regress1/fmf/fore19-exp2-core.smt2 \ + regress1/fmf/german169.smt2 \ + regress1/fmf/german73.smt2 \ + regress1/fmf/issue916-fmf-or.smt2 \ + regress1/fmf/jasmin-cdt-crash.smt2 \ + regress1/fmf/ko-bound-set.cvc \ + regress1/fmf/loopy_coda.smt2 \ + regress1/fmf/lst-no-self-rev-exp.smt2 \ + regress1/fmf/memory_model-R_cpp-dd.cvc \ + regress1/fmf/nun-0208-to.smt2 \ + regress1/fmf/pow2-bool.smt2 \ + regress1/fmf/refcount24.cvc.smt2 \ + regress1/fmf/sc-crash-052316.smt2 \ + regress1/fmf/with-ind-104-core.smt2 \ + regress1/gensys_brn001.smt2 \ + regress1/ho/auth0068.smt2 \ + regress1/ho/fta0409.smt2 \ + regress1/ho/ho-exponential-model.smt2 \ + regress1/ho/ho-matching-enum-2.smt2 \ + regress1/ho/ho-std-fmf.smt2 \ + regress1/hole6.cvc \ + regress1/ite5.smt2 \ + regress1/lemmas/clocksynchro_5clocks.main_invar.base.smt \ + regress1/lemmas/pursuit-safety-8.smt \ + regress1/lemmas/simple_startup_9nodes.abstract.base.smt \ + regress1/nl/NAVIGATION2.smt2 \ + regress1/nl/arrowsmith-050317.smt2 \ + regress1/nl/bad-050217.smt2 \ + regress1/nl/bug698.smt2 \ + regress1/nl/coeff-unsat-base.smt2 \ + regress1/nl/coeff-unsat.smt2 \ + regress1/nl/combine.smt2 \ + regress1/nl/cos-bound.smt2 \ + regress1/nl/cos1-tc.smt2 \ + regress1/nl/disj-eval.smt2 \ + regress1/nl/dist-big.smt2 \ + regress1/nl/div-mod-partial.smt2 \ + regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 \ + regress1/nl/exp-4.5-lt.smt2 \ + regress1/nl/exp1-lb.smt2 \ + regress1/nl/exp_monotone.smt2 \ + regress1/nl/metitarski-1025.smt2 \ + regress1/nl/metitarski-3-4.smt2 \ + regress1/nl/metitarski_3_4_2e.smt2 \ + regress1/nl/mirko-050417.smt2 \ + regress1/nl/nl-eq-infer.smt2 \ + regress1/nl/nl-help-unsat-quant.smt2 \ + regress1/nl/nl-unk-quant.smt2 \ + regress1/nl/ones.smt2 \ + regress1/nl/poly-1025.smt2 \ + regress1/nl/quant-nl.smt2 \ + regress1/nl/red-exp.smt2 \ + regress1/nl/rewriting-sums.smt2 \ + regress1/nl/shifting.smt2 \ + regress1/nl/shifting2.smt2 \ + regress1/nl/simple-mono-unsat.smt2 \ + regress1/nl/simple-mono.smt2 \ + regress1/nl/sin-compare-across-phase.smt2 \ + regress1/nl/sin-compare.smt2 \ + regress1/nl/sin-init-tangents.smt2 \ + regress1/nl/sin-sign.smt2 \ + regress1/nl/sin-sym2.smt2 \ + regress1/nl/sin1-deq-sat.smt2 \ + regress1/nl/sin1-lb.smt2 \ + regress1/nl/sin1-sat.smt2 \ + regress1/nl/sin1-ub.smt2 \ + regress1/nl/sin2-lb.smt2 \ + regress1/nl/sin2-ub.smt2 \ + regress1/nl/sqrt-problem-1.smt2 \ + regress1/nl/sugar-ident-2.smt2 \ + regress1/nl/sugar-ident-3.smt2 \ + regress1/nl/sugar-ident.smt2 \ + regress1/nl/tan-rewrite2.smt2 \ + regress1/nl/zero-subset.smt2 \ + regress1/non-fatal-errors.smt2 \ + regress1/parsing_ringer.cvc \ + regress1/proof00.smt2 \ + regress1/push-pop/arith_lra_01.smt2 \ + regress1/push-pop/arith_lra_02.smt2 \ + regress1/push-pop/bug-fmf-fun-skolem.smt2 \ + regress1/push-pop/bug216.smt2 \ + regress1/push-pop/bug326.smt2 \ + regress1/push-pop/fuzz_1.smt2 \ + regress1/push-pop/fuzz_10.smt2 \ + regress1/push-pop/fuzz_11.smt2 \ + regress1/push-pop/fuzz_15.smt2 \ + regress1/push-pop/fuzz_16.smt2 \ + regress1/push-pop/fuzz_19.smt2 \ + regress1/push-pop/fuzz_1_to_52_merged.smt2 \ + regress1/push-pop/fuzz_20.smt2 \ + regress1/push-pop/fuzz_23.smt2 \ + regress1/push-pop/fuzz_24.smt2 \ + regress1/push-pop/fuzz_25.smt2 \ + regress1/push-pop/fuzz_26.smt2 \ + regress1/push-pop/fuzz_28.smt2 \ + regress1/push-pop/fuzz_29.smt2 \ + regress1/push-pop/fuzz_30.smt2 \ + regress1/push-pop/fuzz_32.smt2 \ + regress1/push-pop/fuzz_34.smt2 \ + regress1/push-pop/fuzz_35.smt2 \ + regress1/push-pop/fuzz_37.smt2 \ + regress1/push-pop/fuzz_39.smt2 \ + regress1/push-pop/fuzz_3_1.smt2 \ + regress1/push-pop/fuzz_3_10.smt2 \ + regress1/push-pop/fuzz_3_11.smt2 \ + regress1/push-pop/fuzz_3_12.smt2 \ + regress1/push-pop/fuzz_3_13.smt2 \ + regress1/push-pop/fuzz_3_14.smt2 \ + regress1/push-pop/fuzz_3_15.smt2 \ + regress1/push-pop/fuzz_3_2.smt2 \ + regress1/push-pop/fuzz_3_3.smt2 \ + regress1/push-pop/fuzz_3_4.smt2 \ + regress1/push-pop/fuzz_3_5.smt2 \ + regress1/push-pop/fuzz_3_6.smt2 \ + regress1/push-pop/fuzz_3_7.smt2 \ + regress1/push-pop/fuzz_3_8.smt2 \ + regress1/push-pop/fuzz_3_9.smt2 \ + regress1/push-pop/fuzz_4.smt2 \ + regress1/push-pop/fuzz_40.smt2 \ + regress1/push-pop/fuzz_41.smt2 \ + regress1/push-pop/fuzz_42.smt2 \ + regress1/push-pop/fuzz_43.smt2 \ + regress1/push-pop/fuzz_44.smt2 \ + regress1/push-pop/fuzz_45.smt2 \ + regress1/push-pop/fuzz_5.smt2 \ + regress1/push-pop/fuzz_51.smt2 \ + regress1/push-pop/fuzz_52.smt2 \ + regress1/push-pop/fuzz_5_1.smt2 \ + regress1/push-pop/fuzz_5_2.smt2 \ + regress1/push-pop/fuzz_5_3.smt2 \ + regress1/push-pop/fuzz_5_4.smt2 \ + regress1/push-pop/fuzz_5_5.smt2 \ + regress1/push-pop/fuzz_5_6.smt2 \ + regress1/push-pop/fuzz_6.smt2 \ + regress1/push-pop/fuzz_7.smt2 \ + regress1/push-pop/fuzz_8.smt2 \ + regress1/push-pop/fuzz_9.smt2 \ + regress1/push-pop/quant-fun-proc-unmacro.smt2 \ + regress1/push-pop/quant-fun-proc.smt2 \ + regress1/quantifiers/006-cbqi-ite.smt2 \ + regress1/quantifiers/AdditiveMethods_OwnedResults.Mz.smt2 \ + regress1/quantifiers/Arrays_Q1-noinfer.smt2 \ + regress1/quantifiers/NUM878.smt2 \ + regress1/quantifiers/RND-small.smt2 \ + regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 \ + regress1/quantifiers/RND_4_16.smt2 \ + regress1/quantifiers/anti-sk-simp.smt2 \ + regress1/quantifiers/ari118-bv-2occ-x.smt2 \ + regress1/quantifiers/arith-rec-fun.smt2 \ + regress1/quantifiers/array-unsat-simp3.smt2 \ + regress1/quantifiers/bi-artm-s.smt2 \ + regress1/quantifiers/bignum_quant.smt2 \ + regress1/quantifiers/bug802.smt2 \ + regress1/quantifiers/bug822.smt2 \ + regress1/quantifiers/bug_743.smt2 \ + regress1/quantifiers/burns13.smt2 \ + regress1/quantifiers/burns4.smt2 \ + regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 \ + regress1/quantifiers/cdt-0208-to.smt2 \ + regress1/quantifiers/ext-ex-deq-trigger.smt2 \ + regress1/quantifiers/extract-nproc.smt2 \ + regress1/quantifiers/florian-case-ax.smt2 \ + regress1/quantifiers/gauss_init_0030.fof.smt2 \ + regress1/quantifiers/inst-max-level-segf.smt2 \ + regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 \ + regress1/quantifiers/is-even.smt2 \ + regress1/quantifiers/javafe.ast.StmtVec.009.smt2 \ + regress1/quantifiers/mix-coeff.smt2 \ + regress1/quantifiers/model_6_1_bv.smt2 \ + regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 \ + regress1/quantifiers/opisavailable-12.smt2 \ + regress1/quantifiers/parametric-lists.smt2 \ + regress1/quantifiers/psyco-001-bv.smt2 \ + regress1/quantifiers/psyco-107-bv.smt2 \ + regress1/quantifiers/psyco-196.smt2 \ + regress1/quantifiers/qbv-disequality3.smt2 \ + regress1/quantifiers/qbv-simple-2vars-vo.smt2 \ + regress1/quantifiers/qbv-test-invert-bvashr-0.smt2 \ + regress1/quantifiers/qbv-test-invert-bvashr-1.smt2 \ + regress1/quantifiers/qbv-test-invert-bvcomp.smt2 \ + regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2 \ + regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2 \ + regress1/quantifiers/qbv-test-invert-bvmul.smt2 \ + regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 \ + regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 \ + regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 \ + regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 \ + regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 \ + regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 \ + regress1/quantifiers/qbv-test-urem-rewrite.smt2 \ + regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 \ + regress1/quantifiers/qcft-smtlib3dbc51.smt2 \ + regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 \ + regress1/quantifiers/rew-to-0211-dd.smt2 \ + regress1/quantifiers/ricart-agrawala6.smt2 \ + regress1/quantifiers/set3.smt2 \ + regress1/quantifiers/set8.smt2 \ + regress1/quantifiers/small-pipeline-fixpoint-3.smt2 \ + regress1/quantifiers/smtlib384a03.smt2 \ + regress1/quantifiers/smtlib46f14a.smt2 \ + regress1/quantifiers/smtlibf957ea.smt2 \ + regress1/quantifiers/stream-x2014-09-18-unsat.smt2 \ + regress1/quantifiers/symmetric_unsat_7.smt2 \ + regress1/quantifiers/z3.620661-no-fv-trigger.smt2 \ + regress1/rels/addr_book_1.cvc \ + regress1/rels/addr_book_1_1.cvc \ + regress1/rels/bv1-unit.cvc \ + regress1/rels/bv1-unitb.cvc \ + regress1/rels/bv1.cvc \ + regress1/rels/bv1p-sat.cvc \ + regress1/rels/bv1p.cvc \ + regress1/rels/bv2.cvc \ + regress1/rels/iden_1_1.cvc \ + regress1/rels/join-eq-structure-and.cvc \ + regress1/rels/join-eq-structure.cvc \ + regress1/rels/join-eq-structure_0_1.cvc \ + regress1/rels/joinImg_0_1.cvc \ + regress1/rels/joinImg_0_2.cvc \ + regress1/rels/joinImg_1.cvc \ + regress1/rels/joinImg_1_1.cvc \ + regress1/rels/joinImg_2.cvc \ + regress1/rels/joinImg_2_1.cvc \ + regress1/rels/prod-mod-eq.cvc \ + regress1/rels/prod-mod-eq2.cvc \ + regress1/rels/rel_complex_3.cvc \ + regress1/rels/rel_complex_4.cvc \ + regress1/rels/rel_complex_5.cvc \ + regress1/rels/rel_mix_0_1.cvc \ + regress1/rels/rel_pressure_0.cvc \ + regress1/rels/rel_tc_10_1.cvc \ + regress1/rels/rel_tc_4.cvc \ + regress1/rels/rel_tc_4_1.cvc \ + regress1/rels/rel_tc_5_1.cvc \ + regress1/rels/rel_tc_6.cvc \ + regress1/rels/rel_tc_9_1.cvc \ + regress1/rels/rel_tp_2.cvc \ + regress1/rels/rel_tp_join_2_1.cvc \ + regress1/rels/set-strat.cvc \ + regress1/rels/strat.cvc \ + regress1/rels/strat_0_1.cvc \ + regress1/rewriterules/datatypes_sat.smt2 \ + regress1/rewriterules/length_gen.smt2 \ + regress1/rewriterules/length_gen_020.smt2 \ + regress1/rewriterules/length_gen_020_sat.smt2 \ + regress1/rewriterules/length_gen_040.smt2 \ + regress1/rewriterules/length_gen_040_lemma.smt2 \ + regress1/rewriterules/length_gen_040_lemma_trigger.smt2 \ + regress1/rewriterules/reachability_back_to_the_future.smt2 \ + regress1/rewriterules/read5.smt2 \ + regress1/sep/chain-int.smt2 \ + regress1/sep/crash1220.smt2 \ + regress1/sep/dispose-list-4-init.smt2 \ + regress1/sep/emp2-quant-unsat.smt2 \ + regress1/sep/finite-witness-sat.smt2 \ + regress1/sep/fmf-nemp-2.smt2 \ + regress1/sep/loop-1220.smt2 \ + regress1/sep/pto-04.smt2 \ + regress1/sep/quant_wand.smt2 \ + regress1/sep/sep-02.smt2 \ + regress1/sep/sep-03.smt2 \ + regress1/sep/sep-find2.smt2 \ + regress1/sep/sep-fmf-priority.smt2 \ + regress1/sep/sep-neg-1refine.smt2 \ + regress1/sep/sep-neg-nstrict.smt2 \ + regress1/sep/sep-neg-nstrict2.smt2 \ + regress1/sep/sep-neg-simple.smt2 \ + regress1/sep/sep-neg-swap.smt2 \ + regress1/sep/sep-nterm-again.smt2 \ + regress1/sep/sep-nterm-val-model.smt2 \ + regress1/sep/sep-simp-unc.smt2 \ + regress1/sep/simple-neg-sat.smt2 \ + regress1/sep/split-find-unsat-w-emp.smt2 \ + regress1/sep/split-find-unsat.smt2 \ + regress1/sep/wand-0526-sat.smt2 \ + regress1/sep/wand-false.smt2 \ + regress1/sep/wand-nterm-simp.smt2 \ + regress1/sep/wand-nterm-simp2.smt2 \ + regress1/sep/wand-simp-sat.smt2 \ + regress1/sep/wand-simp-sat2.smt2 \ + regress1/sep/wand-simp-unsat.smt2 \ + regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 \ + regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 \ + regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 \ + regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 \ + regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 \ + regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 \ + regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 \ + regress1/sets/arjun-set-univ.cvc \ + regress1/sets/card-3.smt2 \ + regress1/sets/card-4.smt2 \ + regress1/sets/card-5.smt2 \ + regress1/sets/card-6.smt2 \ + regress1/sets/card-7.smt2 \ + regress1/sets/card-vc6-minimized.smt2 \ + regress1/sets/copy_check_heap_access_33_4.smt2 \ + regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 \ + regress1/sets/fuzz14418.smt2 \ + regress1/sets/fuzz15201.smt2 \ + regress1/sets/fuzz31811.smt2 \ + regress1/sets/insert_invariant_37_2.smt2 \ + regress1/sets/lemmabug-ListElts317minimized.smt2 \ + regress1/sets/remove_check_free_31_6.smt2 \ + regress1/sets/sets-disequal.smt2 \ + regress1/sets/sets-tuple-poly.cvc \ + regress1/sets/sharingbug.smt2 \ + regress1/sets/univ-set-uf-elim.smt2 \ + regress1/simplification_bug4.smt2 \ + regress1/sqrt2-sort-inf-unk.smt2 \ + regress1/strings/artemis-0512-nonterm.smt2 \ + regress1/strings/at001.smt2 \ + regress1/strings/bug615.smt2 \ + regress1/strings/bug682.smt2 \ + regress1/strings/bug686dd.smt2 \ + regress1/strings/bug768.smt2 \ + regress1/strings/bug799-min.smt2 \ + regress1/strings/chapman150408.smt2 \ + regress1/strings/cmu-2db2-extf-reg.smt2 \ + regress1/strings/cmu-5042-0707-2.smt2 \ + regress1/strings/cmu-inc-nlpp-071516.smt2 \ + regress1/strings/cmu-substr-rw.smt2 \ + regress1/strings/crash-1019.smt2 \ + regress1/strings/csp-prefix-exp-bug.smt2 \ + regress1/strings/double-replace.smt2 \ + regress1/strings/fmf001.smt2 \ + regress1/strings/fmf002.smt2 \ + regress1/strings/gm-inc-071516-2.smt2 \ + regress1/strings/goodAI.smt2 \ + regress1/strings/idof-handg.smt2 \ + regress1/strings/idof-nconst-index.smt2 \ + regress1/strings/idof-neg-index.smt2 \ + regress1/strings/idof-triv.smt2 \ + regress1/strings/ilc-l-nt.smt2 \ + regress1/strings/issue1105.smt2 \ + regress1/strings/kaluza-fl.smt2 \ + regress1/strings/loop002.smt2 \ + regress1/strings/loop003.smt2 \ + regress1/strings/loop004.smt2 \ + regress1/strings/loop005.smt2 \ + regress1/strings/loop006.smt2 \ + regress1/strings/loop007.smt2 \ + regress1/strings/loop008.smt2 \ + regress1/strings/loop009.smt2 \ + regress1/strings/nf-ff-contains-abs.smt2 \ + regress1/strings/norn-360.smt2 \ + regress1/strings/norn-ab.smt2 \ + regress1/strings/norn-nel-bug-052116.smt2 \ + regress1/strings/norn-simp-rew-sat.smt2 \ + regress1/strings/pierre150331.smt2 \ + regress1/strings/regexp001.smt2 \ + regress1/strings/regexp002.smt2 \ + regress1/strings/regexp003.smt2 \ + regress1/strings/reloop.smt2 \ + regress1/strings/repl-empty-sem.smt2 \ + regress1/strings/repl-soundness-sem.smt2 \ + regress1/strings/rew-020618.smt2 \ + regress1/strings/str001.smt2 \ + regress1/strings/str002.smt2 \ + regress1/strings/str006.smt2 \ + regress1/strings/str007.smt2 \ + regress1/strings/string-unsound-sem.smt2 \ + regress1/strings/strings-index-empty.smt2 \ + regress1/strings/strip-endpt-sound.smt2 \ + regress1/strings/substr001.smt2 \ + regress1/strings/type002.smt2 \ + regress1/strings/type003.smt2 \ + regress1/strings/username_checker_min.smt2 \ + regress1/sygus/VC22_a.sy \ + regress1/sygus/array_search_2.sy \ + regress1/sygus/array_sum_2_5.sy \ + regress1/sygus/cegar1.sy \ + regress1/sygus/cggmp.sy \ + regress1/sygus/clock-inc-tuple.sy \ + regress1/sygus/commutative.sy \ + regress1/sygus/constant.sy \ + regress1/sygus/dt-test-ns.sy \ + regress1/sygus/dup-op.sy \ + regress1/sygus/fg_polynomial3.sy \ + regress1/sygus/hd-01-d1-prog.sy \ + regress1/sygus/hd-19-d1-prog-dup-op.sy \ + regress1/sygus/hd-sdiv.sy \ + regress1/sygus/icfp_14.12-flip-args.sy \ + regress1/sygus/icfp_14.12.sy \ + regress1/sygus/icfp_28_10.sy \ + regress1/sygus/icfp_easy-ite.sy \ + regress1/sygus/inv-example.sy \ + regress1/sygus/inv-unused.sy \ + regress1/sygus/list-head-x.sy \ + regress1/sygus/max.sy \ + regress1/sygus/multi-fun-polynomial2.sy \ + regress1/sygus/nflat-fwd-3.sy \ + regress1/sygus/nflat-fwd.sy \ + regress1/sygus/nia-max-square-ns.sy \ + regress1/sygus/no-flat-simp.sy \ + regress1/sygus/no-mention.sy \ + regress1/sygus/process-10-vars.sy \ + regress1/sygus/qe.sy \ + regress1/sygus/real-grammar.sy \ + regress1/sygus/stopwatch-bt.sy \ + regress1/sygus/strings-concat-3-args.sy \ + regress1/sygus/strings-double-rec.sy \ + regress1/sygus/strings-small.sy \ + regress1/sygus/strings-template-infer-unused.sy \ + regress1/sygus/strings-template-infer.sy \ + regress1/sygus/strings-trivial-simp.sy \ + regress1/sygus/strings-trivial-two-type.sy \ + regress1/sygus/strings-trivial.sy \ + regress1/sygus/sygus-dt.sy \ + regress1/sygus/tl-type-0.sy \ + regress1/sygus/tl-type-4x.sy \ + regress1/sygus/tl-type.sy \ + regress1/sygus/triv-type-mismatch-si.sy \ + regress1/sygus/twolets1.sy \ + regress1/sygus/twolets2-orig.sy \ + regress1/sygus/unbdd_inv_gen_ex7.sy \ + regress1/sygus/unbdd_inv_gen_winf1.sy \ + regress1/test12.cvc \ + regress1/trim.cvc \ + regress1/uf2.smt2 \ + regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2 \ + regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 \ + regress1/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 \ + regress1/uflia/microwave21.ec.minimized.smt2 \ + regress1/uflia/simple_cyclic2.smt2 \ + regress1/uflia/speed2_e8_449_e8_517.ec.smt2 \ + regress1/uflia/stalmark_e7_27_e7_31.ec.smt2 + +REG2_TESTS = \ + regress2/DTP_k2_n35_c175_s15.smt2 \ + regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 \ + regress2/GEO123+1.minimized.smt2 \ + regress2/arith/abz5_1400.smt \ + regress2/arith/lpsat-goal-9.smt2 \ + regress2/arith/prp-13-24.smt2 \ + regress2/arith/pursuit-safety-11.smt \ + regress2/arith/pursuit-safety-12.smt \ + regress2/arith/qlock-4-10-9.base.cvc.smt2 \ + regress2/arith/sc-7.base.cvc.smt \ + regress2/arith/uart-8.base.cvc.smt \ + regress2/auflia-fuzz06.smt \ + regress2/bug136.smt \ + regress2/bug148.smt \ + regress2/bug394.smt2 \ + regress2/bug674.smt2 \ + regress2/bug765.smt2 \ + regress2/bug812.smt2 \ + regress2/error0.smt2 \ + regress2/error1.smt \ + regress2/friedman_n4_i5.smt \ + regress2/fuzz_2.smt \ + regress2/hash_sat_06_19.smt2 \ + regress2/hash_sat_07_17.smt2 \ + regress2/hash_sat_09_09.smt2 \ + regress2/hash_sat_10_09.smt2 \ + regress2/hole7.cvc \ + regress2/hole8.cvc \ + regress2/instance_1444.smt \ + regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 \ + regress2/javafe.ast.WhileStmt.447_no_forall.smt2 \ + regress2/nl/siegel-nl-bases.smt2 \ + regress2/ooo.rf6.smt2 \ + regress2/ooo.tag10.smt2 \ + regress2/piVC_5581bd.smt2 \ + regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 \ + regress2/quantifiers/ForElimination-scala-9.smt2 \ + regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 \ + regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 \ + regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 \ + regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2 \ + regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2 \ + regress2/quantifiers/nunchaku2309663.nun.min.smt2 \ + regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 \ + regress2/strings/cmu-dis-0707-3.smt2 \ + regress2/strings/cmu-disagree-0707-dd.smt2 \ + regress2/strings/cmu-prereg-fmf.smt2 \ + regress2/strings/cmu-repl-len-nterm.smt2 \ + regress2/strings/norn-dis-0707-3.smt2 \ + regress2/sygus/MPwL_d1s3.sy \ + regress2/sygus/array_sum_dd.sy \ + regress2/sygus/icfp_easy_mt_ite.sy \ + regress2/sygus/inv_gen_n_c11.sy \ + regress2/sygus/lustre-real.sy \ + regress2/sygus/max2-univ.sy \ + regress2/sygus/mpg_guard1-dd.sy \ + regress2/sygus/nia-max-square.sy \ + regress2/sygus/no-syntax-test-no-si.sy \ + regress2/sygus/process-10-vars-2fun.sy \ + regress2/sygus/process-arg-invariance.sy \ + regress2/sygus/real-grammar-neg.sy \ + regress2/sygus/three.sy \ + regress2/typed_v1l50016-simp.cvc \ + regress2/uflia-error0.smt2 \ + regress2/xs-09-16-3-4-1-5.decn.smt \ + regress2/xs-09-16-3-4-1-5.smt + +REG3_TESTS = \ + regress3/bmc-ibm-1.smt \ + regress3/bmc-ibm-2.smt \ + regress3/bmc-ibm-5.smt \ + regress3/bmc-ibm-7.smt \ + regress3/eq_diamond14.smt \ + regress3/friedman_n6_i4.smt \ + regress3/hole9.cvc \ + regress3/incorrect1.smt \ + regress3/incorrect2.smt \ + regress3/pp-regfile.smt \ + regress3/qwh.35.405.shuffled-as.sat03-1651.smt + +REG4_TESTS = \ + regress4/C880mul.miter.shuffled-as.sat03-348.smt \ + regress4/NEQ016_size5.smt \ + regress4/bug143.smt \ + regress4/comb2.shuffled-as.sat03-420.smt \ + regress4/hole10.cvc \ + regress4/instance_1151.smt + +# dejan: disabled these because it's mixed arithmetic and it doesn't go +# well when changing theoryof: +# - regress0/unconstrained/arith2.smt2 +# - regress0/unconstrained/arith7.smt2 +# +# lianah: disabled these as the unconstrained terms are no longer +# recognized after implementing the divide-by-zero semantics for bv division: +# - regress0/unconstrained/bvdiv.smt2, +# - regress0/unconstrained/bvconcat.smt2 +# +# Proof checking takes too long. Add this back. +# - regress0/bv/fuzz15.delta01.smt +# +# regress1/ho/hoa0102.smt2 results in an assertion failure (see issue #1650). +# +# ajreynol: disabled these since they give different error messages on +# production and debug: +# - regress1/quantifiers/macro-subtype-param.smt2 +# - regress1/quantifiers/subtype-param-unk.smt2 +# - regress1/quantifiers/subtype-param.smt2 +# +# issue1048-arrays-int-real.smt2 -- different errors on debug and production. +# +# regress0/aufbv/bug348 does not seem to terminate with proofs +DISABLED_TESTS = \ + regress0/arith/bug549.cvc \ + regress0/arith/incorrect1.smt \ + regress0/arith/integers/arith-int-014.cvc \ + regress0/arith/integers/arith-int-015.cvc \ + regress0/arith/integers/arith-int-021.cvc \ + regress0/arith/integers/arith-int-023.cvc \ + regress0/arith/integers/arith-int-025.cvc \ + regress0/arith/integers/arith-int-079.cvc \ + regress0/arith/integers/arith-interval.cvc \ + regress0/arith/miplib-opt1217--27.smt \ + regress0/arith/miplib-pp08a-3000.smt \ + regress0/arr1.smt \ + regress0/arr1.smt2 \ + regress0/arr2.smt \ + regress0/aufbv/bug348.smt \ + regress0/aufbv/bug349.smt \ + regress0/aufbv/bug493.smt \ + regress0/aufbv/dubreva005ue.smt \ + regress0/aufbv/fifo32bc06k08.smt \ + regress0/aufbv/fifo32in06k08.delta01.smt \ + regress0/aufbv/fifo32in06k08.smt \ + regress0/aufbv/no_init_multi_delete14.smt \ + regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.smt \ + regress0/aufbv/wchains010ue.smt \ + regress0/auflia/fuzz01.smt \ + regress0/bug2.smt \ + regress0/bug374.delta01.smt \ + regress0/bug374.smt \ + regress0/bv/bug345.smt \ + regress0/bv/bvcomp.cvc \ + regress0/bv/bvsmod.smt2 \ + regress0/bv/core/bitvec0.delta01.smt \ + regress0/bv/core/bitvec1.smt \ + regress0/bv/core/bitvec3.smt \ + regress0/bv/core/bv_eq_diamond11.smt \ + regress0/bv/core/bv_eq_diamond12.smt \ + regress0/bv/core/bv_eq_diamond13.smt \ + regress0/bv/core/bv_eq_diamond14.smt \ + regress0/bv/core/bv_eq_diamond15.smt \ + regress0/bv/core/bv_eq_diamond16.smt \ + regress0/bv/core/bv_eq_diamond17.smt \ + regress0/bv/core/concat-merge-0.cvc \ + regress0/bv/core/concat-merge-1.cvc \ + regress0/bv/core/concat-merge-2.cvc \ + regress0/bv/core/concat-merge-3.cvc \ + regress0/bv/core/constant_core.smt2 \ + regress0/bv/core/equality-00.cvc \ + regress0/bv/core/equality-01.cvc \ + regress0/bv/core/equality-02.cvc \ + regress0/bv/core/equality-03.cvc \ + regress0/bv/core/equality-03.smt \ + regress0/bv/core/equality-04.smt \ + regress0/bv/core/equality-05.smt \ + regress0/bv/core/ext_con_004_001_1024.smt \ + regress0/bv/core/extract-concat-0.cvc \ + regress0/bv/core/extract-concat-1.cvc \ + regress0/bv/core/extract-concat-10.cvc \ + regress0/bv/core/extract-concat-11.cvc \ + regress0/bv/core/extract-concat-2.cvc \ + regress0/bv/core/extract-concat-3.cvc \ + regress0/bv/core/extract-concat-4.cvc \ + regress0/bv/core/extract-concat-5.cvc \ + regress0/bv/core/extract-concat-6.cvc \ + regress0/bv/core/extract-concat-7.cvc \ + regress0/bv/core/extract-concat-8.cvc \ + regress0/bv/core/extract-concat-9.cvc \ + regress0/bv/core/extract-constant.cvc \ + regress0/bv/core/extract-extract-0.cvc \ + regress0/bv/core/extract-extract-1.cvc \ + regress0/bv/core/extract-extract-10.cvc \ + regress0/bv/core/extract-extract-11.cvc \ + regress0/bv/core/extract-extract-2.cvc \ + regress0/bv/core/extract-extract-3.cvc \ + regress0/bv/core/extract-extract-4.cvc \ + regress0/bv/core/extract-extract-5.cvc \ + regress0/bv/core/extract-extract-6.cvc \ + regress0/bv/core/extract-extract-7.cvc \ + regress0/bv/core/extract-extract-8.cvc \ + regress0/bv/core/extract-extract-9.cvc \ + regress0/bv/core/extract-whole-0.cvc \ + regress0/bv/core/extract-whole-1.cvc \ + regress0/bv/core/extract-whole-2.cvc \ + regress0/bv/core/extract-whole-3.cvc \ + regress0/bv/core/extract-whole-4.cvc \ + regress0/bv/core/incremental.smt \ + regress0/bv/core/slice-01.cvc \ + regress0/bv/core/slice-02.cvc \ + regress0/bv/core/slice-03.cvc \ + regress0/bv/core/slice-04.cvc \ + regress0/bv/core/slice-05.cvc \ + regress0/bv/core/slice-06.cvc \ + regress0/bv/core/slice-07.cvc \ + regress0/bv/core/slice-08.cvc \ + regress0/bv/core/slice-09.cvc \ + regress0/bv/core/slice-10.cvc \ + regress0/bv/core/slice-11.cvc \ + regress0/bv/core/slice-12.cvc \ + regress0/bv/core/slice-13.cvc \ + regress0/bv/core/slice-14.cvc \ + regress0/bv/core/slice-15.cvc \ + regress0/bv/core/slice-16.cvc \ + regress0/bv/core/slice-17.cvc \ + regress0/bv/core/slice-18.cvc \ + regress0/bv/core/slice-19.cvc \ + regress0/bv/core/slice-20.cvc \ + regress0/bv/fuzz07-delta.smt \ + regress0/bv/fuzz15.delta01.smt \ + regress0/bv/fuzz15.smt \ + regress0/bv/fuzz16.smt \ + regress0/bv/fuzz17.smt \ + regress0/bv/incorrect1.delta01.smt \ + regress0/bv/incorrect1.smt \ + regress0/bv/inequality00.smt2 \ + regress0/bv/inequality01.smt2 \ + regress0/bv/inequality02.smt2 \ + regress0/bv/inequality03.smt2 \ + regress0/bv/inequality04.smt2 \ + regress0/bv/inequality05.smt2 \ + regress0/bv/test00.smt \ + regress0/cvc3-bug15.cvc \ + regress0/decision/uflia-xs-09-16-3-4-1-5.smt \ + regress0/decision/wchains010ue.smt \ + regress0/incorrect1.smt \ + regress0/ite.smt2 \ + regress0/ite_arith.smt2 \ + regress0/lemmas/fischer3-mutex-16.smt \ + regress0/nl/all-logic.smt2 \ + regress0/quantifiers/qbv-multi-lit-uge.smt2 \ + regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 \ + regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 \ + regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 \ + regress0/rewriterules/datatypes_clark.smt2 \ + regress0/rewriterules/length.smt2 \ + regress0/rewriterules/length_gen_n.smt2 \ + regress0/rewriterules/length_gen_n_lemma.smt2 \ + regress0/rewriterules/length_trick2.smt2 \ + regress0/rewriterules/native_datatypes.smt2 \ + regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 \ + regress0/sets/setel-eq.smt2 \ + regress0/sets/sets-new.smt2 \ + regress0/sets/sets-testlemma-ints.smt2 \ + regress0/sets/sets-testlemma-reals.smt2 \ + regress0/symmetric.smt \ + regress0/tptp/BOO003-4.p \ + regress0/tptp/BOO027-1.p \ + regress0/tptp/MGT031-1.p \ + regress0/tptp/NLP114-1.p \ + regress0/tptp/SYN075+1.p \ + regress0/uf/PEQ018_size4.smt \ + regress0/uf/SEQ032_size2.smt \ + regress0/uf/iso_icl_repgen004.smt \ + regress0/uflia/diseqprop.01.smt \ + regress0/uflia/diseqprop.02.smt \ + regress0/uflia/diseqprop.03.smt \ + regress0/uflia/diseqprop.04.smt \ + regress0/uflia/diseqprop.05.smt \ + regress0/uflia/diseqprop.06.smt \ + regress0/uflia/xs-09-16-3-4-1-5.delta05.smt \ + regress0/uflra/pb_real_10_0200_10_25.smt \ + regress0/uflra/pb_real_10_0200_10_27.smt \ + regress0/unconstrained/arith2.smt2 \ + regress0/unconstrained/arith7.smt2 \ + regress0/unconstrained/bvconcat.smt2 \ + regress0/unconstrained/bvdiv.smt \ + regress1/arith/arith-int-001.cvc \ + regress1/arith/arith-int-002.cvc \ + regress1/arith/arith-int-003.cvc \ + regress1/arith/arith-int-005.cvc \ + regress1/arith/arith-int-006.cvc \ + regress1/arith/arith-int-007.cvc \ + regress1/arith/arith-int-008.cvc \ + regress1/arith/arith-int-009.cvc \ + regress1/arith/arith-int-010.cvc \ + regress1/arith/arith-int-016.cvc \ + regress1/arith/arith-int-017.cvc \ + regress1/arith/arith-int-018.cvc \ + regress1/arith/arith-int-019.cvc \ + regress1/arith/arith-int-020.cvc \ + regress1/arith/arith-int-026.cvc \ + regress1/arith/arith-int-027.cvc \ + regress1/arith/arith-int-028.cvc \ + regress1/arith/arith-int-029.cvc \ + regress1/arith/arith-int-030.cvc \ + regress1/arith/arith-int-031.cvc \ + regress1/arith/arith-int-032.cvc \ + regress1/arith/arith-int-033.cvc \ + regress1/arith/arith-int-034.cvc \ + regress1/arith/arith-int-035.cvc \ + regress1/arith/arith-int-036.cvc \ + regress1/arith/arith-int-037.cvc \ + regress1/arith/arith-int-038.cvc \ + regress1/arith/arith-int-039.cvc \ + regress1/arith/arith-int-040.cvc \ + regress1/arith/arith-int-041.cvc \ + regress1/arith/arith-int-043.cvc \ + regress1/arith/arith-int-044.cvc \ + regress1/arith/arith-int-045.cvc \ + regress1/arith/arith-int-046.cvc \ + regress1/arith/arith-int-049.cvc \ + regress1/arith/arith-int-051.cvc \ + regress1/arith/arith-int-052.cvc \ + regress1/arith/arith-int-053.cvc \ + regress1/arith/arith-int-054.cvc \ + regress1/arith/arith-int-055.cvc \ + regress1/arith/arith-int-056.cvc \ + regress1/arith/arith-int-057.cvc \ + regress1/arith/arith-int-058.cvc \ + regress1/arith/arith-int-059.cvc \ + regress1/arith/arith-int-060.cvc \ + regress1/arith/arith-int-061.cvc \ + regress1/arith/arith-int-062.cvc \ + regress1/arith/arith-int-063.cvc \ + regress1/arith/arith-int-064.cvc \ + regress1/arith/arith-int-065.cvc \ + regress1/arith/arith-int-066.cvc \ + regress1/arith/arith-int-067.cvc \ + regress1/arith/arith-int-068.cvc \ + regress1/arith/arith-int-069.cvc \ + regress1/arith/arith-int-070.cvc \ + regress1/arith/arith-int-071.cvc \ + regress1/arith/arith-int-072.cvc \ + regress1/arith/arith-int-073.cvc \ + regress1/arith/arith-int-074.cvc \ + regress1/arith/arith-int-075.cvc \ + regress1/arith/arith-int-076.cvc \ + regress1/arith/arith-int-077.cvc \ + regress1/arith/arith-int-078.cvc \ + regress1/arith/arith-int-080.cvc \ + regress1/arith/arith-int-081.cvc \ + regress1/arith/arith-int-082.cvc \ + regress1/arith/arith-int-083.cvc \ + regress1/arith/arith-int-086.cvc \ + regress1/arith/arith-int-087.cvc \ + regress1/arith/arith-int-088.cvc \ + regress1/arith/arith-int-089.cvc \ + regress1/arith/arith-int-090.cvc \ + regress1/arith/arith-int-091.cvc \ + regress1/arith/arith-int-092.cvc \ + regress1/arith/arith-int-093.cvc \ + regress1/arith/arith-int-094.cvc \ + regress1/arith/arith-int-095.cvc \ + regress1/arith/arith-int-096.cvc \ + regress1/arith/arith-int-099.cvc \ + regress1/arith/arith-int-100.cvc \ + regress1/auflia/bug337.smt2 \ + regress1/bug472.smt2 \ + regress1/bug585.cvc \ + regress1/bug590.smt2 \ + regress1/bv/bench_38.delta.smt2 \ + regress1/crash_burn_locusts.smt2 \ + regress1/ho/hoa0102.smt2 \ + regress1/issue1048-arrays-int-real.smt2 \ + regress1/quantifiers/macro-subtype-param.smt2 \ + regress1/quantifiers/subtype-param-unk.smt2 \ + regress1/quantifiers/subtype-param.smt2 \ + regress1/rels/garbage_collect.cvc \ + regress1/rewriterules/datatypes2.smt2 \ + regress1/rewriterules/datatypes3.smt2 \ + regress1/rewriterules/datatypes_clark_quantification.smt2 \ + regress1/rewriterules/length_gen_010.smt2 \ + regress1/rewriterules/length_gen_010_lemma.smt2 \ + regress1/rewriterules/length_gen_080.smt2 \ + regress1/rewriterules/length_gen_160_lemma.smt2 \ + regress1/rewriterules/length_gen_inv_160.smt2 \ + regress1/rewriterules/length_trick3.smt2 \ + regress1/rewriterules/length_trick3_int.smt2 \ + regress1/rewriterules/set_A_new_fast_tableau-base.smt2 \ + regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 \ + regress1/rewriterules/test_guards.smt2 \ + regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 \ + regress1/sets/setofsets-disequal.smt2 \ + regress1/simple-rdl-definefun.smt2 \ + regress1/sygus/Base16_1.sy \ + regress1/sygus/enum-test.sy \ + regress1/sygus/inv_gen_fig8.sy \ + regress2/arith/arith-int-098.cvc \ + regress2/arith/miplib-opt1217--27.smt2 \ + regress2/arith/miplib-pp08a-3000.smt2 \ + regress2/bug396.smt2 \ + regress2/nl/dumortier-050317.smt2 \ + regress2/nl/nt-lemmas-bad.smt2 \ + regress2/quantifiers/small-bug1-fixpoint-3.smt2 \ + regress2/xs-11-20-5-2-5-3.smt \ + regress2/xs-11-20-5-2-5-3.smt2 + +TESTS_EXPECT = \ + regress0/arith/miplib-opt1217--27.smt.expect \ + regress0/arith/miplib-pp08a-3000.smt.expect \ + regress0/decision/aufbv-fuzz01.smt.expect \ + regress0/decision/bitvec0.delta01.smt.expect \ + regress0/decision/bitvec0.smt.expect \ + regress0/decision/bitvec5.smt.expect \ + regress0/decision/bug347.smt.expect \ + regress0/decision/bug374a.smt.expect \ + regress0/decision/bug374b.smt2.expect \ + regress0/decision/just_sat.expect \ + regress0/decision/just_unsat.expect \ + regress0/decision/pp-regfile.delta01.smt.expect \ + regress0/decision/pp-regfile.delta02.smt.expect \ + regress0/decision/quant-ex1.smt2.expect \ + regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt.expect \ + regress0/decision/uflia-xs-09-16-3-4-1-5.smt.expect \ + regress0/decision/wchains010ue.delta02.smt.expect \ + regress0/decision/wchains010ue.smt.expect \ + regress0/expect/scrub.01.smt.expect \ + regress0/expect/scrub.03.smt2.expect \ + regress0/expect/scrub.07.sy.expect \ + regress0/quantifiers/bug291.smt2.expect \ + regress0/uflia/check02.smt2.expect \ + regress0/uflia/check03.smt2.expect \ + regress0/uflia/check04.smt2.expect \ + regress0/uflia/check04.smt2.expect \ + regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2.expect \ + regress0/uflia/tiny.smt2.expect \ + regress1/bug216.smt2.expect \ + regress1/bug590.smt2.expect \ + regress1/decision/quant-Arrays_Q1-noinfer.smt2.expect \ + regress1/decision/quant-symmetric_unsat_7.smt2.expect \ + regress1/push-pop/bug216.smt2.expect \ + regress1/simplification_bug4.smt2.expect \ + regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect \ + regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect \ + regress1/uflia/speed2_e8_449_e8_517.ec.smt2.expect \ + regress1/uflia/stalmark_e7_27_e7_31.ec.smt2.expect \ + regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect \ + regress2/uflia-error0.smt2.expect \ + regress2/xs-09-16-3-4-1-5.decn.smt.expect \ + regress3/pp-regfile.smt.expect 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: diff --git a/test/regress/regress1/Makefile b/test/regress/regress1/Makefile deleted file mode 100644 index b720980f1..000000000 --- a/test/regress/regress1/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../.. -srcdir = test/regress/regress1 - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am deleted file mode 100644 index af3f65370..000000000 --- a/test/regress/regress1/Makefile.am +++ /dev/null @@ -1,78 +0,0 @@ -SUBDIRS = . arith bv aufbv auflia datatypes rewriterules lemmas decision fmf ho nl push-pop quantifiers rels strings sets sygus sep uflia - -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -MAKEFLAGS = -k - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - bug425.cvc \ - bug519.smt2 \ - bug521.smt2 \ - bug694-Unapply1.scala-0.smt2 \ - fmf-fun-dbu.smt2 \ - bug296.smt2 \ - bug507.smt2 \ - gensys_brn001.smt2 \ - simplification_bug4.smt2 \ - trim.cvc \ - constarr3.cvc \ - constarr3.smt2 \ - parsing_ringer.cvc \ - arrayinuf_error.smt2 \ - boolean-terms-kernel2.smt2 \ - boolean.cvc \ - bug216.smt2 \ - bug512.smt2 \ - bug516.smt2 \ - bug520.smt2 \ - bug543.smt2 \ - bug567.smt2 \ - bug593.smt2 \ - bug681.smt2 \ - bug800.smt2 \ - bvdiv2.smt2 \ - error.cvc \ - errorcrash.smt2 \ - hole6.cvc \ - ite5.smt2 \ - non-fatal-errors.smt2 \ - proof00.smt2 \ - sqrt2-sort-inf-unk.smt2 \ - test12.cvc \ - uf2.smt2 - -EXTRA_DIST = $(TESTS) \ - simplification_bug4.smt2.expect \ - bug590.smt2.expect \ - bug216.smt2.expect \ - bug590.smt2 \ - bug585.cvc \ - crash_burn_locusts.smt2 \ - bug472.smt2 \ - simple-rdl-definefun.smt2 - -# issue1048-arrays-int-real.smt2 -- different errors on debug and production - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress1/arith/Makefile.am deleted file mode 100644 index e2b0e93d9..000000000 --- a/test/regress/regress1/arith/Makefile.am +++ /dev/null @@ -1,139 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - arith-int-004.cvc \ - arith-int-011.cvc \ - arith-int-048.cvc \ - arith-int-050.cvc \ - arith-int-084.cvc \ - arith-int-085.cvc \ - arith-int-097.cvc \ - bug716.0.smt2 \ - problem__003.smt2 \ - bug547.1.smt2 \ - bug716.1.cvc \ - div.03.smt2 \ - div.06.smt2 \ - div.08.smt2 \ - div.09.smt2 \ - miplib3.cvc \ - mod.02.smt2 \ - mod.03.smt2 \ - mult.02.smt2 \ - arith-int-012.cvc \ - arith-int-013.cvc \ - arith-int-022.cvc \ - arith-int-024.cvc \ - arith-int-047.cvc - -EXTRA_DIST = $(TESTS) \ - arith-int-008.cvc \ - arith-int-018.cvc \ - arith-int-020.cvc \ - arith-int-026.cvc \ - arith-int-029.cvc \ - arith-int-030.cvc \ - arith-int-043.cvc \ - arith-int-044.cvc \ - arith-int-049.cvc \ - arith-int-061.cvc \ - arith-int-062.cvc \ - arith-int-064.cvc \ - arith-int-065.cvc \ - arith-int-081.cvc \ - arith-int-083.cvc \ - arith-int-090.cvc \ - arith-int-091.cvc \ - arith-int-092.cvc \ - arith-int-094.cvc \ - arith-int-096.cvc \ - arith-int-098.cvc \ - arith-int-001.cvc \ - arith-int-002.cvc \ - arith-int-003.cvc \ - arith-int-005.cvc \ - arith-int-006.cvc \ - arith-int-009.cvc \ - arith-int-010.cvc \ - arith-int-016.cvc \ - arith-int-017.cvc \ - arith-int-019.cvc \ - arith-int-027.cvc \ - arith-int-028.cvc \ - arith-int-031.cvc \ - arith-int-032.cvc \ - arith-int-033.cvc \ - arith-int-034.cvc \ - arith-int-035.cvc \ - arith-int-036.cvc \ - arith-int-037.cvc \ - arith-int-038.cvc \ - arith-int-039.cvc \ - arith-int-040.cvc \ - arith-int-041.cvc \ - arith-int-045.cvc \ - arith-int-046.cvc \ - arith-int-051.cvc \ - arith-int-052.cvc \ - arith-int-053.cvc \ - arith-int-054.cvc \ - arith-int-055.cvc \ - arith-int-056.cvc \ - arith-int-057.cvc \ - arith-int-058.cvc \ - arith-int-059.cvc \ - arith-int-060.cvc \ - arith-int-063.cvc \ - arith-int-066.cvc \ - arith-int-067.cvc \ - arith-int-068.cvc \ - arith-int-069.cvc \ - arith-int-070.cvc \ - arith-int-071.cvc \ - arith-int-072.cvc \ - arith-int-073.cvc \ - arith-int-074.cvc \ - arith-int-075.cvc \ - arith-int-076.cvc \ - arith-int-077.cvc \ - arith-int-078.cvc \ - arith-int-080.cvc \ - arith-int-086.cvc \ - arith-int-087.cvc \ - arith-int-088.cvc \ - arith-int-089.cvc \ - arith-int-093.cvc \ - arith-int-095.cvc \ - arith-int-099.cvc \ - arith-int-100.cvc - -FAILING_TESTS = \ - arith-int-007.cvc \ - arith-int-082.cvc \ - arith-int-098.cvc - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/aufbv/Makefile b/test/regress/regress1/aufbv/Makefile deleted file mode 100644 index 197a840e1..000000000 --- a/test/regress/regress1/aufbv/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress1/aufbv - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress1/aufbv/Makefile.am b/test/regress/regress1/aufbv/Makefile.am deleted file mode 100644 index 019e7f23a..000000000 --- a/test/regress/regress1/aufbv/Makefile.am +++ /dev/null @@ -1,31 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - fuzz10.smt \ - bug580.smt2 - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/auflia/Makefile b/test/regress/regress1/auflia/Makefile deleted file mode 100644 index 46e7ebe17..000000000 --- a/test/regress/regress1/auflia/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress1/auflia - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress1/auflia/Makefile.am b/test/regress/regress1/auflia/Makefile.am deleted file mode 100644 index 25a0d89e0..000000000 --- a/test/regress/regress1/auflia/Makefile.am +++ /dev/null @@ -1,31 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - bug330.smt2 - -EXTRA_DIST = $(TESTS) \ - bug337.smt2 - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/bv/Makefile b/test/regress/regress1/bv/Makefile deleted file mode 100644 index 1ddea736f..000000000 --- a/test/regress/regress1/bv/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress1/bv - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress1/bv/Makefile.am b/test/regress/regress1/bv/Makefile.am deleted file mode 100644 index b144a0507..000000000 --- a/test/regress/regress1/bv/Makefile.am +++ /dev/null @@ -1,44 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - bv-proof00.smt \ - fuzz34.smt \ - fuzz38.smt \ - bug_extract_mult_leading_bit.smt2 \ - bug787.smt2 \ - bv-int-collapse2-sat.smt2 \ - cmu-rdk-3.smt2 \ - decision-weight00.smt2 \ - divtest.smt2 \ - bv2nat-ground.smt2 \ - bv2nat-simp-range-sat.smt2 \ - unsound1.smt2 - -EXTRA_DIST = $(TESTS) - -# This benchmark is currently disabled as it uses --check-proof -# bench_38.delta.smt2 - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/datatypes/Makefile b/test/regress/regress1/datatypes/Makefile deleted file mode 100644 index 1e40da253..000000000 --- a/test/regress/regress1/datatypes/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress1/datatypes - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress1/datatypes/Makefile.am b/test/regress/regress1/datatypes/Makefile.am deleted file mode 100644 index 036b8df00..000000000 --- a/test/regress/regress1/datatypes/Makefile.am +++ /dev/null @@ -1,34 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - manos-model.smt2 \ - acyclicity-sr-ground096.smt2 \ - dt-color-2.6.smt2 \ - dt-param-card4-unsat.smt2 \ - error.cvc - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/decision/Makefile b/test/regress/regress1/decision/Makefile deleted file mode 100644 index 92798c450..000000000 --- a/test/regress/regress1/decision/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress1/decision - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress1/decision/Makefile.am b/test/regress/regress1/decision/Makefile.am deleted file mode 100644 index 102c99e01..000000000 --- a/test/regress/regress1/decision/Makefile.am +++ /dev/null @@ -1,34 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - error3.smt \ - quant-symmetric_unsat_7.smt2 \ - quant-Arrays_Q1-noinfer.smt2 - -EXTRA_DIST = $(TESTS) \ - quant-symmetric_unsat_7.smt2.expect \ - quant-Arrays_Q1-noinfer.smt2.expect - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/fmf/Makefile b/test/regress/regress1/fmf/Makefile deleted file mode 100644 index 400ad9d0d..000000000 --- a/test/regress/regress1/fmf/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress1/fmf - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress1/fmf/Makefile.am b/test/regress/regress1/fmf/Makefile.am deleted file mode 100644 index dc07f6ca4..000000000 --- a/test/regress/regress1/fmf/Makefile.am +++ /dev/null @@ -1,68 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - agree466.smt2 \ - ALG008-1.smt2 \ - bug0909.smt2 \ - bug764.smt2 \ - datatypes-ufinite.smt2 \ - datatypes-ufinite-nested.smt2 \ - fc-pigeonhole19.smt2 \ - fib-core.smt2 \ - fmf-bound-2dim.smt2 \ - fmf-fun-no-elim-ext-arith2.smt2 \ - fmf-strange-bounds.smt2 \ - issue916-fmf-or.smt2 \ - jasmin-cdt-crash.smt2 \ - LeftistHeap.scala-8-ncm.smt2 \ - lst-no-self-rev-exp.smt2 \ - nun-0208-to.smt2 \ - pow2-bool.smt2 \ - with-ind-104-core.smt2 \ - agree467.smt2 \ - alg202+1.smt2 \ - am-bad-model.cvc \ - bound-int-alt.smt2 \ - bug651.smt2 \ - bug723-irrelevant-funs.smt2 \ - cons-sets-bounds.smt2 \ - constr-ground-to.smt2 \ - dt-proper-model.smt2 \ - fmf-bound-int.smt2 \ - fmf-fun-no-elim-ext-arith.smt2 \ - forall_unit_data.smt2 \ - fore19-exp2-core.smt2 \ - german169.smt2 \ - german73.smt2 \ - ko-bound-set.cvc \ - loopy_coda.smt2 \ - memory_model-R_cpp-dd.cvc \ - PUZ001+1.smt2 \ - refcount24.cvc.smt2 \ - sc-crash-052316.smt2 - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/ho/Makefile.am b/test/regress/regress1/ho/Makefile.am deleted file mode 100644 index 6ae3a116f..000000000 --- a/test/regress/regress1/ho/Makefile.am +++ /dev/null @@ -1,35 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - auth0068.smt2 \ - fta0409.smt2 \ - ho-exponential-model.smt2 \ - ho-matching-enum-2.smt2 \ - ho-std-fmf.smt2 - -EXTRA_DIST = $(TESTS) \ - hoa0102.smt2 - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/lemmas/Makefile b/test/regress/regress1/lemmas/Makefile deleted file mode 100644 index 46d254aef..000000000 --- a/test/regress/regress1/lemmas/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress1/lemmas - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress1/lemmas/Makefile.am b/test/regress/regress1/lemmas/Makefile.am deleted file mode 100644 index d22553d64..000000000 --- a/test/regress/regress1/lemmas/Makefile.am +++ /dev/null @@ -1,32 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - clocksynchro_5clocks.main_invar.base.smt \ - pursuit-safety-8.smt \ - simple_startup_9nodes.abstract.base.smt - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/nl/Makefile.am b/test/regress/regress1/nl/Makefile.am deleted file mode 100644 index a008e4df1..000000000 --- a/test/regress/regress1/nl/Makefile.am +++ /dev/null @@ -1,78 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - mirko-050417.smt2 \ - arrowsmith-050317.smt2 \ - bug698.smt2 \ - dist-big.smt2 \ - dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 \ - exp-4.5-lt.smt2 \ - metitarski_3_4_2e.smt2 \ - metitarski-3-4.smt2 \ - nl-help-unsat-quant.smt2 \ - poly-1025.smt2 \ - quant-nl.smt2 \ - red-exp.smt2 \ - rewriting-sums.smt2 \ - simple-mono.smt2 \ - sin1-sat.smt2 \ - sin-compare.smt2 \ - sin-compare-across-phase.smt2 \ - sqrt-problem-1.smt2 \ - sugar-ident-2.smt2 \ - sugar-ident-3.smt2 \ - tan-rewrite2.smt2 \ - bad-050217.smt2 \ - coeff-unsat-base.smt2 \ - coeff-unsat.smt2 \ - combine.smt2 \ - cos-bound.smt2 \ - cos1-tc.smt2 \ - disj-eval.smt2 \ - div-mod-partial.smt2 \ - exp_monotone.smt2 \ - exp1-lb.smt2 \ - metitarski-1025.smt2 \ - NAVIGATION2.smt2 \ - nl-unk-quant.smt2 \ - ones.smt2 \ - shifting.smt2 \ - shifting2.smt2 \ - simple-mono-unsat.smt2 \ - sin-init-tangents.smt2 \ - sin-sign.smt2 \ - sin-sym2.smt2 \ - sin1-lb.smt2 \ - sin1-ub.smt2 \ - sin2-lb.smt2 \ - sin2-ub.smt2 \ - sugar-ident.smt2 \ - zero-subset.smt2 \ - sin1-deq-sat.smt2 \ - nl-eq-infer.smt2 - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/push-pop/Makefile.am b/test/regress/regress1/push-pop/Makefile.am deleted file mode 100644 index d1fe52984..000000000 --- a/test/regress/regress1/push-pop/Makefile.am +++ /dev/null @@ -1,92 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - arith_lra_01.smt2 \ - arith_lra_02.smt2 \ - bug-fmf-fun-skolem.smt2 \ - bug216.smt2 \ - bug326.smt2 \ - fuzz_1_to_52_merged.smt2 \ - fuzz_1.smt2 \ - fuzz_10.smt2 \ - fuzz_11.smt2 \ - fuzz_15.smt2 \ - fuzz_16.smt2 \ - fuzz_19.smt2 \ - fuzz_20.smt2 \ - fuzz_23.smt2 \ - fuzz_24.smt2 \ - fuzz_25.smt2 \ - fuzz_26.smt2 \ - fuzz_28.smt2 \ - fuzz_29.smt2 \ - fuzz_3_1.smt2 \ - fuzz_3_10.smt2 \ - fuzz_3_11.smt2 \ - fuzz_3_12.smt2 \ - fuzz_3_13.smt2 \ - fuzz_3_14.smt2 \ - fuzz_3_15.smt2 \ - fuzz_3_2.smt2 \ - fuzz_3_3.smt2 \ - fuzz_3_4.smt2 \ - fuzz_3_5.smt2 \ - fuzz_3_6.smt2 \ - fuzz_3_7.smt2 \ - fuzz_3_8.smt2 \ - fuzz_3_9.smt2 \ - fuzz_30.smt2 \ - fuzz_32.smt2 \ - fuzz_34.smt2 \ - fuzz_35.smt2 \ - fuzz_37.smt2 \ - fuzz_39.smt2 \ - fuzz_4.smt2 \ - fuzz_40.smt2 \ - fuzz_41.smt2 \ - fuzz_42.smt2 \ - fuzz_43.smt2 \ - fuzz_44.smt2 \ - fuzz_45.smt2 \ - fuzz_5_1.smt2 \ - fuzz_5_2.smt2 \ - fuzz_5_3.smt2 \ - fuzz_5_4.smt2 \ - fuzz_5_5.smt2 \ - fuzz_5_6.smt2 \ - fuzz_5.smt2 \ - fuzz_51.smt2 \ - fuzz_52.smt2 \ - fuzz_6.smt2 \ - fuzz_7.smt2 \ - fuzz_8.smt2 \ - fuzz_9.smt2 \ - quant-fun-proc-unmacro.smt2 \ - quant-fun-proc.smt2 - -EXTRA_DIST = $(TESTS) \ - bug216.smt2.expect - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/quantifiers/Makefile b/test/regress/regress1/quantifiers/Makefile deleted file mode 100644 index fcd888f99..000000000 --- a/test/regress/regress1/quantifiers/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress1/quantifiers - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress1/quantifiers/Makefile.am b/test/regress/regress1/quantifiers/Makefile.am deleted file mode 100644 index af277af90..000000000 --- a/test/regress/regress1/quantifiers/Makefile.am +++ /dev/null @@ -1,103 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - bug802.smt2 \ - 006-cbqi-ite.smt2 \ - AdditiveMethods_OwnedResults.Mz.smt2 \ - ari118-bv-2occ-x.smt2 \ - array-unsat-simp3.smt2 \ - bignum_quant.smt2 \ - bug_743.smt2 \ - bug822.smt2 \ - cdt-0208-to.smt2 \ - gauss_init_0030.fof.smt2 \ - inst-max-level-segf.smt2 \ - intersection-example-onelane.proof-node22337.smt2 \ - javafe.ast.StmtVec.009.smt2 \ - model_6_1_bv.smt2 \ - nested9_true-unreach-call.i_575.smt2 \ - NUM878.smt2 \ - opisavailable-12.smt2 \ - psyco-107-bv.smt2 \ - psyco-196.smt2 \ - qbv-simple-2vars-vo.smt2 \ - qbv-test-invert-bvcomp.smt2 \ - qbv-test-invert-bvudiv-0.smt2 \ - qbv-test-invert-bvudiv-1.smt2 \ - qbv-test-invert-bvurem-1.smt2 \ - qcft-javafe.filespace.TreeWalker.006.smt2 \ - qcft-smtlib3dbc51.smt2 \ - quaternion_ds1_symm_0428.fof.smt2 \ - rew-to-0211-dd.smt2 \ - ricart-agrawala6.smt2 \ - RND_4_16.smt2 \ - small-pipeline-fixpoint-3.smt2 \ - smtlib384a03.smt2 \ - smtlib46f14a.smt2 \ - smtlibf957ea.smt2 \ - stream-x2014-09-18-unsat.smt2 \ - symmetric_unsat_7.smt2 \ - anti-sk-simp.smt2 \ - Arrays_Q1-noinfer.smt2 \ - bi-artm-s.smt2 \ - burns13.smt2 \ - burns4.smt2 \ - cbqi-sdlx-fixpoint-3-dd.smt2 \ - ext-ex-deq-trigger.smt2 \ - extract-nproc.smt2 \ - florian-case-ax.smt2 \ - is-even.smt2 \ - mix-coeff.smt2 \ - parametric-lists.smt2 \ - psyco-001-bv.smt2 \ - qbv-disequality3.smt2 \ - qbv-test-invert-bvashr-0.smt2 \ - qbv-test-invert-bvashr-1.smt2 \ - qbv-test-invert-bvlshr-1.smt2 \ - qbv-test-invert-bvmul-neq.smt2 \ - qbv-test-invert-bvmul.smt2 \ - qbv-test-invert-bvudiv-0-neq.smt2 \ - qbv-test-invert-bvudiv-1-neq.smt2 \ - qbv-test-invert-bvurem-1-neq.smt2 \ - qbv-test-urem-rewrite.smt2 \ - RND-small.smt2 \ - RNDPRE_4_1-dd-nqe.smt2 \ - set8.smt2 \ - z3.620661-no-fv-trigger.smt2 \ - arith-rec-fun.smt2 \ - set3.smt2 - -# removed because they take more than 20s -# javafe.ast.ArrayInit.35.smt2 - -# FIXME: I've disabled these since they give different error messages on production and debug -# macro-subtype-param.smt2 -# subtype-param-unk.smt2 -# subtype-param.smt2 - -EXTRA_DIST = $(TESTS) \ - set3.smt2 - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/rels/Makefile.am b/test/regress/regress1/rels/Makefile.am deleted file mode 100644 index c35ea2914..000000000 --- a/test/regress/regress1/rels/Makefile.am +++ /dev/null @@ -1,66 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - bv1p.cvc \ - rel_pressure_0.cvc \ - rel_tc_5_1.cvc \ - set-strat.cvc \ - addr_book_1_1.cvc \ - addr_book_1.cvc \ - bv1-unit.cvc \ - bv1-unitb.cvc \ - bv1.cvc \ - bv1p-sat.cvc \ - bv2.cvc \ - iden_1_1.cvc \ - join-eq-structure_0_1.cvc \ - join-eq-structure-and.cvc \ - join-eq-structure.cvc \ - joinImg_0_1.cvc \ - joinImg_0_2.cvc \ - joinImg_1_1.cvc \ - joinImg_1.cvc \ - joinImg_2_1.cvc \ - joinImg_2.cvc \ - prod-mod-eq.cvc \ - prod-mod-eq2.cvc \ - rel_complex_3.cvc \ - rel_complex_4.cvc \ - rel_complex_5.cvc \ - rel_mix_0_1.cvc \ - rel_tc_10_1.cvc \ - rel_tc_4_1.cvc \ - rel_tc_4.cvc \ - rel_tc_6.cvc \ - rel_tc_9_1.cvc \ - rel_tp_2.cvc \ - rel_tp_join_2_1.cvc \ - strat_0_1.cvc \ - strat.cvc - -EXTRA_DIST = $(TESTS) \ - garbage_collect.cvc - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/rewriterules/Makefile b/test/regress/regress1/rewriterules/Makefile deleted file mode 100644 index 0eb938072..000000000 --- a/test/regress/regress1/rewriterules/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress1/rewriterules - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress1/rewriterules/Makefile.am b/test/regress/regress1/rewriterules/Makefile.am deleted file mode 100644 index 6c5ce19fb..000000000 --- a/test/regress/regress1/rewriterules/Makefile.am +++ /dev/null @@ -1,55 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -MAKEFLAGS = -k - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - reachability_back_to_the_future.smt2 \ - read5.smt2 \ - length_gen.smt2 \ - length_gen_020.smt2 \ - length_gen_020_sat.smt2 \ - length_gen_040.smt2 \ - length_gen_040_lemma.smt2 \ - length_gen_040_lemma_trigger.smt2 \ - datatypes_sat.smt2 - - -EXTRA_DIST = $(TESTS) \ - datatypes_clark_quantification.smt2 \ - datatypes2.smt2 \ - datatypes3.smt2 \ - length_gen_010_lemma.smt2 \ - length_gen_010.smt2 \ - length_gen_080.smt2 \ - length_gen_160_lemma.smt2 \ - length_gen_inv_160.smt2 \ - length_trick3_int.smt2 \ - length_trick3.smt2 \ - set_A_new_fast_tableau-base_sat.smt2 \ - set_A_new_fast_tableau-base.smt2 \ - test_guards.smt2 \ - why3_vstte10_max_sum_harness2.smt2 - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/sep/Makefile b/test/regress/regress1/sep/Makefile deleted file mode 100644 index 5733b5526..000000000 --- a/test/regress/regress1/sep/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress1/sep - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress1/sep/Makefile.am b/test/regress/regress1/sep/Makefile.am deleted file mode 100644 index bda7e4484..000000000 --- a/test/regress/regress1/sep/Makefile.am +++ /dev/null @@ -1,60 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - loop-1220.smt2 \ - sep-simp-unc.smt2 \ - split-find-unsat.smt2 \ - split-find-unsat-w-emp.smt2 \ - dispose-list-4-init.smt2 \ - finite-witness-sat.smt2 \ - sep-find2.smt2 \ - sep-fmf-priority.smt2 \ - sep-neg-1refine.smt2 \ - sep-nterm-again.smt2 \ - chain-int.smt2 \ - crash1220.smt2 \ - emp2-quant-unsat.smt2 \ - fmf-nemp-2.smt2 \ - pto-04.smt2 \ - quant_wand.smt2 \ - sep-02.smt2 \ - sep-03.smt2 \ - sep-neg-nstrict.smt2 \ - sep-neg-nstrict2.smt2 \ - sep-neg-simple.smt2 \ - sep-neg-swap.smt2 \ - sep-nterm-val-model.smt2 \ - simple-neg-sat.smt2 \ - wand-0526-sat.smt2 \ - wand-false.smt2 \ - wand-nterm-simp.smt2 \ - wand-nterm-simp2.smt2 \ - wand-simp-sat.smt2 \ - wand-simp-sat2.smt2 \ - wand-simp-unsat.smt2 - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/sets/Makefile b/test/regress/regress1/sets/Makefile deleted file mode 100644 index e78e958ad..000000000 --- a/test/regress/regress1/sets/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress1/sets - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress1/sets/Makefile.am b/test/regress/regress1/sets/Makefile.am deleted file mode 100644 index f52ab44e7..000000000 --- a/test/regress/regress1/sets/Makefile.am +++ /dev/null @@ -1,56 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - sets-disequal.smt2 \ - card-vc6-minimized.smt2 \ - card-4.smt2 \ - fuzz15201.smt2 \ - insert_invariant_37_2.smt2 \ - remove_check_free_31_6.smt2 \ - TalkingAboutSets.hs.fqout.cvc4.3577.smt2 \ - arjun-set-univ.cvc \ - card-3.smt2 \ - card-5.smt2 \ - card-6.smt2 \ - card-7.smt2 \ - copy_check_heap_access_33_4.smt2 \ - deepmeas0.hs.fqout.cvc4.41.smt2 \ - fuzz14418.smt2 \ - fuzz31811.smt2 \ - lemmabug-ListElts317minimized.smt2 \ - ListElem.hs.fqout.cvc4.38.smt2 \ - ListElts.hs.fqout.cvc4.317.smt2 \ - sets-tuple-poly.cvc \ - sharingbug.smt2 \ - UniqueZipper.hs.1030minimized.cvc4.smt2 \ - UniqueZipper.hs.1030minimized2.cvc4.smt2 \ - UniqueZipper.hs.fqout.cvc4.10.smt2 \ - UniqueZipper.hs.fqout.cvc4.1832.smt2 \ - univ-set-uf-elim.smt2 - -EXTRA_DIST = $(TESTS) \ - setofsets-disequal.smt2 - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/strings/Makefile b/test/regress/regress1/strings/Makefile deleted file mode 100644 index b4a9df5b2..000000000 --- a/test/regress/regress1/strings/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress1/strings - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress1/strings/Makefile.am b/test/regress/regress1/strings/Makefile.am deleted file mode 100644 index 7e9242e73..000000000 --- a/test/regress/regress1/strings/Makefile.am +++ /dev/null @@ -1,87 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - cmu-5042-0707-2.smt2 \ - artemis-0512-nonterm.smt2 \ - bug615.smt2 \ - bug682.smt2 \ - bug686dd.smt2 \ - bug768.smt2 \ - bug799-min.smt2 \ - chapman150408.smt2 \ - cmu-inc-nlpp-071516.smt2 \ - cmu-substr-rw.smt2 \ - crash-1019.smt2 \ - csp-prefix-exp-bug.smt2 \ - fmf001.smt2 \ - fmf002.smt2 \ - idof-nconst-index.smt2 \ - kaluza-fl.smt2 \ - loop007.smt2 \ - loop008.smt2 \ - loop009.smt2 \ - nf-ff-contains-abs.smt2 \ - norn-360.smt2 \ - norn-ab.smt2 \ - norn-nel-bug-052116.smt2 \ - pierre150331.smt2 \ - regexp001.smt2 \ - regexp002.smt2 \ - reloop.smt2 \ - str006.smt2 \ - strings-index-empty.smt2 \ - strip-endpt-sound.smt2 \ - substr001.smt2 \ - type002.smt2 \ - type003.smt2 \ - username_checker_min.smt2 \ - at001.smt2 \ - cmu-2db2-extf-reg.smt2 \ - gm-inc-071516-2.smt2 \ - idof-handg.smt2 \ - idof-neg-index.smt2 \ - idof-triv.smt2 \ - ilc-l-nt.smt2 \ - issue1105.smt2 \ - loop002.smt2 \ - loop003.smt2 \ - loop004.smt2 \ - loop005.smt2 \ - loop006.smt2 \ - norn-simp-rew-sat.smt2 \ - regexp003.smt2 \ - repl-empty-sem.smt2 \ - repl-soundness-sem.smt2 \ - str001.smt2 \ - str002.smt2 \ - str007.smt2 \ - rew-020618.smt2 \ - double-replace.smt2 \ - string-unsound-sem.smt2 \ - goodAI.smt2 - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/sygus/Makefile b/test/regress/regress1/sygus/Makefile deleted file mode 100644 index c8dc4fdf7..000000000 --- a/test/regress/regress1/sygus/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress1/sygus - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress1/sygus/Makefile.am b/test/regress/regress1/sygus/Makefile.am deleted file mode 100644 index c44c5034d..000000000 --- a/test/regress/regress1/sygus/Makefile.am +++ /dev/null @@ -1,81 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - hd-sdiv.sy \ - stopwatch-bt.sy \ - VC22_a.sy \ - unbdd_inv_gen_ex7.sy \ - real-grammar.sy \ - cegar1.sy \ - cggmp.sy \ - clock-inc-tuple.sy \ - dup-op.sy \ - fg_polynomial3.sy \ - hd-01-d1-prog.sy \ - icfp_14.12.sy \ - icfp_14.12-flip-args.sy \ - icfp_28_10.sy \ - icfp_easy-ite.sy \ - inv-example.sy \ - inv-unused.sy \ - multi-fun-polynomial2.sy \ - no-flat-simp.sy \ - process-10-vars.sy \ - tl-type.sy \ - tl-type-4x.sy \ - twolets2-orig.sy \ - unbdd_inv_gen_winf1.sy \ - array_search_2.sy \ - array_sum_2_5.sy \ - commutative.sy \ - constant.sy \ - dt-test-ns.sy \ - hd-19-d1-prog-dup-op.sy \ - list-head-x.sy \ - max.sy \ - nflat-fwd-3.sy \ - nflat-fwd.sy \ - nia-max-square-ns.sy \ - no-mention.sy \ - qe.sy \ - strings-concat-3-args.sy \ - strings-double-rec.sy \ - strings-small.sy \ - strings-template-infer-unused.sy \ - strings-template-infer.sy \ - strings-trivial-simp.sy \ - strings-trivial-two-type.sy \ - strings-trivial.sy \ - sygus-dt.sy \ - tl-type-0.sy \ - triv-type-mismatch-si.sy \ - twolets1.sy - -EXTRA_DIST = $(TESTS) \ - enum-test.sy - -# Base16_1.sy - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/uflia/Makefile.am b/test/regress/regress1/uflia/Makefile.am deleted file mode 100644 index c9a5ee372..000000000 --- a/test/regress/regress1/uflia/Makefile.am +++ /dev/null @@ -1,41 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 \ - microwave21.ec.minimized.smt2 \ - simple_cyclic2.smt2 \ - DRAGON_11_e1_2450.ec.minimized.smt2 \ - FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 \ - speed2_e8_449_e8_517.ec.smt2 \ - stalmark_e7_27_e7_31.ec.smt2 - - -EXTRA_DIST = $(TESTS) \ - DRAGON_11_e1_2450.ec.minimized.smt2.expect \ - FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect \ - speed2_e8_449_e8_517.ec.smt2.expect \ - stalmark_e7_27_e7_31.ec.smt2.expect - -# synonyms for "check" in this directory -.PHONY: regress regress1 test -regress regress1 test: check - -# do nothing in this subdir -.PHONY: regress0 regress2 regress3 regress4 -regress0 regress2 regress3 regress4: diff --git a/test/regress/regress2/Makefile b/test/regress/regress2/Makefile deleted file mode 100644 index 5a9aa63be..000000000 --- a/test/regress/regress2/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../.. -srcdir = test/regress/regress2 - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am deleted file mode 100644 index 34a26aae7..000000000 --- a/test/regress/regress2/Makefile.am +++ /dev/null @@ -1,79 +0,0 @@ -SUBDIRS = . arith nl quantifiers strings sygus - -# 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 = \ - bug136.smt \ - bug148.smt \ - bug394.smt2 \ - DTP_k2_n35_c175_s15.smt2 \ - GEO123+1.minimized.smt2 \ - error1.smt \ - friedman_n4_i5.smt \ - hole7.cvc \ - hole8.cvc \ - instance_1444.smt \ - fuzz_2.smt \ - hash_sat_10_09.smt2 \ - hash_sat_07_17.smt2 \ - ooo.tag10.smt2 \ - hash_sat_06_19.smt2 \ - hash_sat_09_09.smt2 \ - ooo.rf6.smt2 \ - auflia-fuzz06.smt \ - piVC_5581bd.smt2 \ - typed_v1l50016-simp.cvc \ - FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 \ - xs-09-16-3-4-1-5.smt \ - xs-09-16-3-4-1-5.decn.smt \ - uflia-error0.smt2 \ - bug812.smt2 \ - bug765.smt2 \ - simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 \ - bug674.smt2 \ - javafe.ast.WhileStmt.447_no_forall.smt2 \ - javafe.ast.StandardPrettyPrint.319_no_forall.smt2 - -EXTRA_DIST = $(TESTS) \ - FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect \ - uflia-error0.smt2.expect \ - xs-09-16-3-4-1-5.decn.smt.expect \ - bug396.smt2 \ - javafe.ast.StandardPrettyPrint.319_no_forall.smt2 \ - javafe.ast.WhileStmt.447_no_forall.smt2 - -#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 regress2 test -regress regress2 test: check - -# do nothing in this subdir -.PHONY: regress0 regress1 regress3 regress4 -regress0 regress1 regress3 regress4: diff --git a/test/regress/regress2/arith/Makefile b/test/regress/regress2/arith/Makefile deleted file mode 100644 index f96dc45f2..000000000 --- a/test/regress/regress2/arith/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../../.. -srcdir = test/regress/regress2/arith - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress2/arith/Makefile.am b/test/regress/regress2/arith/Makefile.am deleted file mode 100644 index 1bfad1dc3..000000000 --- a/test/regress/regress2/arith/Makefile.am +++ /dev/null @@ -1,41 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - abz5_1400.smt \ - pursuit-safety-11.smt \ - pursuit-safety-12.smt \ - sc-7.base.cvc.smt \ - uart-8.base.cvc.smt \ - qlock-4-10-9.base.cvc.smt2 \ - lpsat-goal-9.smt2 \ - prp-13-24.smt2 - - -EXTRA_DIST = $(TESTS) \ - miplib-opt1217--27.smt2 \ - miplib-pp08a-3000.smt2 \ - arith-int-098.cvc - -# synonyms for "check" in this directory -.PHONY: regress regress2 test -regress regress2 test: check - -# do nothing in this subdir -.PHONY: regress0 regress1 regress3 regress4 -regress0 regress1 regress3 regress4: diff --git a/test/regress/regress2/nl/Makefile.am b/test/regress/regress2/nl/Makefile.am deleted file mode 100644 index 246473831..000000000 --- a/test/regress/regress2/nl/Makefile.am +++ /dev/null @@ -1,33 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - siegel-nl-bases.smt2 - - -EXTRA_DIST = $(TESTS) \ - dumortier-050317.smt2 \ - nt-lemmas-bad.smt2 - -# synonyms for "check" in this directory -.PHONY: regress regress2 test -regress regress2 test: check - -# do nothing in this subdir -.PHONY: regress0 regress1 regress3 regress4 -regress0 regress1 regress3 regress4: diff --git a/test/regress/regress2/quantifiers/Makefile.am b/test/regress/regress2/quantifiers/Makefile.am deleted file mode 100644 index 19d1efb26..000000000 --- a/test/regress/regress2/quantifiers/Makefile.am +++ /dev/null @@ -1,38 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - ForElimination-scala-9.smt2 \ - javafe.ast.ArrayInit.35.smt2 \ - javafe.ast.StandardPrettyPrint.319.smt2 \ - javafe.ast.WhileStmt.447.smt2 \ - javafe.tc.CheckCompilationUnit.001.smt2 \ - javafe.tc.FlowInsensitiveChecks.682.smt2 \ - nunchaku2309663.nun.min.smt2 \ - AdditiveMethods_AdditiveMethods..ctor.smt2 - -EXTRA_DIST = $(TESTS) \ - small-bug1-fixpoint-3.smt2 - -# synonyms for "check" in this directory -.PHONY: regress regress2 test -regress regress2 test: check - -# do nothing in this subdir -.PHONY: regress0 regress1 regress3 regress4 -regress0 regress1 regress3 regress4: diff --git a/test/regress/regress2/strings/Makefile.am b/test/regress/regress2/strings/Makefile.am deleted file mode 100644 index 4e6f3aa56..000000000 --- a/test/regress/regress2/strings/Makefile.am +++ /dev/null @@ -1,35 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - cmu-dis-0707-3.smt2 \ - cmu-prereg-fmf.smt2 \ - cmu-repl-len-nterm.smt2 \ - cmu-disagree-0707-dd.smt2 - - -EXTRA_DIST = $(TESTS) \ - norn-dis-0707-3.smt2 - -# synonyms for "check" in this directory -.PHONY: regress regress2 test -regress regress2 test: check - -# do nothing in this subdir -.PHONY: regress0 regress1 regress3 regress4 -regress0 regress1 regress3 regress4: diff --git a/test/regress/regress2/sygus/Makefile.am b/test/regress/regress2/sygus/Makefile.am deleted file mode 100644 index 02091c3bd..000000000 --- a/test/regress/regress2/sygus/Makefile.am +++ /dev/null @@ -1,42 +0,0 @@ -# don't override a BINARY imported from a personal.mk -@mk_if@eq ($(BINARY),) -@mk_empty@BINARY = cvc4 -end@mk_if@ - -LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) - -if AUTOMAKE_1_11 -# old-style (pre-automake 1.12) test harness -TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) -endif - -# These are run for all build profiles. -# If a test shouldn't be run in e.g. competition mode, -# put it below in "TESTS +=" -TESTS = \ - array_sum_dd.sy \ - icfp_easy_mt_ite.sy \ - inv_gen_n_c11.sy \ - MPwL_d1s3.sy \ - nia-max-square.sy \ - no-syntax-test-no-si.sy \ - process-10-vars-2fun.sy \ - process-arg-invariance.sy \ - real-grammar-neg.sy \ - lustre-real.sy \ - max2-univ.sy \ - mpg_guard1-dd.sy \ - three.sy - -EXTRA_DIST = $(TESTS) - -# synonyms for "check" in this directory -.PHONY: regress regress2 test -regress regress2 test: check - -# do nothing in this subdir -.PHONY: regress0 regress1 regress3 regress4 -regress0 regress1 regress3 regress4: diff --git a/test/regress/regress3/Makefile b/test/regress/regress3/Makefile deleted file mode 100644 index 223547305..000000000 --- a/test/regress/regress3/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../.. -srcdir = test/regress/regress3 - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am deleted file mode 100644 index 4846a97f6..000000000 --- a/test/regress/regress3/Makefile.am +++ /dev/null @@ -1,54 +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 = bmc-ibm-1.smt \ - bmc-ibm-2.smt \ - bmc-ibm-5.smt \ - bmc-ibm-7.smt \ - friedman_n6_i4.smt \ - hole9.cvc \ - qwh.35.405.shuffled-as.sat03-1651.smt \ - eq_diamond14.smt \ - incorrect1.smt \ - incorrect2.smt \ - pp-regfile.smt - -EXTRA_DIST = $(TESTS) \ - pp-regfile.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 regress3 test -regress regress3 test: check - -# do nothing in this subdir -.PHONY: regress0 regress1 regress2 regress4 -regress0 regress1 regress2 regress4: diff --git a/test/regress/regress4/Makefile b/test/regress/regress4/Makefile deleted file mode 100644 index b926bb86e..000000000 --- a/test/regress/regress4/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -topdir = ../../.. -srcdir = test/regress/regress4 - -include $(topdir)/Makefile.subdir - -# synonyms for "check" -.PHONY: test -test: check diff --git a/test/regress/regress4/Makefile.am b/test/regress/regress4/Makefile.am deleted file mode 100644 index 5a31fb24e..000000000 --- a/test/regress/regress4/Makefile.am +++ /dev/null @@ -1,48 +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 = bug143.smt \ - C880mul.miter.shuffled-as.sat03-348.smt \ - comb2.shuffled-as.sat03-420.smt \ - hole10.cvc \ - instance_1151.smt \ - NEQ016_size5.smt - -EXTRA_DIST = $(TESTS) - -#if CVC4_BUILD_PROFILE_COMPETITION -#else -#TESTS += \ -# error.cvc -#endif -# -# and make sure to distribute it -#EXTRA_DIST += \ -# error.cvc - -# synonyms for "check" in this directory -.PHONY: regress regress4 test -regress regress4 test: check - -# do nothing in this subdir -.PHONY: regress0 regress1 regress2 regress3 -regress0 regress1 regress2 regress3: |