From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Sat, 15 Sep 2018 07:03:27 +0000 (-0700)
Subject: cmake: Disable unit tests if assertions are not enabled.
X-Git-Tag: cvc5-1.0.0~4544
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a8c0ae49ee9c04327b1a8d538a0cdae746616d5b;p=cvc5.git

cmake: Disable unit tests if assertions are not enabled.
---

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()