From b94e9b63abdb6c3930720801474d82965196a803 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 6 Jun 2012 17:35:09 +0000 Subject: [PATCH] unconstrained regressions are now run with "make check", but with --unconstrained-simp option --- test/regress/regress0/Makefile.am | 3 +-- 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 -- 2.30.2