diff options
Diffstat (limited to 'CMakeLists.txt')
| -rw-r--r-- | CMakeLists.txt | 10 |
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("") |