cmake: Run regression level 2 for make check. (#2645)

diff --git a/INSTALL.md b/INSTALL.md
index 9e0c9dfc488c1183d03683888aa44bb92d4d9033..98cef20618686c0ee03a4f27c9b6dd7f45df8a29 100644 (file)
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -297,7 +297,7 @@ All custom test targets build and run a preconfigured set of tests.
 
 - `make check [-jN] [ARGS=-jN]`  
   The default build-and-test target for CVC4, builds and runs all examples,
-  all system and unit tests, and regression tests from levels 0 and 1.
+  all system and unit tests, and regression tests from levels 0 to 2.
 
 - `make systemtests [-jN] [ARGS=-jN]`  
   Build and run all system tests.
@@ -306,7 +306,7 @@ All custom test targets build and run a preconfigured set of tests.
   Build and run all unit tests.
 
 - `make regress [-jN] [ARGS=-jN]`  
-  Build and run regression tests from levels 0 and 1.
+  Build and run regression tests from levels 0 to 2.
 
 - `make runexamples [-jN] [ARGS=-jN]`  
   Build and run all examples.

diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index b2f138572918173c9a545f8faca885d45c020268..1970bb659eee4ff86867a912463a9de8e08e95dd 100644 (file)
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -17,7 +17,7 @@ add_dependencies(build-tests examples)
 # Dependencies of check are added in the corresponding subdirectories.
 add_custom_target(check
   COMMAND
-    ctest --output-on-failure -LE "regress[2-4]" -j${CTEST_NTHREADS} $(ARGS)
+    ctest --output-on-failure -LE "regress[3-4]" -j${CTEST_NTHREADS} $(ARGS)
   DEPENDS
     build-tests)
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cd98a8917e849c0d6420105b7635d105e88e3020..5d0459015e89eb6809e2745c47fed6658ae4f6d5 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2097,7 +2097,7 @@ add_dependencies(build-tests build-regress)
 
 add_custom_target(regress
   COMMAND
-    ctest --output-on-failure -L "regress[0-1]" -j${CTEST_NTHREADS} $(ARGS)
+    ctest --output-on-failure -L "regress[0-2]" -j${CTEST_NTHREADS} $(ARGS)
   DEPENDS build-regress)
 
 macro(cvc4_add_regression_test level file)