support for proof regressions in other parts of the test tree

diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index ceb57a8dcd68f1ede835baf5beaf272cc78f1c42..fdd0ad4edb2583a4f6369d7e0e1917f275195ec7 100644 (file)
--- 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 843d29200b1da20c42cd783807b74b47d05f75ba..91f4cf7580a48837d432b08e73dc666fc5ba34c1 100644 (file)
--- 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 db786040e98b7c105c6c9141f0c7fbffdf4fcb02..137b5bb6df5ce172f760eb371e553ce21b94f568 100644 (file)
--- 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 4fbf5998b0dd04cc25ec04bd86c5db087dcf7130..8d65ee3a9dfbc2eb04aeca51579edbfcf97bdff0 100644 (file)
--- 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 9a036ada03ed09d3ecdb7fddb744594359cc3384..fa0144da0f1e843e73554d5e52def45e465f05ee 100644 (file)
--- 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 efc9954c29795f62e9d769fb92a78d6582d27db4..aa9b9ce0b543952e21502384296ad9557669f829 100644 (file)
--- 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 1855118ab672f28adca40a5c0320d238c95c6e7f..70375e1d7be527f17d0657550b38bf91aa584033 100644 (file)
--- 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 d82dfd60b00483bab314a4634e6a7a64caa776f2..6d60bcb4f38c463ae07539e1f5833d803af820fa 100644 (file)
--- 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 a4fe70946d10f5e4c95e7ac9b96422d06da557cd..85d188515f04a83ab4caf676038bcbac3c893264 100644 (file)
--- 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 1dd1dcfd5e08ddf85da5ab124da18f781577d177..827dc04aacb9ee30e7617b0345d5092b117c9060 100644 (file)
--- 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 ca2b19a96ace725af5baeae7970e5ca1b5f74e2a..3a97495981382ab89cc4d61d7e77a63e21f6ebf3 100644 (file)
--- 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 377489ef76e08aae2d3f5d564478d47c94c9ad17..7caeedbb3f8d0e02c13b5a3416b09f783ef0ebf8 100644 (file)
--- 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 aeed6d4f9c20e0f5a6d2347c304797038044199a..355a1f85be48fdf069d051bc206809d4f865c49d 100644 (file)
--- 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 72f71d341955d90543b7335446fe3cebb1d918e0..53aff2491eb2ed05f0c333caddc5774c564eafc4 100644 (file)
--- 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 010b2b0d3c4b8d5ea6bb704a26ccd81845416f17..8a17bf6b244b488b93200b206896e3b78865ca02 100644 (file)
--- 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 6811e84a17da6cbd4c946855ba8ba4d32703e057..08a6752731e1e5897e7b24df6cfd396bda18b041 100644 (file)
--- 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.