Update copyright headers.

[cvc5.git] / cmake / ConfigDebug.cmake

diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake
index 9decc07be3f067037b4010d27394894615e2b5d8..a4331bfcecdc7f8bd6a29f0791152dcb997b7db8 100644 (file)
--- a/cmake/ConfigDebug.cmake
+++ b/cmake/ConfigDebug.cmake
@@ -1,4 +1,3 @@
-set(CVC4_BUILD_PROFILE_DEBUG 1)
 add_definitions(-DCVC4_DEBUG)
 set(CVC4_DEBUG 1)
 add_check_c_cxx_flag("-fno-inline")
@@ -19,7 +18,15 @@ cvc4_set_option(ENABLE_PROOFS ON)
 # enable_tracing=yes
 cvc4_set_option(ENABLE_TRACING ON)
 # enable_dumping=yes
-cvc4_set_option(ENABLE_DUMPING ON)
+if(ENABLE_PORTFOLIO)
+  # Only print warning if dumping was not explicitely disabled by the user.
+  if(${ENABLE_DUMPING} STREQUAL "IGNORE")
+    message(WARNING
+      "Disabling dumping support, not supported with a portfolio build.")
+  endif()
+else()
+  cvc4_set_option(ENABLE_DUMPING ON)
+endif()
 # enable_muzzle=no
 cvc4_set_option(ENABLE_MUZZLE OFF)
 # enable_valgrind=optional