summaryrefslogtreecommitdiff
path: root/CMakeLists.txt
diff options
context:
space:
mode:
Diffstat (limited to 'CMakeLists.txt')
-rw-r--r--CMakeLists.txt18
1 files changed, 18 insertions, 0 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 453f1bcf7..3eced0885 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -217,6 +217,24 @@ endif()
enable_testing()
#-----------------------------------------------------------------------------#
+# Check GCC version.
+#
+# GCC version 4.5.1 builds MiniSat incorrectly with -O2, which results in
+# incorrect answers.
+
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
+ execute_process(
+ COMMAND ${CMAKE_CXX_COMPILER} -dumpversion
+ OUTPUT_VARIABLE GCC_VERSION
+ OUTPUT_STRIP_TRAILING_WHITESPACE)
+ if(GCC_VERSION VERSION_EQUAL "4.5.1")
+ message(FATAL_ERROR
+ "GCC 4.5.1's optimizer is known to build MiniSat incorrectly "
+ "(and by extension CVC4).")
+ endif()
+endif()
+
+#-----------------------------------------------------------------------------#
# Check options, find packages and configure build.
if(USE_PYTHON2)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback