diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-06-06 16:17:19 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-06-06 16:17:19 +0000 |
| commit | ee29e7343e0306875e8e09dda1ac58f845ac603e (patch) | |
| tree | c303a29ec48f53eb46e45d5b4197c04da17f5f95 /test/regress | |
| parent | b8d08b54a0dc3e05cf557e9f5f0d375b1330fed6 (diff) | |
Fixing numerous issues with tests and "make dist":
* test/regress/regress0/unconstrained wasn't being distributed. This caused the debian build failure last night. (It still doesn't run on "make check", but had to be distributed properly.)
* Fixing an issue where a test name was longer than 99 characters and couldn't be distributed in the "old" tar format. (Told automake to use a newer tar format.)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/aufbv/Makefile.am | 2 | ||||
| -rw-r--r-- | test/regress/regress0/unconstrained/Makefile | 8 | ||||
| -rw-r--r-- | test/regress/regress0/unconstrained/Makefile.am | 2 |
4 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index db9b4d07f..bb9cb2384 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,4 +1,5 @@ SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes lemmas push-pop preprocess +DIST_SUBDIRS = $(SUBDIRS) unconstrained BINARY = cvc4 if PROOF_REGRESSIONS diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index 9b9820258..cd5f1d981 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -5,6 +5,8 @@ else TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY) endif +MAKEFLAGS = -k + # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" diff --git a/test/regress/regress0/unconstrained/Makefile b/test/regress/regress0/unconstrained/Makefile new file mode 100644 index 000000000..594b10e3c --- /dev/null +++ b/test/regress/regress0/unconstrained/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/unconstrained + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am index 241b78848..e963ae739 100644 --- a/test/regress/regress0/unconstrained/Makefile.am +++ b/test/regress/regress0/unconstrained/Makefile.am @@ -59,6 +59,8 @@ TESTS = \ uf2.smt2 \ xor.smt2 +EXTRA_DIST = $(TESTS) + #if CVC4_BUILD_PROFILE_COMPETITION #else #TESTS += \ |