summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--CMakeLists.txt12
-rw-r--r--cmake/ConfigDebug.cmake11
-rw-r--r--cmake/ConfigProduction.cmake11
-rw-r--r--cmake/ConfigTesting.cmake11
4 files changed, 38 insertions, 7 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 617ca2780..bbdc863bd 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -245,10 +245,6 @@ if(ENABLE_DEBUG_CONTEXT_MM)
add_definitions(-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER)
endif()
-if(ENABLE_DUMPING)
- add_definitions(-DCVC4_DUMPING)
-endif()
-
if(ENABLE_DEBUG_SYMBOLS)
add_check_c_cxx_flag("-ggdb3")
endif()
@@ -260,6 +256,9 @@ endif()
# This check needs to come before the USE_CLN check.
if(ENABLE_PORTFOLIO)
find_package(Boost 1.50.0 REQUIRED COMPONENTS thread)
+ if (ENABLE_DUMPING)
+ message(FATAL_ERROR "Dumping not supported with a portfolio build.")
+ endif()
# Disable CLN for portfolio builds since it is not thread safe (uses an
# unlocked hash table internally).
if(USE_CLN)
@@ -275,6 +274,11 @@ if(ENABLE_PORTFOLIO)
set(BOOST_HAS_THREAD_ATTR 1)
endif()
+# This has to be processed after ENABLE_PORTFOLIO (disables dumping support).
+if(ENABLE_DUMPING)
+ add_definitions(-DCVC4_DUMPING)
+endif()
+
if(ENABLE_PROFILING)
add_definitions(-DCVC4_PROFILING)
add_check_c_cxx_flag("-pg")
diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake
index 9f58d3548..9c9f5ec10 100644
--- a/cmake/ConfigDebug.cmake
+++ b/cmake/ConfigDebug.cmake
@@ -18,7 +18,16 @@ 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)
+ if(ENABLE_DUMPING)
+ message(FATAL_ERROR "Dumping not supported with a portfolio build.")
+ else()
+ 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
diff --git a/cmake/ConfigProduction.cmake b/cmake/ConfigProduction.cmake
index 1b30dc1aa..db63507a7 100644
--- a/cmake/ConfigProduction.cmake
+++ b/cmake/ConfigProduction.cmake
@@ -15,7 +15,16 @@ cvc4_set_option(ENABLE_PROOFS ON)
# enable_tracing=no
cvc4_set_option(ENABLE_TRACING OFF)
# enable_dumping=yes
-cvc4_set_option(ENABLE_DUMPING ON)
+if(ENABLE_PORTFOLIO)
+ if(ENABLE_DUMPING)
+ message(FATAL_ERROR "Dumping not supported with a portfolio build.")
+ else()
+ 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=no
diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake
index 9627bcd52..3c995e421 100644
--- a/cmake/ConfigTesting.cmake
+++ b/cmake/ConfigTesting.cmake
@@ -15,7 +15,16 @@ 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)
+ if(ENABLE_DUMPING)
+ message(FATAL_ERROR "Dumping not supported with a portfolio build.")
+ else()
+ 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=no
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback