summaryrefslogtreecommitdiff
path: root/CMakeLists.txt
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2021-06-16 14:04:09 -0700
committerGitHub <noreply@github.com>2021-06-16 21:04:09 +0000
commitb8d09076cfeb124bfaa6e1c3f0f37e3df1b1b516 (patch)
treee634a4f8d9176a238b55a51e4b18d77c69c9895d /CMakeLists.txt
parent0f04a6c4cf618fb5914934bac5b5c6277f07127c (diff)
Make symfpu a required dependency. (#6749)
Diffstat (limited to 'CMakeLists.txt')
-rw-r--r--CMakeLists.txt10
1 files changed, 1 insertions, 9 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt
index b555c7bdc..b29585f3b 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -128,7 +128,6 @@ cvc5_option(USE_EDITLINE "Use Editline for better interactive support")
# > for options where we don't need to detect if set by user (default: OFF)
option(USE_POLY "Use LibPoly for polynomial arithmetic")
option(USE_COCOA "Use CoCoALib for further polynomial operations")
-option(USE_SYMFPU "Use SymFPU for floating point support")
option(USE_PYTHON2 "Force Python 2 (deprecated)")
# Custom install directories for dependencies
@@ -476,13 +475,7 @@ if(USE_EDITLINE)
endif()
endif()
-if(USE_SYMFPU)
- find_package(SymFPU REQUIRED)
- add_definitions(-DCVC5_USE_SYMFPU)
- set(CVC5_USE_SYMFPU 1)
-else()
- set(CVC5_USE_SYMFPU 0)
-endif()
+find_package(SymFPU REQUIRED)
if(GPL_LIBS)
if(NOT ENABLE_GPL)
@@ -673,7 +666,6 @@ else()
print_config("MP library " "gmp")
endif()
print_config("Editline " ${USE_EDITLINE})
-print_config("SymFPU " ${USE_SYMFPU})
message("")
print_config("Api docs " ${BUILD_DOCS})
message("")
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback