From 852d41b2878ae4981ab4a9b246345bb05bbe23ab Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 22 May 2013 16:33:15 -0500
Subject: Add regressions for finite model finding

---
 test/regress/regress0/fmf/Makefile.am | 47 +++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100755 test/regress/regress0/fmf/Makefile.am

(limited to 'test/regress/regress0/fmf/Makefile.am')

diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
new file mode 100755
index 000000000..a367447c9
--- /dev/null
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -0,0 +1,47 @@
+BINARY = cvc4
+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 = \
+	$(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 =	\
+	agree466.smt2 \
+	ALG008-1.smt2 \
+	german169.smt2 \
+	Hoare-z3.931718.smt \
+	QEpres-uf.855035.smt \
+	agree467.smt2 \
+	Arrow_Order-smtlib.778341.smt \
+	german73.smt2 \
+	PUZ001+1.smt2 \
+	refcount24.cvc.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
+regress1 regress2 regress3:
-- 
cgit v1.2.3