From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Fri, 19 Oct 2018 02:22:22 +0000 (-0700)
Subject: cmake: Run regression level 2 for make check. (#2645)
X-Git-Tag: cvc5-1.0.0~4404
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e57e2c8911d0b39a59aad29330466c93c8081506;p=cvc5.git

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

diff --git a/INSTALL.md b/INSTALL.md
index 9e0c9dfc4..98cef2061 100644
--- 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 b2f138572..1970bb659 100644
--- 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 cd98a8917..5d0459015 100644
--- 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)