cmake: Disable unit tests if assertions are not enabled.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 23a52db59e6cae13e9117142f4f00ed28327ae98..69f990903e5932d2cadc6ceb1e2265da038ccbe2 100644 (file)
--- 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 64fa378ff99eeb9447aee274283d615f0432576c..e1205faa076bfc96a459f65f25d75ae691d1f11b 100644 (file)
--- 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()