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

diff --git a/configure.ac b/configure.ac
index e80c80e24cb921042b8fc1bb63173688efb6f335..e7d5a005aed2f774901bd3ef75d0ef7935827403 100644 (file)
--- 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 521536630499f0a2e068f70c1ea178e65e8b5ef3..dc046429a40a4dc66c5dd3077c4fa1996b54fa33 100644 (file)
--- 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