From a8c0ae49ee9c04327b1a8d538a0cdae746616d5b Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Sat, 15 Sep 2018 00:03:27 -0700
Subject: [PATCH] cmake: Disable unit tests if assertions are not enabled.

---
 CMakeLists.txt      | 3 +++
 test/CMakeLists.txt | 5 ++++-
 2 files changed, 7 insertions(+), 1 deletion(-)

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