CMakeLists.txt

   1 cmake_minimum_required(VERSION 3.1)
   2
   3 if(POLICY CMP0075)
   4   cmake_policy(SET CMP0075 NEW)
   5 endif()
   6
   7 #-----------------------------------------------------------------------------#
   8 # Project configuration
   9
  10 project(cvc4)
  11
  12 set(CVC4_MAJOR   1) # Major component of the version of CVC4.
  13 set(CVC4_MINOR   7) # Minor component of the version of CVC4.
  14 set(CVC4_RELEASE 0) # Release component of the version of CVC4.
  15
  16 # Extraversion component of the version of CVC4.
  17 set(CVC4_EXTRAVERSION "-prerelease")
  18
  19 # Shared library versioning. Increment SOVERSION for every new CVC4 release.
  20 set(CVC4_SOVERSION 5)
  21
  22 # Full release string for CVC4.
  23 if(CVC4_RELEASE)
  24   set(CVC4_RELEASE_STRING
  25       "${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}${CVC4_EXTRAVERSION}")
  26 else()
  27   set(CVC4_RELEASE_STRING "${CVC4_MAJOR}.${CVC4_MINOR}${CVC4_EXTRAVERSION}")
  28 endif()
  29
  30 set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
  31 set(CMAKE_C_STANDARD 99)
  32 set(CMAKE_CXX_STANDARD 11)
  33
  34 #-----------------------------------------------------------------------------#
  35
  36 include(Helpers)
  37
  38 #-----------------------------------------------------------------------------#
  39 # User options
  40
  41 # License
  42 option(ENABLE_GPL "Enable GPL dependencies")
  43
  44 # General build options
  45 #
  46 # >> 3-valued: INGORE ON OFF
  47 #    > allows to detect if set by user (default: IGNORE)
  48 #    > only necessary for options set for build types
  49 cvc4_option(ENABLE_ASAN          "Enable ASAN build")
  50 cvc4_option(ENABLE_ASSERTIONS    "Enable assertions")
  51 cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
  52 cvc4_option(ENABLE_DUMPING       "Enable dumping")
  53 cvc4_option(ENABLE_MUZZLE        "Suppress ALL non-result output")
  54 cvc4_option(ENABLE_OPTIMIZED     "Enable optimization")
  55 cvc4_option(ENABLE_PORTFOLIO     "Enable portfolio support")
  56 cvc4_option(ENABLE_PROOFS        "Enable proof support")
  57 cvc4_option(ENABLE_REPLAY        "Enable the replay feature")
  58 cvc4_option(ENABLE_STATISTICS    "Enable statistics")
  59 cvc4_option(ENABLE_TRACING       "Enable tracing")
  60 cvc4_option(ENABLE_UNIT_TESTING  "Enable unit testing")
  61 cvc4_option(ENABLE_VALGRIND      "Enable valgrind instrumentation")
  62 cvc4_option(ENABLE_SHARED        "Build as shared library")
  63 # >> 2-valued: ON OFF
  64 #    > for options where we don't need to detect if set by user (default: OFF)
  65 option(ENABLE_BEST             "Enable dependencies known to give best performance")
  66 option(ENABLE_COVERAGE         "Enable support for gcov coverage testing")
  67 option(ENABLE_DEBUG_CONTEXT_MM "Enable the debug context memory manager")
  68 option(ENABLE_PROFILING        "Enable support for gprof profiling")
  69
  70 # Optional dependencies
  71 #
  72 # >> 3-valued: INGORE ON OFF
  73 #    > allows to detect if set by user (default: IGNORE)
  74 #    > only necessary for options set for ENABLE_BEST
  75 cvc4_option(USE_ABC      "Use ABC for AIG bit-blasting")
  76 cvc4_option(USE_CLN      "Use CLN instead of GMP")
  77 cvc4_option(USE_GLPK     "Use GLPK simplex solver")
  78 cvc4_option(USE_READLINE "Use readline for better interactive support")
  79 # >> 2-valued: ON OFF
  80 #    > for options where we don't need to detect if set by user (default: OFF)
  81 option(USE_CADICAL       "Use CaDiCaL SAT solver")
  82 option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
  83 option(USE_LFSC          "Use LFSC proof checker")
  84 option(USE_SYMFPU        "Use SymFPU for floating point support")
  85 option(USE_PYTHON2       "Prefer using Python 2 (for Python bindings)")
  86
  87 # Custom install directories for dependencies
  88 # If no directory is provided by the user, we first check if the dependency was
  89 # installed via the corresponding contrib/get-* script and if not found, we
  90 # check the intalled system version. If the user provides a directory we
  91 # immediately fail if the dependency was not found at the specified location.
  92 set(ABC_DIR           "" CACHE STRING "Set ABC install directory")
  93 set(ANTLR_DIR         "" CACHE STRING "Set ANTLR3 install directory")
  94 set(CADICAL_DIR       "" CACHE STRING "Set CaDiCaL install directory")
  95 set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory")
  96 set(GLPK_DIR          "" CACHE STRING "Set GLPK install directory")
  97 set(GMP_DIR           "" CACHE STRING "Set GMP install directory")
  98 set(LFSC_DIR          "" CACHE STRING "Set LFSC install directory")
  99 set(SYMFPU_DIR        "" CACHE STRING "Set SymFPU install directory")
 100
 101 # Supported language bindings
 102 option(BUILD_BINDINGS_JAVA   "Build Java bindings")
 103 option(BUILD_BINDINGS_PYTHON "Build Python bindings")
 104
 105 #-----------------------------------------------------------------------------#
 106 # Internal cmake variables
 107
 108 set(OPTIMIZATION_LEVEL 3)
 109 set(GPL_LIBS "")
 110
 111 #-----------------------------------------------------------------------------#
 112 # Build types
 113
 114 # Note: Module CodeCoverage requires the name of the debug build to conform
 115 #       to cmake standards (first letter uppercase).
 116 set(BUILD_TYPES Production Debug Testing Competition)
 117
 118 if(ENABLE_ASAN)
 119   set(CMAKE_BUILD_TYPE Debug)
 120 endif()
 121
 122 # Set the default build type to Production
 123 if(NOT CMAKE_BUILD_TYPE)
 124   set(CMAKE_BUILD_TYPE
 125       Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
 126   # Provide drop down menu options in cmake-gui
 127   set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
 128 endif()
 129
 130 # Check if specified build type is valid.
 131 list(FIND BUILD_TYPES ${CMAKE_BUILD_TYPE} FOUND_BUILD_TYPE)
 132 if(${FOUND_BUILD_TYPE} EQUAL -1)
 133   message(FATAL_ERROR
 134     "'${CMAKE_BUILD_TYPE}' is not a valid build type. "
 135     "Available builds are: ${BUILD_TYPES}")
 136 endif()
 137
 138 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
 139 include(Config${CMAKE_BUILD_TYPE})
 140
 141 #-----------------------------------------------------------------------------#
 142 # Compiler flags
 143
 144 add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
 145 add_check_c_flag("-fexceptions")
 146 add_check_c_cxx_flag("-Wno-deprecated")
 147 add_check_cxx_flag("-Wsuggest-override")
 148 add_check_cxx_flag("-Wnon-virtual-dtor")
 149
 150 #-----------------------------------------------------------------------------#
 151 # Option defaults (three-valued options (cvc4_option(...)))
 152 #
 153 # These options are only set if their value is IGNORE. Otherwise, the user
 154 # already set the option, which we don't want to overwrite.
 155
 156 cvc4_set_option(ENABLE_SHARED ON)
 157
 158 #-----------------------------------------------------------------------------#
 159 # Set options for best configuration
 160
 161 if(ENABLE_BEST)
 162   cvc4_set_option(USE_ABC ON)
 163   cvc4_set_option(USE_CLN ON)
 164   cvc4_set_option(USE_GLPK ON)
 165   cvc4_set_option(USE_READLINE ON)
 166 endif()
 167
 168 #-----------------------------------------------------------------------------#
 169 # Static libraries
 170
 171 # This needs to be set before any find_package(...) command since we want to
 172 # search for static libraries with suffix .a.
 173 if(NOT ENABLE_SHARED)
 174   set(CMAKE_FIND_LIBRARY_SUFFIXES ".a")
 175   set(CMAKE_EXE_LINKER_FLAGS "-static")
 176   set(BUILD_SHARED_LIBS OFF)
 177 endif()
 178
 179 #-----------------------------------------------------------------------------#
 180 # Enable the ctest testing framework
 181
 182 # This needs to be enabled here rather than in subdirectory test in order to
 183 # allow calling ctest from the root build directory.
 184 enable_testing()
 185
 186 #-----------------------------------------------------------------------------#
 187 # Check options, find packages and configure build.
 188
 189 if(USE_PYTHON2)
 190   find_package(PythonInterp 2.7 REQUIRED)
 191 else()
 192   find_package(PythonInterp 3)
 193   find_package(PythonInterp REQUIRED)
 194 endif()
 195
 196 set(GMP_HOME ${GMP_DIR})
 197 find_package(GMP REQUIRED)
 198 libcvc4_link_libraries(${GMP_LIBRARIES})
 199 libcvc4_include_directories(${GMP_INCLUDE_DIR})
 200
 201 if(ENABLE_ASAN)
 202   set(CMAKE_REQUIRED_LIBRARIES -fsanitize=address)
 203   add_required_c_cxx_flag("-fsanitize=address")
 204   unset(CMAKE_REQUIRED_LIBRARIES)
 205   add_required_c_cxx_flag("-fno-omit-frame-pointer")
 206   add_check_c_cxx_flag("-fsanitize-recover=address")
 207 endif()
 208
 209 if(ENABLE_ASSERTIONS)
 210   add_definitions(-DCVC4_ASSERTIONS)
 211 else()
 212   add_definitions(-DNDEBUG)
 213   # Only enable unit testing if assertions are enabled. Otherwise, unit tests
 214   # that expect AssertionException to be thrown will fail.
 215   set(ENABLE_UNIT_TESTING OFF)
 216 endif()
 217
 218 if(ENABLE_COVERAGE)
 219   include(CodeCoverage)
 220   APPEND_COVERAGE_COMPILER_FLAGS()
 221   add_definitions(-DCVC4_COVERAGE)
 222   setup_target_for_coverage_lcov(
 223     NAME coverage
 224     EXECUTABLE ctest $(ARGS)
 225     DEPENDENCIES cvc4-bin)
 226 endif()
 227
 228 if(ENABLE_DEBUG_CONTEXT_MM)
 229   add_definitions(-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER)
 230 endif()
 231
 232 if(ENABLE_DEBUG_SYMBOLS)
 233   add_check_c_cxx_flag("-ggdb3")
 234 endif()
 235
 236 if(ENABLE_MUZZLE)
 237   add_definitions(-DCVC4_MUZZLE)
 238 endif()
 239
 240 # This check needs to come before the USE_CLN check.
 241 if(ENABLE_PORTFOLIO)
 242   find_package(Boost 1.50.0 REQUIRED COMPONENTS thread)
 243   if (ENABLE_DUMPING)
 244     message(FATAL_ERROR "Dumping not supported with a portfolio build.")
 245   endif()
 246   # Disable CLN for portfolio builds since it is not thread safe (uses an
 247   # unlocked hash table internally).
 248   if(USE_CLN)
 249     message(WARNING "Disabling CLN support since portfolio is enabled.")
 250     set(USE_CLN OFF)
 251   endif()
 252   set(THREADS_PREFER_PTHREAD_FLAG ON)
 253   find_package(Threads REQUIRED)
 254   if(THREADS_HAVE_PTHREAD_ARG)
 255     add_c_cxx_flag(-pthread)
 256   endif()
 257   add_definitions(-DCVC4_PORTFOLIO)
 258   set(BOOST_HAS_THREAD_ATTR 1)
 259 endif()
 260
 261 # This has to be processed after ENABLE_PORTFOLIO (disables dumping support).
 262 if(ENABLE_DUMPING)
 263   add_definitions(-DCVC4_DUMPING)
 264 endif()
 265
 266 if(ENABLE_PROFILING)
 267   add_definitions(-DCVC4_PROFILING)
 268   add_check_c_cxx_flag("-pg")
 269 endif()
 270
 271 if(ENABLE_PROOFS)
 272   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --enable-proof)
 273   add_definitions(-DCVC4_PROOF)
 274 endif()
 275
 276 if(ENABLE_REPLAY)
 277   add_definitions(-DCVC4_REPLAY)
 278 endif()
 279
 280 if(ENABLE_TRACING)
 281   add_definitions(-DCVC4_TRACING)
 282 endif()
 283
 284 if(ENABLE_UNIT_TESTING)
 285         find_package(CxxTest REQUIRED)
 286   # Force shared libs for unit tests, static libs with unit tests are not
 287   # working right now.
 288   set(ENABLE_SHARED ON)
 289 endif()
 290
 291 if(ENABLE_SHARED)
 292   set(BUILD_SHARED_LIBS ON)
 293 endif()
 294
 295 if(ENABLE_STATISTICS)
 296   add_definitions(-DCVC4_STATISTICS_ON)
 297 endif()
 298
 299 if(ENABLE_VALGRIND)
 300   find_package(Valgrind REQUIRED)
 301   libcvc4_include_directories(${Valgrind_INCLUDE_DIR})
 302   add_definitions(-DCVC4_VALGRIND)
 303 endif()
 304
 305 if(USE_ABC)
 306   set(ABC_HOME "${ABC_DIR}")
 307   find_package(ABC REQUIRED)
 308   libcvc4_link_libraries(${ABC_LIBRARIES})
 309   libcvc4_include_directories(${ABC_INCLUDE_DIR})
 310   add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS})
 311 endif()
 312
 313 if(USE_CADICAL)
 314   set(CaDiCaL_HOME ${CADICAL_DIR})
 315   find_package(CaDiCaL REQUIRED)
 316   libcvc4_link_libraries(${CaDiCaL_LIBRARIES})
 317   libcvc4_include_directories(${CaDiCaL_INCLUDE_DIR})
 318   add_definitions(-DCVC4_USE_CADICAL)
 319 endif()
 320
 321 if(USE_CLN)
 322   set(GPL_LIBS "${GPL_LIBS} cln")
 323   find_package(CLN 1.2.2 REQUIRED)
 324   libcvc4_link_libraries(${CLN_LIBRARIES})
 325   libcvc4_include_directories(${CLN_INCLUDE_DIR})
 326   set(CVC4_USE_CLN_IMP 1)
 327   set(CVC4_USE_GMP_IMP 0)
 328 else()
 329   set(CVC4_USE_CLN_IMP 0)
 330   set(CVC4_USE_GMP_IMP 1)
 331 endif()
 332
 333 if(USE_CRYPTOMINISAT)
 334   # CryptoMiniSat requires pthreads support
 335   set(THREADS_PREFER_PTHREAD_FLAG ON)
 336   find_package(Threads REQUIRED)
 337   if(THREADS_HAVE_PTHREAD_ARG)
 338     add_c_cxx_flag(-pthread)
 339   endif()
 340   set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR})
 341   find_package(CryptoMiniSat REQUIRED)
 342   libcvc4_link_libraries(${CryptoMiniSat_LIBRARIES})
 343   libcvc4_include_directories(${CryptoMiniSat_INCLUDE_DIR})
 344   add_definitions(-DCVC4_USE_CRYPTOMINISAT)
 345 endif()
 346
 347 if(USE_GLPK)
 348   set(GPL_LIBS "${GPL_LIBS} glpk")
 349   set(GLPK_HOME ${GLPK_DIR})
 350   find_package(GLPK REQUIRED)
 351   libcvc4_link_libraries(${GLPK_LIBRARIES})
 352   libcvc4_include_directories(${GLPK_INCLUDE_DIR})
 353   add_definitions(-DCVC4_USE_GLPK)
 354 endif()
 355
 356 if(USE_LFSC)
 357   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
 358   set(LFSC_HOME ${LFSC_DIR})
 359   find_package(LFSC REQUIRED)
 360   libcvc4_link_libraries(${LFSC_LIBRARIES})
 361   libcvc4_include_directories(${LFSC_INCLUDE_DIR})
 362   add_definitions(-DCVC4_USE_LFSC)
 363 endif()
 364
 365 if(USE_READLINE)
 366   find_package(Readline REQUIRED)
 367   set(HAVE_LIBREADLINE 1)
 368   if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
 369     set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
 370   endif()
 371 endif()
 372
 373 if(USE_SYMFPU)
 374   set(SymFPU_HOME ${SYMFPU_DIR})
 375   find_package(SymFPU REQUIRED)
 376   libcvc4_include_directories(${SymFPU_INCLUDE_DIR})
 377   add_definitions(-DCVC4_USE_SYMFPU)
 378   set(CVC4_USE_SYMFPU 1)
 379 else()
 380   set(CVC4_USE_SYMFPU 0)
 381 endif()
 382
 383 if(GPL_LIBS)
 384   if(NOT ENABLE_GPL)
 385     message(FATAL_ERROR
 386       "Bad configuration detected: BSD-licensed code only, but also requested "
 387       "GPLed libraries: ${GPL_LIBS}")
 388   endif()
 389   set(CVC4_GPL_DEPS 1)
 390 endif()
 391
 392 #-----------------------------------------------------------------------------#
 393 # Generate CVC4's cvc4autoconfig.h header
 394
 395 include(ConfigureCVC4)
 396 configure_file(cvc4autoconfig.new.h.in cvc4autoconfig.h)
 397 include_directories(${CMAKE_CURRENT_BINARY_DIR})
 398
 399 #-----------------------------------------------------------------------------#
 400 # Add subdirectories
 401
 402 # signatures needs to come before src since it adds source files to libcvc4.
 403 if(ENABLE_PROOFS)
 404   add_subdirectory(proofs/signatures)
 405 endif()
 406
 407 add_subdirectory(doc)
 408 add_subdirectory(examples EXCLUDE_FROM_ALL)  # excluded from all target
 409 add_subdirectory(src)
 410 add_subdirectory(test)
 411
 412 if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
 413   add_subdirectory(src/bindings)
 414 endif()
 415
 416 #-----------------------------------------------------------------------------#
 417 # Print build configuration
 418
 419 # Convert build type to lower case.
 420 string(TOLOWER ${CMAKE_BUILD_TYPE} CVC4_BUILD_PROFILE_STRING)
 421
 422 # Get all definitions added via add_definitions.
 423 get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS)
 424 string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
 425
 426 message("CVC4 ${CVC4_RELEASE_STRING}")
 427 message("")
 428 message("Build profile        : ${CVC4_BUILD_PROFILE_STRING}")
 429 message("")
 430 print_config("GPL                  :" ENABLE_GPL)
 431 print_config("Best configuration   :" ENABLE_BEST)
 432 print_config("Optimized            :" ENABLE_OPTIMIZED)
 433 print_config("Optimization level   :" OPTIMIZATION_LEVEL)
 434 message("")
 435 print_config("Assertions           :" ENABLE_ASSERTIONS)
 436 print_config("Debug symbols        :" ENABLE_DEBUG_SYMBOLS)
 437 print_config("Debug context mem mgr:" ENABLE_DEBUG_CONTEXT_MM)
 438 message("")
 439 print_config("Dumping              :" ENABLE_DUMPING)
 440 print_config("Muzzle               :" ENABLE_MUZZLE)
 441 print_config("Proofs               :" ENABLE_PROOFS)
 442 print_config("Replay               :" ENABLE_REPLAY)
 443 print_config("Statistics           :" ENABLE_STATISTICS)
 444 print_config("Tracing              :" ENABLE_TRACING)
 445 message("")
 446 print_config("Asan                 :" ENABLE_ASAN)
 447 print_config("Coverage (gcov)      :" ENABLE_COVERAGE)
 448 print_config("Profiling (gprof)    :" ENABLE_PROFILING)
 449 print_config("Unit tests           :" ENABLE_UNIT_TESTING)
 450 print_config("Valgrind             :" ENABLE_VALGRIND)
 451 message("")
 452 print_config("Shared libs          :" ENABLE_SHARED)
 453 print_config("Java bindings        :" BUILD_BINDINGS_JAVA)
 454 print_config("Python bindings      :" BUILD_BINDINGS_PYTHON)
 455 print_config("Python2              :" USE_PYTHON2)
 456 message("")
 457 print_config("Portfolio            :" ENABLE_PORTFOLIO)
 458 message("")
 459 print_config("ABC                  :" USE_ABC)
 460 print_config("CaDiCaL              :" USE_CADICAL)
 461 print_config("CryptoMiniSat        :" USE_CRYPTOMINISAT)
 462 print_config("GLPK                 :" USE_GLPK)
 463 print_config("LFSC                 :" USE_LFSC)
 464
 465 if(CVC4_USE_CLN_IMP)
 466   message("MP library           : cln")
 467 else()
 468   message("MP library           : gmp")
 469 endif()
 470 print_config("Readline             :" ${USE_READLINE})
 471 print_config("SymFPU               :" ${USE_SYMFPU})
 472 message("")
 473 if(ABC_DIR)
 474   message("ABC dir              : ${ABC_DIR}")
 475 endif()
 476 if(ANTLR_DIR)
 477   message("ANTLR dir            : ${ANTLR_DIR}")
 478 endif()
 479 if(CADICAL_DIR)
 480   message("CADICAL dir          : ${CADICAL_DIR}")
 481 endif()
 482 if(CRYPTOMINISAT_DIR)
 483   message("CRYPTOMINISAT dir    : ${CRYPTOMINISAT_DIR}")
 484 endif()
 485 if(GLPK_DIR)
 486   message("GLPK dir             : ${GLPK_DIR}")
 487 endif()
 488 if(GMP_DIR)
 489   message("GMP dir              : ${GMP_DIR}")
 490 endif()
 491 if(LFSC_DIR)
 492   message("LFSC dir             : ${LFSC_DIR}")
 493 endif()
 494 if(SYMFPU_DIR)
 495   message("SYMFPU dir           : ${SYMFPU_DIR}")
 496 endif()
 497 message("")
 498 message("CPPLAGS (-D...)      : ${CVC4_DEFINITIONS}")
 499 message("CXXFLAGS             : ${CMAKE_CXX_FLAGS}")
 500 message("CFLAGS               : ${CMAKE_C_FLAGS}")
 501 message("")
 502 message("Install prefix       : ${CMAKE_INSTALL_PREFIX}")
 503 message("")
 504
 505 if(GPL_LIBS)
 506   message(
 507   "CVC4 license         : GPLv3 (due to optional libraries; see below)"
 508   "\n"
 509   "\n"
 510   "Please note that CVC4 will be built against the following GPLed libraries:"
 511   "\n"
 512   "${GPL_LIBS}"
 513   "\n"
 514   "As these libraries are covered under the GPLv3, so is this build of CVC4."
 515   "\n"
 516   "CVC4 is also available to you under the terms of the (modified) BSD license."
 517   "\n"
 518   "If you prefer to license CVC4 under those terms, please configure CVC4 to"
 519   "\n"
 520   "disable all optional GPLed library dependences (-DENABLE_BSD_ONLY=ON)."
 521   )
 522 else()
 523   message(
 524   "CVC4 license         : modified BSD"
 525   "\n"
 526   "\n"
 527   "Note that this configuration is NOT built against any GPL'ed libraries, so"
 528   "\n"
 529   "it is covered by the (modified) BSD license.  This is, however, not the best"
 530   "\n"
 531   "performing configuration of CVC4.  To build against GPL'ed libraries which"
 532   "\n"
 533   "improve CVC4's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
 534   )
 535 endif()
 536
 537 message("")
 538 message("Now just type make, followed by make check or make install.")
 539 message("")