summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--test/regress/regress0/arith/Makefile.am5
-rw-r--r--test/regress/regress0/arith/integers/Makefile.am5
-rw-r--r--test/regress/regress0/arrays/Makefile.am4
-rw-r--r--test/regress/regress0/bv/Makefile.am5
-rw-r--r--test/regress/regress0/bv/core/Makefile.am4
-rw-r--r--test/regress/regress0/datatypes/Makefile.am5
-rw-r--r--test/regress/regress0/lemmas/Makefile.am5
-rw-r--r--test/regress/regress0/precedence/Makefile.am4
-rw-r--r--test/regress/regress0/preprocess/Makefile.am5
-rw-r--r--test/regress/regress0/push-pop/Makefile.am5
-rw-r--r--test/regress/regress0/uf/Makefile.am4
-rw-r--r--test/regress/regress0/uflra/Makefile.am5
-rw-r--r--test/regress/regress1/Makefile.am5
-rw-r--r--test/regress/regress1/arith/Makefile.am4
-rw-r--r--test/regress/regress2/Makefile.am5
-rw-r--r--test/regress/regress3/Makefile.am5
16 files changed, 75 insertions, 0 deletions
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index ceb57a8dc..fdd0ad4ed 100644
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -1,6 +1,11 @@
SUBDIRS = . integers
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+endif
+
MAKEFLAGS = -k
# These are run for all build profiles.
diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am
index 843d29200..91f4cf758 100644
--- a/test/regress/regress0/arith/integers/Makefile.am
+++ b/test/regress/regress0/arith/integers/Makefile.am
@@ -1,6 +1,11 @@
SUBDIRS = .
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/cvc4
+endif
+
MAKEFLAGS = -k
# These are run for all build profiles.
diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index db786040e..137b5bb6d 100644
--- a/test/regress/regress0/arrays/Makefile.am
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -1,4 +1,8 @@
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+endif
# These are run for all build profiles.
# If a test shouldn't be run in e.g. competition mode,
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 4fbf5998b..8d65ee3a9 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -1,6 +1,11 @@
SUBDIRS = . core
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+endif
+
MAKEFLAGS = -k
# These are run for all build profiles.
diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am
index 9a036ada0..fa0144da0 100644
--- a/test/regress/regress0/bv/core/Makefile.am
+++ b/test/regress/regress0/bv/core/Makefile.am
@@ -1,4 +1,8 @@
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/cvc4
+endif
# These are run for all build profiles.
# If a test shouldn't be run in e.g. competition mode,
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index efc9954c2..aa9b9ce0b 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -1,6 +1,11 @@
SUBDIRS = .
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+endif
+
MAKEFLAGS = -k
# These are run for all build profiles.
diff --git a/test/regress/regress0/lemmas/Makefile.am b/test/regress/regress0/lemmas/Makefile.am
index 1855118ab..70375e1d7 100644
--- a/test/regress/regress0/lemmas/Makefile.am
+++ b/test/regress/regress0/lemmas/Makefile.am
@@ -1,6 +1,11 @@
SUBDIRS = .
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+endif
+
MAKEFLAGS = -k
# These are run for all build profiles.
diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am
index d82dfd60b..6d60bcb4f 100644
--- a/test/regress/regress0/precedence/Makefile.am
+++ b/test/regress/regress0/precedence/Makefile.am
@@ -1,4 +1,8 @@
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+endif
# These are run for all build profiles.
# If a test shouldn't be run in e.g. competition mode,
diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am
index a4fe70946..85d188515 100644
--- a/test/regress/regress0/preprocess/Makefile.am
+++ b/test/regress/regress0/preprocess/Makefile.am
@@ -1,6 +1,11 @@
SUBDIRS = .
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+endif
+
MAKEFLAGS = -k
# These are run for all build profiles.
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 1dd1dcfd5..827dc04aa 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -1,6 +1,11 @@
SUBDIRS = .
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+endif
+
MAKEFLAGS = -k
# These are run for all build profiles.
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index ca2b19a96..3a9749598 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -1,4 +1,8 @@
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+endif
# These are run for all build profiles.
# If a test shouldn't be run in e.g. competition mode,
diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am
index 377489ef7..7caeedbb3 100644
--- a/test/regress/regress0/uflra/Makefile.am
+++ b/test/regress/regress0/uflra/Makefile.am
@@ -1,4 +1,9 @@
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+endif
+
MAKEFLAGS = -k
# These are run for all build profiles.
diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
index aeed6d4f9..355a1f85b 100644
--- a/test/regress/regress1/Makefile.am
+++ b/test/regress/regress1/Makefile.am
@@ -1,6 +1,11 @@
SUBDIRS = . arith
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+endif
+
MAKEFLAGS = -k
# These are run for all build profiles.
diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress1/arith/Makefile.am
index 72f71d341..53aff2491 100644
--- a/test/regress/regress1/arith/Makefile.am
+++ b/test/regress/regress1/arith/Makefile.am
@@ -1,4 +1,8 @@
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+endif
# These are run for all build profiles.
# If a test shouldn't be run in e.g. competition mode,
diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am
index 010b2b0d3..8a17bf6b2 100644
--- a/test/regress/regress2/Makefile.am
+++ b/test/regress/regress2/Makefile.am
@@ -1,6 +1,11 @@
SUBDIRS = .
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+endif
+
MAKEFLAGS = -k
# These are run for all build profiles.
diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am
index 6811e84a1..08a675273 100644
--- a/test/regress/regress3/Makefile.am
+++ b/test/regress/regress3/Makefile.am
@@ -1,6 +1,11 @@
SUBDIRS = .
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/cvc4
+else
TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+endif
+
MAKEFLAGS = -k
# These are run for all build profiles.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback