From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 27 May 2010 04:08:33 +0000 (+0000)
Subject: fix bug 120; competition mode regression failures for intentionally-buggy input
X-Git-Tag: cvc5-1.0.0~9040
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5a658f2900ae5443190fd41bf86b750eec95d790;p=cvc5.git

fix bug 120; competition mode regression failures for intentionally-buggy input
---

diff --git a/configure.ac b/configure.ac
index e80c80e24..e7d5a005a 100644
--- a/configure.ac
+++ b/configure.ac
@@ -246,6 +246,11 @@ case "$with_build" in
     ;;
 esac
 
+AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION],  [test "$with_build" = production])
+AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG],       [test "$with_build" = debug])
+AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEFAULT],     [test "$with_build" = default])
+AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition])
+
 # permit a static binary
 AC_MSG_CHECKING([whether to build a static binary])
 AC_ARG_ENABLE([static-binary],
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 521536630..dc046429a 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,8 +1,11 @@
 SUBDIRS = precedence uf
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below.
 TESTS =	\
-	error.cvc \
 	boolean-prec.cvc \
 	distinct.smt \
 	flet.smt \
@@ -52,6 +55,12 @@ TESTS =	\
 	wiki.20.cvc \
 	wiki.21.cvc
 
+if CVC4_BUILD_PROFILE_COMPETITION
+else
+TESTS += \
+	error.cvc
+endif
+
 # synonyms for "check"
 .PHONY: regress regress0 test
 regress regress0 test: check