diff options
| -rw-r--r-- | CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/CMakeLists.txt | 5 |
2 files changed, 7 insertions, 1 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 23a52db59..69f990903 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -228,6 +228,9 @@ if(ENABLE_ASSERTIONS) add_definitions(-DCVC4_ASSERTIONS) else() add_definitions(-DNDEBUG) + # Only enable unit testing if assertions are enabled. Otherwise, unit tests + # that expect AssertionException to be thrown will fail. + set(ENABLE_UNIT_TESTING OFF) endif() if(ENABLE_COVERAGE) diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 64fa378ff..e1205faa0 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -28,7 +28,10 @@ endif() add_custom_target(check COMMAND ctest --output-on-failure -LE "regress[2-4]" -j${NTHREADS} $(ARGS) - DEPENDS units regress systemtests) + DEPENDS regress systemtests) if(BUILD_BINDINGS_JAVA) add_dependencies(check cvc4javatests) endif() +if(ENABLE_UNIT_TESTING) + add_dependencies(check units) +endif() |