unconstrained regressions are now run with "make check", but with --unconstrained...

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index bb9cb23841116c4fd0dac1b0b736a50ff361f15a..a030841292ffccf9e1ac54061e2c74092bf54005 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,5 +1,4 @@
-SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes lemmas push-pop preprocess
-DIST_SUBDIRS = $(SUBDIRS) unconstrained
+SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes lemmas push-pop preprocess unconstrained
 
 BINARY = cvc4
 if PROOF_REGRESSIONS

diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am
index e963ae739941c9d178499443115d6c5521793c0a..984cd4d459e92935efe4b12493088fd26763dc0e 100644 (file)
--- a/test/regress/regress0/unconstrained/Makefile.am
+++ b/test/regress/regress0/unconstrained/Makefile.am
@@ -5,6 +5,9 @@ else
 TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
 endif
 
+override CVC4_REGRESSION_ARGS += --unconstrained-simp
+export CVC4_REGRESSION_ARGS
+
 # These are run for all build profiles.
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
@@ -18,7 +21,6 @@ TESTS =       \
        arith.smt2 \
        array1.smt2 \
        bvbool2.smt2 \
-       bvbool3.smt2 \
        bvbool.smt2 \
        bvcmp.smt2 \
        bvconcat2.smt2 \
@@ -59,7 +61,9 @@ TESTS =       \
        uf2.smt2 \
        xor.smt2
 
-EXTRA_DIST = $(TESTS)
+# bvbool3 takes too long for regress0
+EXTRA_DIST = $(TESTS) \
+       bvbool3.smt2
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else