diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-06 17:35:09 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-06 17:35:09 +0000 |
commit | b94e9b63abdb6c3930720801474d82965196a803 (patch) | |
tree | c00ef5088be870dd24fc341bc2a2d0f842bf3bff /test | |
parent | ee29e7343e0306875e8e09dda1ac58f845ac603e (diff) |
unconstrained regressions are now run with "make check", but with --unconstrained-simp option
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/unconstrained/Makefile.am | 8 |
2 files changed, 7 insertions, 4 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index bb9cb2384..a03084129 100644 --- 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 e963ae739..984cd4d45 100644 --- 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 |