From e57e2c8911d0b39a59aad29330466c93c8081506 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Thu, 18 Oct 2018 19:22:22 -0700 Subject: [PATCH] cmake: Run regression level 2 for make check. (#2645) --- INSTALL.md | 4 ++-- test/CMakeLists.txt | 2 +- test/regress/CMakeLists.txt | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) 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) -- 2.30.2