From: Andres Noetzli Date: Wed, 21 Mar 2018 20:10:24 +0000 (-0700) Subject: Move regression tests to single Makefile.am (#1658) X-Git-Tag: cvc5-1.0.0~5225 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b8db52f9bad5b1053810c93f0067de8423349da3;p=cvc5.git Move regression tests to single Makefile.am (#1658) Until now, regression tests were split across tens of different Makefile.am, which required a lot of code duplication and does not really seem to be in the spirit of automake. If we want to change the LOG_COMPILER/LOG_DRIVER for example, we have to change every single Makefile.am, which is cumbersome (I was able to get something semi-working by exporting those variables but it didn't seem very clean). Additionally, it made the output of the regression tests fairly verbose and split the output across multiple log files. Finally it also limited parallelism when running the regression tests (this fix lowers the time it takes to run regression level 1 from 3m to 1m45s on my machine with 16 threads). This commit moves all the regression tests into test/regress/Makefile.tests and changes test/regress/Makefile.am to deal with this new structure. Finally, it changes how the test summary in test/Makefile.am is produced: instead of relying on the log files for the subdirectories, it greps for the test results in the log files of the individual tests. Not the most elegant solution but we should probably anyway delegate that task to a Python script at some point. --- 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: