summaryrefslogtreecommitdiff
path: root/test/regress/CMakeLists.txt
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2018-09-12 09:15:04 -0700
committerMathias Preiner <mathias.preiner@gmail.com>2018-09-22 16:30:59 -0700
commit89042eec4f63f0aebd3e540dbca5e01714d152b4 (patch)
tree748d4d337f265daa0e8110cd7032eb7618e00f9d /test/regress/CMakeLists.txt
parent479aebfc657eb9bc90fad550f51ec3b3d2efec76 (diff)
cmake: Added target check
Targets 'check', 'units', 'systemtests' and 'regress' are now run in parallel with the number of available cores by default. This can be overriden by passing ARGS=-jN.
Diffstat (limited to 'test/regress/CMakeLists.txt')
-rw-r--r--test/regress/CMakeLists.txt6
1 files changed, 5 insertions, 1 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c4ba87489..9ecb218d8 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2050,11 +2050,15 @@ set(regression_disabled_tests
regress2/xs-11-20-5-2-5-3.smt2
)
+#-----------------------------------------------------------------------------#
+# Add target 'regress', builds and runs
+# > regression tests of levels 0 and 1
+
get_target_property(path_to_cvc4 cvc4-bin RUNTIME_OUTPUT_DIRECTORY)
set(run_regress_script ${CMAKE_CURRENT_LIST_DIR}/run_regression.py)
add_custom_target(regress
- COMMAND ctest --output-on-failure -L "regress[0-1]" $(ARGS)
+ COMMAND ctest --output-on-failure -L "regress[0-1]" -j${NTHREADS} $(ARGS)
DEPENDS cvc4-bin)
macro(cvc4_add_regression_test level file)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback