summaryrefslogtreecommitdiff
path: root/test/regress/regress2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress2')
-rw-r--r--test/regress/regress2/Makefile8
-rw-r--r--test/regress/regress2/Makefile.am79
-rw-r--r--test/regress/regress2/arith/Makefile8
-rw-r--r--test/regress/regress2/arith/Makefile.am41
-rw-r--r--test/regress/regress2/nl/Makefile.am33
-rw-r--r--test/regress/regress2/quantifiers/Makefile.am38
-rw-r--r--test/regress/regress2/strings/Makefile.am35
-rw-r--r--test/regress/regress2/sygus/Makefile.am42
8 files changed, 0 insertions, 284 deletions
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback