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/regress/regress0/unconstrained | |
| parent | ee29e7343e0306875e8e09dda1ac58f845ac603e (diff) | |
unconstrained regressions are now run with "make check", but with --unconstrained-simp option
Diffstat (limited to 'test/regress/regress0/unconstrained')
| -rw-r--r-- | test/regress/regress0/unconstrained/Makefile.am | 8 |
1 files changed, 6 insertions, 2 deletions
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 |