From b8d09076cfeb124bfaa6e1c3f0f37e3df1b1b516 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 16 Jun 2021 14:04:09 -0700
Subject: [PATCH] Make symfpu a required dependency. (#6749)

---
 CMakeLists.txt                                |  10 +-
 INSTALL.md                                    |   6 +-
 NEWS                                          |   1 +
 configure.sh                                  |   7 -
 examples/api/java/FloatingPointArith.java     |   7 -
 examples/api/python/floating_point.py         |   6 -
 src/CMakeLists.txt                            |   5 +-
 src/api/cpp/cvc5.cpp                          |  30 ---
 src/api/cpp/cvc5.h                            |   6 -
 src/api/python/cvc5.pxd                       |   1 -
 src/api/python/cvc5.pxi                       |   3 -
 src/base/configuration.cpp                    |  13 +-
 src/base/configuration.h                      |   2 -
 src/base/configuration_private.h              |   6 -
 src/options/options_handler.cpp               |   1 -
 src/theory/fp/fp_converter.cpp                |  33 ----
 src/theory/fp/fp_converter.h                  |  10 -
 src/theory/fp/theory_fp.cpp                   |   2 +-
 src/theory/fp/theory_fp_rewriter.cpp          |  14 --
 src/theory/fp/theory_fp_type_rules.cpp        |   8 -
 src/theory/logic_info.cpp                     |   4 -
 src/util/CMakeLists.txt                       |   3 -
 src/util/floatingpoint_literal_symfpu.cpp     | 185 ------------------
 ...pu.h.in => floatingpoint_literal_symfpu.h} |  38 +---
 .../floatingpoint_literal_symfpu_traits.cpp   |   3 -
 ... => floatingpoint_literal_symfpu_traits.h} |   9 +-
 test/api/issue4889.cpp                        |   2 -
 test/python/unit/api/test_solver.py           |  82 ++------
 test/python/unit/api/test_sort.py             |  32 ++-
 test/regress/README.md                        |   8 +-
 test/regress/regress0/fp/abs-unsound.smt2     |   1 -
 test/regress/regress0/fp/abs-unsound2.smt2    |   1 -
 test/regress/regress0/fp/down-cast-RNA.smt2   |   1 -
 test/regress/regress0/fp/ext-rew-test.smt2    |   1 -
 test/regress/regress0/fp/from_sbv.smt2        |   1 -
 test/regress/regress0/fp/from_ubv.smt2        |   1 -
 test/regress/regress0/fp/issue-5524.smt2      |   1 -
 test/regress/regress0/fp/issue3536.smt2       |   1 -
 test/regress/regress0/fp/issue3582.smt2       |   1 -
 test/regress/regress0/fp/issue3619.smt2       |   1 -
 .../regress0/fp/issue4277-assign-func.smt2    |   1 -
 test/regress/regress0/fp/issue5511.smt2       |   1 -
 test/regress/regress0/fp/issue5734.smt2       |   1 -
 test/regress/regress0/fp/issue6164.smt2       |   1 -
 test/regress/regress0/fp/rti_3_5_bug.smt2     |   1 -
 test/regress/regress0/fp/simple.smt2          |   1 -
 test/regress/regress0/fp/wrong-model.smt2     |   1 -
 test/regress/regress0/issue5370.smt2          |   1 -
 test/regress/regress0/parser/to_fp.smt2       |   1 -
 .../regress1/fp/rti_3_5_bug_report.smt2       |   1 -
 .../regress1/quantifiers/fp-cegqi-unsat.smt2  |   1 -
 .../issue4420-order-sensitive.smt2            |   1 -
 test/regress/regress1/rr-verify/fp-arith.sy   |   1 -
 test/regress/regress1/rr-verify/fp-bool.sy    |   1 -
 .../temp_input_to_synth_ic-error-121418.sy    |   1 -
 .../regress1/wrong-qfabvfp-smtcomp2018.smt2   |   1 -
 test/regress/regress2/sygus/min_IC_1.sy       |   1 -
 test/unit/api/solver_black.cpp                | 115 ++---------
 test/unit/api/sort_black.cpp                  |  36 ++--
 test/unit/theory/logic_info_white.cpp         |  27 +--
 test/unit/util/CMakeLists.txt                 |   2 -
 61 files changed, 86 insertions(+), 658 deletions(-)
 rename src/util/{floatingpoint_literal_symfpu.h.in => floatingpoint_literal_symfpu.h} (92%)
 rename src/util/{floatingpoint_literal_symfpu_traits.h.in => floatingpoint_literal_symfpu_traits.h} (99%)

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("")
diff --git a/INSTALL.md b/INSTALL.md
index 41f770288..1a9c03476 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -57,6 +57,7 @@ minimum versions; more recent versions should be compatible.
 - [GMP v6.1 (GNU Multi-Precision arithmetic library)](https://gmplib.org)
 - [ANTLR 3.4](http://www.antlr3.org/)
 - [Java >= 1.6](https://www.java.com)
+- [SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4)
 
 
 ### ANTLR 3.4 parser generator
@@ -74,8 +75,6 @@ cross-compile, or you want to build cvc5 statically but the distribution does
 not ship static libraries, cvc5 builds GMP automatically when `--auto-download`
 is given.
 
-## Optional Dependencies
-
 ### SymFPU (Support for the Theory of Floating Point Numbers)
 
 [SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4)
@@ -83,7 +82,8 @@ is an implementation of SMT-LIB/IEEE-754 floating-point operations in terms
 of bit-vector operations.
 It is required for supporting the theory of floating-point numbers and
 can be downloaded and built automatically.
-Configure cvc5 with `configure.sh --symfpu` to build with this dependency.
+
+## Optional Dependencies
 
 ### CaDiCaL (Optional SAT solver)
 
diff --git a/NEWS b/NEWS
index 60a70a6c5..1943d7f00 100644
--- a/NEWS
+++ b/NEWS
@@ -4,6 +4,7 @@ Changes since CVC4 1.8
 ======================
 
 New Features:
+* SymFPU is now a required dependency.
 * New unsat-core production modes based on the new proof infrastructure
   (`--unsat-cores-mode=sat-proof`) and on the solving-under-assumption feature
   of Minisat (`--unsat-cores-mode=assumptions`). The mode based on SAT
diff --git a/configure.sh b/configure.sh
index 487bbcb5a..25203f8a6 100755
--- a/configure.sh
+++ b/configure.sh
@@ -64,7 +64,6 @@ The following flags enable optional packages (disable with --no-<option name>).
   --kissat                 use the Kissat SAT solver
   --poly                   use the LibPoly library [default=yes]
   --cocoa                  use the CoCoA library
-  --symfpu                 use SymFPU for floating point solver [default=yes]
   --editline               support the editline library
 
 Optional Path to Optional Packages:
@@ -133,7 +132,6 @@ editline=default
 shared=default
 static_binary=default
 statistics=default
-symfpu=ON
 tracing=default
 tsan=default
 ubsan=default
@@ -260,9 +258,6 @@ do
     --statistics) statistics=ON;;
     --no-statistics) statistics=OFF;;
 
-    --symfpu) symfpu=ON;;
-    --no-symfpu) symfpu=OFF;;
-
     --tracing) tracing=ON;;
     --no-tracing) tracing=OFF;;
 
@@ -398,8 +393,6 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DUSE_POLY=$poly"
 [ $cocoa != default ] \
   && cmake_opts="$cmake_opts -DUSE_COCOA=$cocoa"
-[ $symfpu != default ] \
-  && cmake_opts="$cmake_opts -DUSE_SYMFPU=$symfpu"
 [ "$abc_dir" != default ] \
   && cmake_opts="$cmake_opts -DABC_DIR=$abc_dir"
 [ "$glpk_dir" != default ] \
diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java
index 61ab18148..46f8b8330 100644
--- a/examples/api/java/FloatingPointArith.java
+++ b/examples/api/java/FloatingPointArith.java
@@ -27,13 +27,6 @@ public class FloatingPointArith {
     System.loadLibrary("cvc4jni");
 
     // Test whether CVC4 was built with floating-point support
-    if (!Configuration.isBuiltWithSymFPU()) {
-      System.out.println("CVC4 was built without floating-point support.");
-      System.out.println("Configure with --symfpu and rebuild CVC4 to run");
-      System.out.println("this example.");
-      System.exit(77);
-    }
-
     ExprManager em = new ExprManager();
     SmtEngine smt = new SmtEngine(em);
 
diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py
index 66b18642d..0001f726b 100644
--- a/examples/api/python/floating_point.py
+++ b/examples/api/python/floating_point.py
@@ -22,12 +22,6 @@ from pycvc5 import kinds
 if __name__ == "__main__":
     slv = pycvc5.Solver()
 
-    if not slv.supportsFloatingPoint():
-        # cvc5 must be built with SymFPU to support the theory of
-        # floating-point numbers
-        print("cvc5 was not built with floating-point support.")
-        exit()
-
     slv.setOption("produce-models", "true")
     slv.setLogic("QF_FP")
 
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2419e1e41..d7da67cbe 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1204,9 +1204,8 @@ endif()
 if(USE_POLY)
   target_link_libraries(cvc5 PRIVATE Polyxx)
 endif()
-if(USE_SYMFPU)
-  target_link_libraries(cvc5 PRIVATE SymFPU)
-endif()
+
+target_link_libraries(cvc5 PRIVATE SymFPU)
 
 # Note: When linked statically GMP needs to be linked after CLN since CLN
 # depends on GMP.
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 307222988..43bb3d2dc 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -5197,18 +5197,6 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
       << " children (the one under construction has " << nchildren << ")";
 }
 
-/* Solver Configuration                                                       */
-/* -------------------------------------------------------------------------- */
-
-bool Solver::supportsFloatingPoint() const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  //////// all checks before this line
-  return Configuration::isBuiltWithSymFPU();
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 /* Sorts Handling                                                             */
 /* -------------------------------------------------------------------------- */
 
@@ -5276,8 +5264,6 @@ Sort Solver::getRoundingModeSort(void) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   //////// all checks before this line
   return Sort(this, getNodeManager()->roundingModeType());
   ////////
@@ -5314,8 +5300,6 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0";
   CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0";
   //////// all checks before this line
@@ -5794,8 +5778,6 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
       FloatingPoint::makeInf(FloatingPointSize(exp, sig), false));
@@ -5807,8 +5789,6 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
       FloatingPoint::makeInf(FloatingPointSize(exp, sig), true));
@@ -5820,8 +5800,6 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
       FloatingPoint::makeNaN(FloatingPointSize(exp, sig)));
@@ -5833,8 +5811,6 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), false));
@@ -5846,8 +5822,6 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), true));
@@ -5859,8 +5833,6 @@ Term Solver::mkRoundingMode(RoundingMode rm) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   //////// all checks before this line
   return mkValHelper<cvc5::RoundingMode>(s_rmodes.at(rm));
   ////////
@@ -5914,8 +5886,6 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   CVC5_API_SOLVER_CHECK_TERM(val);
   CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0";
   CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0";
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index a1421cf12..161522654 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2751,12 +2751,6 @@ class CVC5_EXPORT Solver
   Solver(const Solver&) = delete;
   Solver& operator=(const Solver&) = delete;
 
-  /* .................................................................... */
-  /* Solver Configuration                                                 */
-  /* .................................................................... */
-
-  bool supportsFloatingPoint() const;
-
   /* .................................................................... */
   /* Sorts Handling                                                       */
   /* .................................................................... */
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index fdc1872e7..9d980267d 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -151,7 +151,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
 
     cdef cppclass Solver:
         Solver(Options*) except +
-        bint supportsFloatingPoint() except +
         Sort getBooleanSort() except +
         Sort getIntegerSort() except +
         Sort getRealSort() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 258005207..874c63c3d 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -460,9 +460,6 @@ cdef class Solver:
     def __dealloc__(self):
         del self.csolver
 
-    def supportsFloatingPoint(self):
-        return self.csolver.supportsFloatingPoint()
-
     def getBooleanSort(self):
         cdef Sort sort = Sort(self)
         sort.csort = self.csolver.getBooleanSort()
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 61951841b..1befb34ea 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -123,7 +123,6 @@ std::string Configuration::copyright() {
   if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCadical()
       || Configuration::isBuiltWithCryptominisat()
       || Configuration::isBuiltWithKissat()
-      || Configuration::isBuiltWithSymFPU()
       || Configuration::isBuiltWithEditline())
   {
     ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n"
@@ -151,12 +150,6 @@ std::string Configuration::copyright() {
          << "  See https://fmv.jku.at/kissat for copyright "
          << "information.\n\n";
     }
-    if (Configuration::isBuiltWithSymFPU())
-    {
-      ss << "  SymFPU - The Symbolic Floating Point Unit\n"
-         << "  See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright "
-         << "information.\n\n";
-    }
     if (Configuration::isBuiltWithEditline())
     {
       ss << "  Editline Library\n"
@@ -165,6 +158,10 @@ std::string Configuration::copyright() {
     }
   }
 
+  ss << "  SymFPU - The Symbolic Floating Point Unit\n"
+     << "  See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright "
+     << "information.\n\n";
+
   if (Configuration::isBuiltWithGmp() || Configuration::isBuiltWithPoly())
   {
     ss << "This version of cvc5 is linked against the following third party\n"
@@ -259,8 +256,6 @@ bool Configuration::isBuiltWithPoly()
   return IS_POLY_BUILD;
 }
 
-bool Configuration::isBuiltWithSymFPU() { return IS_SYMFPU_BUILD; }
-
 unsigned Configuration::getNumDebugTags() {
 #if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
   /* -1 because a NULL pointer is inserted as the last value */
diff --git a/src/base/configuration.h b/src/base/configuration.h
index 78e86f920..2a7df1b4a 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -113,8 +113,6 @@ public:
 
   static bool isBuiltWithPoly();
 
-  static bool isBuiltWithSymFPU();
-
   /* Return the number of debug tags */
   static unsigned getNumDebugTags();
   /* Return a sorted array of the debug tags name */
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 3027b23bc..39c5e89e9 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -126,12 +126,6 @@ namespace cvc5 {
 #define IS_EDITLINE_BUILD false
 #endif /* HAVE_LIBEDITLINE */
 
-#ifdef CVC5_USE_SYMFPU
-#define IS_SYMFPU_BUILD true
-#else /* HAVE_SYMFPU_HEADERS */
-#define IS_SYMFPU_BUILD false
-#endif /* HAVE_SYMFPU_HEADERS */
-
 #if CVC5_GPL_DEPS
 #  define IS_GPL_BUILD true
 #else /* CVC5_GPL_DEPS */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index e109ab44c..d31d2e58f 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -403,7 +403,6 @@ void OptionsHandler::showConfiguration(const std::string& option,
   print_config_cond("kissat", Configuration::isBuiltWithKissat());
   print_config_cond("poly", Configuration::isBuiltWithPoly());
   print_config_cond("editline", Configuration::isBuiltWithEditline());
-  print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
 
   exit(0);
 }
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 0d1b25549..0e196c0e0 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -23,7 +23,6 @@
 #include "util/floatingpoint.h"
 #include "util/floatingpoint_literal_symfpu.h"
 
-#ifdef CVC5_USE_SYMFPU
 #include "symfpu/core/add.h"
 #include "symfpu/core/classify.h"
 #include "symfpu/core/compare.h"
@@ -38,9 +37,7 @@
 #include "symfpu/core/sqrt.h"
 #include "symfpu/utils/numberOfRoundingModes.h"
 #include "symfpu/utils/properties.h"
-#endif
 
-#ifdef CVC5_USE_SYMFPU
 namespace symfpu {
 using namespace ::cvc5::theory::fp::symfpuSymbolic;
 
@@ -143,11 +140,6 @@ void probabilityAnnotation<traits, traits::prop>(const traits::prop &p,
   return;
 }
 };
-#endif
-
-#ifndef CVC5_USE_SYMFPU
-#define SYMFPU_NUMBER_OF_ROUNDING_MODES 5
-#endif
 
 namespace cvc5 {
 namespace theory {
@@ -242,11 +234,7 @@ symbolicProposition symbolicProposition::operator^(
 
 bool symbolicRoundingMode::checkNodeType(const TNode n)
 {
-#ifdef CVC5_USE_SYMFPU
   return n.getType(false).isBitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES);
-#else
-  return false;
-#endif
 }
 
 symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n)
@@ -254,7 +242,6 @@ symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n)
   Assert(checkNodeType(*this));
 }
 
-#ifdef CVC5_USE_SYMFPU
 symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
     : nodeWrapper(NodeManager::currentNM()->mkConst(
           BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
@@ -262,14 +249,6 @@ symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
   Assert((v & (v - 1)) == 0 && v != 0);  // Exactly one bit set
   Assert(checkNodeType(*this));
 }
-#else
-symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
-    : nodeWrapper(NodeManager::currentNM()->mkConst(
-          BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
-{
-  Unreachable();
-}
-#endif
 
 symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old)
     : nodeWrapper(old)
@@ -755,20 +734,17 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const
 
 FpConverter::FpConverter(context::UserContext* user)
     : d_additionalAssertions(user)
-#ifdef CVC5_USE_SYMFPU
       ,
       d_fpMap(user),
       d_rmMap(user),
       d_boolMap(user),
       d_ubvMap(user),
       d_sbvMap(user)
-#endif
 {
 }
 
 FpConverter::~FpConverter() {}
 
-#ifdef CVC5_USE_SYMFPU
 Node FpConverter::ufToNode(const fpt &format, const uf &u) const
 {
   NodeManager *nm = NodeManager::currentNM();
@@ -843,7 +819,6 @@ FpConverter::uf FpConverter::buildComponents(TNode current)
 
   return tmp;
 }
-#endif
 
 // Non-convertible things should only be added to the stack at the very start,
 // thus...
@@ -851,7 +826,6 @@ FpConverter::uf FpConverter::buildComponents(TNode current)
 
 Node FpConverter::convert(TNode node)
 {
-#ifdef CVC5_USE_SYMFPU
   std::vector<TNode> workStack;
   TNode result = node;
 
@@ -1704,9 +1678,6 @@ Node FpConverter::convert(TNode node)
   }
 
   return result;
-#else
-  Unimplemented() << "Conversion is dependent on SymFPU";
-#endif
 }
 
 #undef CVC5_FPCONV_PASSTHROUGH
@@ -1715,7 +1686,6 @@ Node FpConverter::getValue(Valuation &val, TNode var)
 {
   Assert(Theory::isLeafOf(var, THEORY_FP));
 
-#ifdef CVC5_USE_SYMFPU
   TypeNode t(var.getType());
 
   Assert(t.isRoundingMode() || t.isFloatingPoint())
@@ -1735,9 +1705,6 @@ Node FpConverter::getValue(Valuation &val, TNode var)
   Assert(i != d_fpMap.end())
       << "Asking for the value of an unregistered expression";
   return ufToNode(fpt(t), (*i).second);
-#else
-  Unimplemented() << "Conversion is dependent on SymFPU";
-#endif
 }
 
 }  // namespace fp
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index f1b7c8a83..9900c2987 100644
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -33,9 +33,7 @@
 #include "util/floatingpoint_size.h"
 #include "util/hash.h"
 
-#ifdef CVC5_USE_SYMFPU
 #include "symfpu/core/unpackedFloat.h"
-#endif
 
 #ifdef CVC5_SYM_SYMBOLIC_EVAL
 // This allows debugging of the cvc5 symbolic back-end.
@@ -120,9 +118,7 @@ class symbolicProposition : public nodeWrapper
  protected:
   bool checkNodeType(const TNode node);
 
-#ifdef CVC5_USE_SYMFPU
   friend ::symfpu::ite<symbolicProposition, symbolicProposition>;  // For ITE
-#endif
 
  public:
   symbolicProposition(const Node n);
@@ -141,9 +137,7 @@ class symbolicRoundingMode : public nodeWrapper
  protected:
   bool checkNodeType(const TNode n);
 
-#ifdef CVC5_USE_SYMFPU
   friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>;  // For ITE
-#endif
 
  public:
   symbolicRoundingMode(const Node n);
@@ -183,10 +177,8 @@ class symbolicBitVector : public nodeWrapper
   bool checkNodeType(const TNode n);
   friend symbolicBitVector<!isSigned>;  // To allow conversion between the types
 
-#ifdef CVC5_USE_SYMFPU
   friend ::symfpu::ite<symbolicProposition,
                        symbolicBitVector<isSigned> >;  // For ITE
-#endif
 
  public:
   symbolicBitVector(const Node n);
@@ -314,7 +306,6 @@ class FpConverter
   context::CDList<Node> d_additionalAssertions;
 
  protected:
-#ifdef CVC5_USE_SYMFPU
   typedef symfpuSymbolic::traits traits;
   typedef ::symfpu::unpackedFloat<symfpuSymbolic::traits> uf;
   typedef symfpuSymbolic::traits::rm rm;
@@ -348,7 +339,6 @@ class FpConverter
 
   /* Creates the relevant components for a variable */
   uf buildComponents(TNode current);
-#endif
 };
 
 }  // namespace fp
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 3d81a2995..77dba0724 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -661,7 +661,7 @@ bool TheoryFp::isRegistered(TNode node) {
 
 void TheoryFp::preRegisterTerm(TNode node)
 {
-  if (Configuration::isBuiltWithSymFPU() && !options::fpExp())
+  if (!options::fpExp())
   {
     TypeNode tn = node.getType();
     if (tn.isFloatingPoint())
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 76f7d55cf..8bc7900de 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -1026,12 +1026,10 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
     bool result;
     switch (k)
     {
-#ifdef CVC5_USE_SYMFPU
       case kind::FLOATINGPOINT_COMPONENT_NAN: result = arg0.isNaN(); break;
       case kind::FLOATINGPOINT_COMPONENT_INF: result = arg0.isInfinite(); break;
       case kind::FLOATINGPOINT_COMPONENT_ZERO: result = arg0.isZero(); break;
       case kind::FLOATINGPOINT_COMPONENT_SIGN: result = arg0.getSign(); break;
-#endif
       default: Unreachable() << "Unknown kind used in componentFlag"; break;
     }
 
@@ -1050,11 +1048,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
     // \todo Add a proper interface for this sort of thing to FloatingPoint #1915
     return RewriteResponse(
         REWRITE_DONE,
-#ifdef CVC5_USE_SYMFPU
         NodeManager::currentNM()->mkConst((BitVector)arg0.getExponent())
-#else
-        node
-#endif
     );
   }
 
@@ -1066,11 +1060,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
     return RewriteResponse(
         REWRITE_DONE,
-#ifdef CVC5_USE_SYMFPU
         NodeManager::currentNM()->mkConst((BitVector)arg0.getSignificand())
-#else
-        node
-#endif
     );
   }
 
@@ -1080,7 +1070,6 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
     BitVector value;
 
-#ifdef CVC5_USE_SYMFPU
     /* \todo fix the numbering of rounding modes so this doesn't need
      * to call symfpu at all and remove the dependency on fp_converter.h #1915 */
     RoundingMode arg0(node[0].getConst<RoundingMode>());
@@ -1110,9 +1099,6 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
         Unreachable() << "Unknown rounding mode in roundingModeBitBlast";
         break;
     }
-#else
-    value = BitVector(5U, 0U);
-#endif
     return RewriteResponse(REWRITE_DONE,
                            NodeManager::currentNM()->mkConst(value));
   }
diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp
index b78ef24c7..77c1ef8f0 100644
--- a/src/theory/fp/theory_fp_type_rules.cpp
+++ b/src/theory/fp/theory_fp_type_rules.cpp
@@ -727,7 +727,6 @@ TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager,
     }
   }
 
-#ifdef CVC5_USE_SYMFPU
   /* Need to create some symfpu objects as the size of bit-vector
    * that is needed for this component is dependent on the encoding
    * used (i.e. whether subnormals are forcibly normalised or not).
@@ -735,9 +734,6 @@ TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager,
    * back-end but it should't make a difference. */
   FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
   uint32_t bw = FloatingPoint::getUnpackedExponentWidth(fps);
-#else
-  uint32_t bw = 2;
-#endif
   return nodeManager->mkBitVectorType(bw);
 }
 
@@ -767,13 +763,9 @@ TypeNode FloatingPointComponentSignificand::computeType(
     }
   }
 
-#ifdef CVC5_USE_SYMFPU
   /* As before we need to use some of sympfu. */
   FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
   uint32_t bw = FloatingPoint::getUnpackedSignificandWidth(fps);
-#else
-  uint32_t bw = 1;
-#endif
   return nodeManager->mkBitVectorType(bw);
 }
 
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 8ba43aa1a..d53b06151 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -44,10 +44,6 @@ LogicInfo::LogicInfo()
 {
   for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id)
   {
-    if (id == THEORY_FP && !Configuration::isBuiltWithSymFPU())
-    {
-      continue;
-    }
     enableTheory(id);
   }
 }
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 2938ddcca..71742dfce 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -13,9 +13,6 @@
 # The build system configuration.
 ##
 
-configure_file(floatingpoint_literal_symfpu.h.in floatingpoint_literal_symfpu.h)
-configure_file(floatingpoint_literal_symfpu_traits.h.in
-               floatingpoint_literal_symfpu_traits.h)
 configure_file(rational.h.in rational.h)
 configure_file(integer.h.in integer.h)
 configure_file(real_algebraic_number.h.in real_algebraic_number.h)
diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp
index c2c3fe77b..dc3dce6b9 100644
--- a/src/util/floatingpoint_literal_symfpu.cpp
+++ b/src/util/floatingpoint_literal_symfpu.cpp
@@ -16,7 +16,6 @@
 
 #include "base/check.h"
 
-#ifdef CVC5_USE_SYMFPU
 #include "symfpu/core/add.h"
 #include "symfpu/core/classify.h"
 #include "symfpu/core/compare.h"
@@ -31,11 +30,9 @@
 #include "symfpu/core/sqrt.h"
 #include "symfpu/utils/numberOfRoundingModes.h"
 #include "symfpu/utils/properties.h"
-#endif
 
 /* -------------------------------------------------------------------------- */
 
-#ifdef CVC5_USE_SYMFPU
 namespace symfpu {
 
 #define CVC5_LIT_ITE_DFN(T)                                            \
@@ -57,7 +54,6 @@ CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::ubv);
 
 #undef CVC5_LIT_ITE_DFN
 }  // namespace symfpu
-#endif
 
 /* -------------------------------------------------------------------------- */
 
@@ -65,44 +61,30 @@ namespace cvc5 {
 
 uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size)
 {
-#ifdef CVC5_USE_SYMFPU
   return SymFPUUnpackedFloatLiteral::exponentWidth(size);
-#else
-  unimplemented();
-  return 2;
-#endif
 }
 
 uint32_t FloatingPointLiteral::getUnpackedSignificandWidth(
     FloatingPointSize& size)
 {
-#ifdef CVC5_USE_SYMFPU
   return SymFPUUnpackedFloatLiteral::significandWidth(size);
-#else
-  unimplemented();
-  return 2;
-#endif
 }
 
 FloatingPointLiteral::FloatingPointLiteral(uint32_t exp_size,
                                            uint32_t sig_size,
                                            const BitVector& bv)
     : d_fp_size(exp_size, sig_size)
-#ifdef CVC5_USE_SYMFPU
       ,
       d_symuf(symfpu::unpack<symfpuLiteral::traits>(
           symfpuLiteral::Cvc5FPSize(exp_size, sig_size), bv))
-#endif
 {
 }
 
 FloatingPointLiteral::FloatingPointLiteral(
     const FloatingPointSize& size, FloatingPointLiteral::SpecialConstKind kind)
     : d_fp_size(size)
-#ifdef CVC5_USE_SYMFPU
       ,
       d_symuf(SymFPUUnpackedFloatLiteral::makeNaN(size))
-#endif
 {
   Assert(kind == FloatingPointLiteral::SpecialConstKind::FPNAN);
 }
@@ -112,12 +94,10 @@ FloatingPointLiteral::FloatingPointLiteral(
     FloatingPointLiteral::SpecialConstKind kind,
     bool sign)
     : d_fp_size(size)
-#ifdef CVC5_USE_SYMFPU
       ,
       d_symuf(kind == FloatingPointLiteral::SpecialConstKind::FPINF
                   ? SymFPUUnpackedFloatLiteral::makeInf(size, sign)
                   : SymFPUUnpackedFloatLiteral::makeZero(size, sign))
-#endif
 {
   Assert(kind == FloatingPointLiteral::SpecialConstKind::FPINF
          || kind == FloatingPointLiteral::SpecialConstKind::FPZERO);
@@ -126,10 +106,8 @@ FloatingPointLiteral::FloatingPointLiteral(
 FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
                                            const BitVector& bv)
     : d_fp_size(size)
-#ifdef CVC5_USE_SYMFPU
       ,
       d_symuf(symfpu::unpack<symfpuLiteral::traits>(size, bv))
-#endif
 {
 }
 
@@ -138,7 +116,6 @@ FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
                                            const BitVector& bv,
                                            bool signedBV)
     : d_fp_size(size)
-#ifdef CVC5_USE_SYMFPU
       ,
       d_symuf(signedBV ? symfpu::convertSBVToFloat<symfpuLiteral::traits>(
                   symfpuLiteral::Cvc5FPSize(size),
@@ -148,97 +125,61 @@ FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
                            symfpuLiteral::Cvc5FPSize(size),
                            symfpuLiteral::Cvc5RM(rm),
                            symfpuLiteral::Cvc5UnsignedBitVector(bv)))
-#endif
 {
 }
 
 BitVector FloatingPointLiteral::pack(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_symuf));
-#else
-  unimplemented();
-  BitVector bv(4u, 0u);
-#endif
   return bv;
 }
 
 FloatingPointLiteral FloatingPointLiteral::absolute(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return FloatingPointLiteral(
       d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::negate(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return FloatingPointLiteral(
       d_fp_size, symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::add(
     const RoundingMode& rm, const FloatingPointLiteral& arg) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return FloatingPointLiteral(d_fp_size,
                               symfpu::add<symfpuLiteral::traits>(
                                   d_fp_size, rm, d_symuf, arg.d_symuf, true));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::sub(
     const RoundingMode& rm, const FloatingPointLiteral& arg) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return FloatingPointLiteral(d_fp_size,
                               symfpu::add<symfpuLiteral::traits>(
                                   d_fp_size, rm, d_symuf, arg.d_symuf, false));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::mult(
     const RoundingMode& rm, const FloatingPointLiteral& arg) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return FloatingPointLiteral(d_fp_size,
                               symfpu::multiply<symfpuLiteral::traits>(
                                   d_fp_size, rm, d_symuf, arg.d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::div(
     const RoundingMode& rm, const FloatingPointLiteral& arg) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return FloatingPointLiteral(d_fp_size,
                               symfpu::divide<symfpuLiteral::traits>(
                                   d_fp_size, rm, d_symuf, arg.d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::fma(
@@ -246,276 +187,150 @@ FloatingPointLiteral FloatingPointLiteral::fma(
     const FloatingPointLiteral& arg1,
     const FloatingPointLiteral& arg2) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg1.d_fp_size);
   Assert(d_fp_size == arg2.d_fp_size);
   return FloatingPointLiteral(
       d_fp_size,
       symfpu::fma<symfpuLiteral::traits>(
           d_fp_size, rm, d_symuf, arg1.d_symuf, arg2.d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::sqrt(const RoundingMode& rm) const
 {
-#ifdef CVC5_USE_SYMFPU
   return FloatingPointLiteral(
       d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::rti(const RoundingMode& rm) const
 {
-#ifdef CVC5_USE_SYMFPU
   return FloatingPointLiteral(
       d_fp_size,
       symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::rem(
     const FloatingPointLiteral& arg) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return FloatingPointLiteral(d_fp_size,
                               symfpu::remainder<symfpuLiteral::traits>(
                                   d_fp_size, d_symuf, arg.d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::maxTotal(
     const FloatingPointLiteral& arg, bool zeroCaseLeft) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return FloatingPointLiteral(
       d_fp_size,
       symfpu::max<symfpuLiteral::traits>(
           d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::minTotal(
     const FloatingPointLiteral& arg, bool zeroCaseLeft) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return FloatingPointLiteral(
       d_fp_size,
       symfpu::min<symfpuLiteral::traits>(
           d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 bool FloatingPointLiteral::operator==(const FloatingPointLiteral& fp) const
 {
-#ifdef CVC5_USE_SYMFPU
   return ((d_fp_size == fp.d_fp_size)
           && symfpu::smtlibEqual<symfpuLiteral::traits>(
               d_fp_size, d_symuf, fp.d_symuf));
-#else
-  unimplemented();
-  return ((d_fp_size == fp.d_fp_size));
-#endif
 }
 
 bool FloatingPointLiteral::operator<=(const FloatingPointLiteral& arg) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return symfpu::lessThanOrEqual<symfpuLiteral::traits>(
       d_fp_size, d_symuf, arg.d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::operator<(const FloatingPointLiteral& arg) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return symfpu::lessThan<symfpuLiteral::traits>(
       d_fp_size, d_symuf, arg.d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 BitVector FloatingPointLiteral::getExponent() const
 {
-#ifdef CVC5_USE_SYMFPU
   return d_symuf.exponent;
-#else
-  unimplemented();
-  Unreachable() << "no concrete implementation of FloatingPointLiteral";
-  return BitVector();
-#endif
 }
 
 BitVector FloatingPointLiteral::getSignificand() const
 {
-#ifdef CVC5_USE_SYMFPU
   return d_symuf.significand;
-#else
-  unimplemented();
-  Unreachable() << "no concrete implementation of FloatingPointLiteral";
-  return BitVector();
-#endif
 }
 
 bool FloatingPointLiteral::getSign() const
 {
-#ifdef CVC5_USE_SYMFPU
   return d_symuf.sign;
-#else
-  unimplemented();
-  Unreachable() << "no concrete implementation of FloatingPointLiteral";
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::isNormal(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::isSubnormal(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::isZero(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::isInfinite(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::isNaN(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::isNegative(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::isPositive(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::convert(
     const FloatingPointSize& target, const RoundingMode& rm) const
 {
-#ifdef CVC5_USE_SYMFPU
   return FloatingPointLiteral(
       target,
       symfpu::convertFloatToFloat<symfpuLiteral::traits>(
           d_fp_size, target, rm, d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 BitVector FloatingPointLiteral::convertToSBVTotal(BitVectorSize width,
                                                   const RoundingMode& rm,
                                                   BitVector undefinedCase) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
       d_fp_size, rm, d_symuf, width, undefinedCase);
-#else
-  unimplemented();
-  return undefinedCase;
-#endif
 }
 
 BitVector FloatingPointLiteral::convertToUBVTotal(BitVectorSize width,
                                                   const RoundingMode& rm,
                                                   BitVector undefinedCase) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
       d_fp_size, rm, d_symuf, width, undefinedCase);
-#else
-  unimplemented();
-  return undefinedCase;
-#endif
 }
 
-#ifndef CVC5_USE_SYMFPU
-void FloatingPointLiteral::unimplemented(void)
-{
-  Unimplemented() << "no concrete implementation of FloatingPointLiteral";
-}
-
-size_t FloatingPointLiteral::hash(void) const
-{
-  unimplemented();
-  return 23;
-}
-#endif
-
 }  // namespace cvc5
diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h
similarity index 92%
rename from src/util/floatingpoint_literal_symfpu.h.in
rename to src/util/floatingpoint_literal_symfpu.h
index 54827a308..5b2b0f7c8 100644
--- a/src/util/floatingpoint_literal_symfpu.h.in
+++ b/src/util/floatingpoint_literal_symfpu.h
@@ -20,20 +20,16 @@
 #define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
 
 #include "util/bitvector.h"
-#include "util/floatingpoint_size.h"
 #include "util/floatingpoint_literal_symfpu_traits.h"
+#include "util/floatingpoint_size.h"
 #include "util/roundingmode.h"
 
 /* -------------------------------------------------------------------------- */
 
 namespace cvc5 {
 
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-// clang-format on
 using SymFPUUnpackedFloatLiteral =
     ::symfpu::unpackedFloat<symfpuLiteral::traits>;
-#endif
 
 class FloatingPointLiteral
 {
@@ -65,13 +61,6 @@ class FloatingPointLiteral
    */
   static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size);
 
-// clang-format off
-#if !@CVC5_USE_SYMFPU@
-  // clang-format on
-  /** Catch-all for unimplemented functions. */
-  static void unimplemented(void);
-#endif
-
   /** Constructors. */
 
   /** Create a FP literal from its IEEE bit-vector representation. */
@@ -197,18 +186,10 @@ class FloatingPointLiteral
   BitVector convertToUBVTotal(BitVectorSize width,
                               const RoundingMode& rm,
                               BitVector undefinedCase) const;
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-  // clang-format on
   /** Return wrapped floating-point literal. */
   const SymFPUUnpackedFloatLiteral& getSymUF() const { return d_symuf; }
-#else
-  /** Dummy hash function. */
-  size_t hash(void) const;
-#endif
 
  private:
-
   /**
    * Create a FP literal from unpacked representation.
    *
@@ -223,34 +204,19 @@ class FloatingPointLiteral
                        const bool sign,
                        const BitVector& exp,
                        const BitVector& sig)
-      : d_fp_size(size)
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-        // clang-format on
-        ,
-        d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig))
-#endif
+      : d_fp_size(size), d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig))
   {
   }
 
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-  // clang-format on
-
   /** Create a FP literal from a symFPU unpacked float. */
   FloatingPointLiteral(const FloatingPointSize& size,
                        SymFPUUnpackedFloatLiteral symuf)
       : d_fp_size(size), d_symuf(symuf){};
-#endif
 
   /** The floating-point size of this floating-point literal. */
   FloatingPointSize d_fp_size;
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-  // clang-format on
   /** The actual floating-point value, a SymFPU unpackedFloat. */
   SymFPUUnpackedFloatLiteral d_symuf;
-#endif
 };
 
 /* -------------------------------------------------------------------------- */
diff --git a/src/util/floatingpoint_literal_symfpu_traits.cpp b/src/util/floatingpoint_literal_symfpu_traits.cpp
index 071b69912..0f46708b0 100644
--- a/src/util/floatingpoint_literal_symfpu_traits.cpp
+++ b/src/util/floatingpoint_literal_symfpu_traits.cpp
@@ -13,8 +13,6 @@
  * SymFPU glue code for floating-point values.
  */
 
-#if CVC5_USE_SYMFPU
-
 #include "util/floatingpoint_literal_symfpu_traits.h"
 
 #include "base/check.h"
@@ -413,4 +411,3 @@ void traits::invariant(const traits::prop& p)
 }
 }  // namespace symfpuLiteral
 }  // namespace cvc5
-#endif
diff --git a/src/util/floatingpoint_literal_symfpu_traits.h.in b/src/util/floatingpoint_literal_symfpu_traits.h
similarity index 99%
rename from src/util/floatingpoint_literal_symfpu_traits.h.in
rename to src/util/floatingpoint_literal_symfpu_traits.h
index 76d2f47e2..bc5caaf88 100644
--- a/src/util/floatingpoint_literal_symfpu_traits.h.in
+++ b/src/util/floatingpoint_literal_symfpu_traits.h
@@ -25,16 +25,12 @@
 #ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
 #define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
 
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-// clang-format on
+#include <symfpu/core/unpackedFloat.h>
 
 #include "util/bitvector.h"
 #include "util/floatingpoint_size.h"
 #include "util/roundingmode.h"
 
-#include <symfpu/core/unpackedFloat.h>
-
 /* -------------------------------------------------------------------------- */
 
 namespace cvc5 {
@@ -258,7 +254,6 @@ class wrappedBitVector : public BitVector
                                      Cvc5BitWidth lower) const;
 };
 }  // namespace symfpuLiteral
-}
+}  // namespace cvc5
 
 #endif
-#endif
diff --git a/test/api/issue4889.cpp b/test/api/issue4889.cpp
index f84d99f42..8e0853682 100644
--- a/test/api/issue4889.cpp
+++ b/test/api/issue4889.cpp
@@ -19,7 +19,6 @@ using namespace cvc5::api;
 
 int main()
 {
-#ifdef CVC5_USE_SYMFPU
   Solver slv;
   Sort sort_int = slv.getIntegerSort();
   Sort sort_array = slv.mkArraySort(sort_int, sort_int);
@@ -33,6 +32,5 @@ int main()
   Term rem = slv.mkTerm(FLOATINGPOINT_REM, ite, const1);
   Term isnan = slv.mkTerm(FLOATINGPOINT_ISNAN, rem);
   slv.checkSatAssuming(isnan);
-#endif
   return 0;
 }
diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index 44ce684dd..1255bf270 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -32,11 +32,7 @@ def test_recoverable_exception(solver):
 
 
 def test_supports_floating_point(solver):
-    if solver.supportsFloatingPoint():
-        solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
+    solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
 
 
 def test_get_boolean_sort(solver):
@@ -60,11 +56,7 @@ def test_get_string_sort(solver):
 
 
 def test_get_rounding_mode_sort(solver):
-    if solver.supportsFloatingPoint():
-        solver.getRoundingModeSort()
-    else:
-        with pytest.raises(RuntimeError):
-            solver.getRoundingModeSort()
+    solver.getRoundingModeSort()
 
 
 def test_mk_array_sort(solver):
@@ -79,10 +71,9 @@ def test_mk_array_sort(solver):
     solver.mkArraySort(boolSort, intSort)
     solver.mkArraySort(realSort, bvSort)
 
-    if (solver.supportsFloatingPoint()):
-        fpSort = solver.mkFloatingPointSort(3, 5)
-        solver.mkArraySort(fpSort, fpSort)
-        solver.mkArraySort(bvSort, fpSort)
+    fpSort = solver.mkFloatingPointSort(3, 5)
+    solver.mkArraySort(fpSort, fpSort)
+    solver.mkArraySort(bvSort, fpSort)
 
     slv = pycvc5.Solver()
     with pytest.raises(RuntimeError):
@@ -96,15 +87,11 @@ def test_mk_bit_vector_sort(solver):
 
 
 def test_mk_floating_point_sort(solver):
-    if solver.supportsFloatingPoint():
-        solver.mkFloatingPointSort(4, 8)
-        with pytest.raises(RuntimeError):
-            solver.mkFloatingPointSort(0, 8)
-        with pytest.raises(RuntimeError):
-            solver.mkFloatingPointSort(4, 0)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkFloatingPointSort(4, 8)
+    solver.mkFloatingPointSort(4, 8)
+    with pytest.raises(RuntimeError):
+        solver.mkFloatingPointSort(0, 8)
+    with pytest.raises(RuntimeError):
+        solver.mkFloatingPointSort(4, 0)
 
 
 def test_mk_datatype_sort(solver):
@@ -313,11 +300,7 @@ def test_mk_boolean(solver):
 
 
 def test_mk_rounding_mode(solver):
-    if solver.supportsFloatingPoint():
-        solver.mkRoundingMode(pycvc5.RoundTowardZero)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkRoundingMode(pycvc5.RoundTowardZero)
+    solver.mkRoundingMode(pycvc5.RoundTowardZero)
 
 
 def test_mk_uninterpreted_const(solver):
@@ -333,11 +316,7 @@ def test_mk_floating_point(solver):
     t1 = solver.mkBitVector(8)
     t2 = solver.mkBitVector(4)
     t3 = solver.mkInteger(2)
-    if (solver.supportsFloatingPoint()):
-        solver.mkFloatingPoint(3, 5, t1)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkFloatingPoint(3, 5, t1)
+    solver.mkFloatingPoint(3, 5, t1)
 
     with pytest.raises(RuntimeError):
         solver.mkFloatingPoint(0, 5, pycvc5.Term(solver))
@@ -350,10 +329,9 @@ def test_mk_floating_point(solver):
     with pytest.raises(RuntimeError):
         solver.mkFloatingPoint(3, 5, t2)
 
-    if (solver.supportsFloatingPoint()):
-        slv = pycvc5.Solver()
-        with pytest.raises(RuntimeError):
-            slv.mkFloatingPoint(3, 5, t1)
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkFloatingPoint(3, 5, t1)
 
 
 def test_mk_empty_set(solver):
@@ -382,43 +360,23 @@ def test_mk_false(solver):
 
 
 def test_mk_nan(solver):
-    if (solver.supportsFloatingPoint()):
-        solver.mkNaN(3, 5)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkNaN(3, 5)
+    solver.mkNaN(3, 5)
 
 
 def test_mk_neg_zero(solver):
-    if (solver.supportsFloatingPoint()):
-        solver.mkNegZero(3, 5)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkNegZero(3, 5)
+    solver.mkNegZero(3, 5)
 
 
 def test_mk_neg_inf(solver):
-    if (solver.supportsFloatingPoint()):
-        solver.mkNegInf(3, 5)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkNegInf(3, 5)
+    solver.mkNegInf(3, 5)
 
 
 def test_mk_pos_inf(solver):
-    if (solver.supportsFloatingPoint()):
-        solver.mkPosInf(3, 5)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkPosInf(3, 5)
+    solver.mkPosInf(3, 5)
 
 
 def test_mk_pos_zero(solver):
-    if (solver.supportsFloatingPoint()):
-        solver.mkPosZero(3, 5)
-    else:
-        with pytest.raises(RuntimeError):
-            solver.mkPosZero(3, 5)
+    solver.mkPosZero(3, 5)
 
 
 def test_mk_pi(solver):
diff --git a/test/python/unit/api/test_sort.py b/test/python/unit/api/test_sort.py
index 5e86382ee..def539cf4 100644
--- a/test/python/unit/api/test_sort.py
+++ b/test/python/unit/api/test_sort.py
@@ -89,9 +89,8 @@ def test_is_reg_exp(solver):
 
 
 def test_is_rounding_mode(solver):
-    if solver.supportsFloatingPoint():
-        assert solver.getRoundingModeSort().isRoundingMode()
-        Sort(solver).isRoundingMode()
+    assert solver.getRoundingModeSort().isRoundingMode()
+    Sort(solver).isRoundingMode()
 
 
 def test_is_bit_vector(solver):
@@ -100,9 +99,8 @@ def test_is_bit_vector(solver):
 
 
 def test_is_floating_point(solver):
-    if solver.supportsFloatingPoint():
-        assert solver.mkFloatingPointSort(8, 24).isFloatingPoint()
-        Sort(solver).isFloatingPoint()
+    assert solver.mkFloatingPointSort(8, 24).isFloatingPoint()
+    Sort(solver).isFloatingPoint()
 
 
 def test_is_datatype(solver):
@@ -447,21 +445,19 @@ def test_get_bv_size(solver):
 
 
 def test_get_fp_exponent_size(solver):
-    if solver.supportsFloatingPoint():
-        fpSort = solver.mkFloatingPointSort(4, 8)
-        fpSort.getFPExponentSize()
-        setSort = solver.mkSetSort(solver.getIntegerSort())
-        with pytest.raises(RuntimeError):
-            setSort.getFPExponentSize()
+    fpSort = solver.mkFloatingPointSort(4, 8)
+    fpSort.getFPExponentSize()
+    setSort = solver.mkSetSort(solver.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        setSort.getFPExponentSize()
 
 
 def test_get_fp_significand_size(solver):
-    if solver.supportsFloatingPoint():
-        fpSort = solver.mkFloatingPointSort(4, 8)
-        fpSort.getFPSignificandSize()
-        setSort = solver.mkSetSort(solver.getIntegerSort())
-        with pytest.raises(RuntimeError):
-            setSort.getFPSignificandSize()
+    fpSort = solver.mkFloatingPointSort(4, 8)
+    fpSort.getFPSignificandSize()
+    setSort = solver.mkSetSort(solver.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        setSort.getFPSignificandSize()
 
 
 def test_get_datatype_paramsorts(solver):
diff --git a/test/regress/README.md b/test/regress/README.md
index efd79472b..ca6fc30ab 100644
--- a/test/regress/README.md
+++ b/test/regress/README.md
@@ -115,11 +115,11 @@ configurations. The `REQUIRES` directive can be used to only run
 a given benchmark when a feature is supported. For example:
 
 ```
-; REQUIRES: symfpu
+; REQUIRES: cryptominisat
 ```
 
-This benchmark is only run when symfpu has been configured.  Multiple
+This benchmark is only run when CryptoMiniSat has been configured.  Multiple
 `REQUIRES` directives are supported. For a list of features that can be listed
 as a requirement, refer to cvc5's `--show-config` output. Features can also be
-excluded by adding the `no-` prefix, e.g. `no-symfpu` means that the test is
-not valid for builds that include symfpu support.
+excluded by adding the `no-` prefix, e.g. `no-cryptominisat` means that the
+test is not valid for builds that include CryptoMiniSat support.
diff --git a/test/regress/regress0/fp/abs-unsound.smt2 b/test/regress/regress0/fp/abs-unsound.smt2
index b5aa0452e..ae7117047 100644
--- a/test/regress/regress0/fp/abs-unsound.smt2
+++ b/test/regress/regress0/fp/abs-unsound.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; COMMAND-LINE: --fp-exp
 ; EXPECT: sat
 (set-logic QF_FP)
diff --git a/test/regress/regress0/fp/abs-unsound2.smt2 b/test/regress/regress0/fp/abs-unsound2.smt2
index ad603f8c9..3040f9ba9 100644
--- a/test/regress/regress0/fp/abs-unsound2.smt2
+++ b/test/regress/regress0/fp/abs-unsound2.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; COMMAND-LINE: --fp-exp
 ; EXPECT: unsat
 (set-logic QF_FP)
diff --git a/test/regress/regress0/fp/down-cast-RNA.smt2 b/test/regress/regress0/fp/down-cast-RNA.smt2
index dc99ff144..62314f284 100644
--- a/test/regress/regress0/fp/down-cast-RNA.smt2
+++ b/test/regress/regress0/fp/down-cast-RNA.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; COMMAND-LINE: --fp-exp
 ; EXPECT: unsat
 
diff --git a/test/regress/regress0/fp/ext-rew-test.smt2 b/test/regress/regress0/fp/ext-rew-test.smt2
index 726487e18..3fb3a9e53 100644
--- a/test/regress/regress0/fp/ext-rew-test.smt2
+++ b/test/regress/regress0/fp/ext-rew-test.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg
 ; EXPECT: unsat
 (set-info :smt-lib-version 2.6)
diff --git a/test/regress/regress0/fp/from_sbv.smt2 b/test/regress/regress0/fp/from_sbv.smt2
index 3211339d6..226d6589c 100644
--- a/test/regress/regress0/fp/from_sbv.smt2
+++ b/test/regress/regress0/fp/from_sbv.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; COMMAND-LINE: --fp-exp
 ; EXPECT: unsat
 (set-logic QF_BVFP)
diff --git a/test/regress/regress0/fp/from_ubv.smt2 b/test/regress/regress0/fp/from_ubv.smt2
index c02f8d304..6939e478a 100644
--- a/test/regress/regress0/fp/from_ubv.smt2
+++ b/test/regress/regress0/fp/from_ubv.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; EXPECT: unsat
 (set-logic QF_FP)
 (declare-const r RoundingMode)
diff --git a/test/regress/regress0/fp/issue-5524.smt2 b/test/regress/regress0/fp/issue-5524.smt2
index 8c361163c..741d77a19 100644
--- a/test/regress/regress0/fp/issue-5524.smt2
+++ b/test/regress/regress0/fp/issue-5524.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; EXPECT: unsat
 (set-logic QF_FP)
 (declare-fun fpv5 () Float32)
diff --git a/test/regress/regress0/fp/issue3536.smt2 b/test/regress/regress0/fp/issue3536.smt2
index 68a17347e..6a58b371f 100644
--- a/test/regress/regress0/fp/issue3536.smt2
+++ b/test/regress/regress0/fp/issue3536.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic QF_FP)
diff --git a/test/regress/regress0/fp/issue3582.smt2 b/test/regress/regress0/fp/issue3582.smt2
index 2de76b680..c06cdb110 100644
--- a/test/regress/regress0/fp/issue3582.smt2
+++ b/test/regress/regress0/fp/issue3582.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; EXPECT: unsat
 (set-logic QF_FP)
 (declare-fun bv () (_ BitVec 1))
diff --git a/test/regress/regress0/fp/issue3619.smt2 b/test/regress/regress0/fp/issue3619.smt2
index 3e0858035..ab3c781bb 100644
--- a/test/regress/regress0/fp/issue3619.smt2
+++ b/test/regress/regress0/fp/issue3619.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic QF_FPLRA)
diff --git a/test/regress/regress0/fp/issue4277-assign-func.smt2 b/test/regress/regress0/fp/issue4277-assign-func.smt2
index c42bad235..d1fbc73d2 100644
--- a/test/regress/regress0/fp/issue4277-assign-func.smt2
+++ b/test/regress/regress0/fp/issue4277-assign-func.smt2
@@ -1,6 +1,5 @@
 ; COMMAND-LINE: -q
 ; EXPECT: sat
-; REQUIRES: symfpu
 (set-logic HO_ALL)
 (set-option :assign-function-values false)
 (set-info :status sat)
diff --git a/test/regress/regress0/fp/issue5511.smt2 b/test/regress/regress0/fp/issue5511.smt2
index d4393486c..911db54ee 100644
--- a/test/regress/regress0/fp/issue5511.smt2
+++ b/test/regress/regress0/fp/issue5511.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; EXPECT: sat
 (set-logic QF_FP)
 (declare-fun a () (_ FloatingPoint 53 11))
diff --git a/test/regress/regress0/fp/issue5734.smt2 b/test/regress/regress0/fp/issue5734.smt2
index 2ad9ac921..d66e6aec7 100644
--- a/test/regress/regress0/fp/issue5734.smt2
+++ b/test/regress/regress0/fp/issue5734.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; EXPECT: sat
 (set-logic QF_FP)
 (declare-fun a () RoundingMode)
diff --git a/test/regress/regress0/fp/issue6164.smt2 b/test/regress/regress0/fp/issue6164.smt2
index 056a98afc..3ec9f1594 100644
--- a/test/regress/regress0/fp/issue6164.smt2
+++ b/test/regress/regress0/fp/issue6164.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; EXPECT: sat
 ; EXPECT: ((((_ to_fp 5 11) roundNearestTiesToAway (/ 1 10)) (fp #b0 #b01011 #b1001100110)))
 (set-logic ALL)
diff --git a/test/regress/regress0/fp/rti_3_5_bug.smt2 b/test/regress/regress0/fp/rti_3_5_bug.smt2
index 2c837b415..724e08b8c 100644
--- a/test/regress/regress0/fp/rti_3_5_bug.smt2
+++ b/test/regress/regress0/fp/rti_3_5_bug.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; COMMAND-LINE: --fp-exp
 ; EXPECT: unsat
 
diff --git a/test/regress/regress0/fp/simple.smt2 b/test/regress/regress0/fp/simple.smt2
index 0b4a11f08..754186943 100644
--- a/test/regress/regress0/fp/simple.smt2
+++ b/test/regress/regress0/fp/simple.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; EXPECT: unsat
 (set-logic QF_FP)    
 (declare-const x Float32)
diff --git a/test/regress/regress0/fp/wrong-model.smt2 b/test/regress/regress0/fp/wrong-model.smt2
index 7694d8a35..298c21b18 100644
--- a/test/regress/regress0/fp/wrong-model.smt2
+++ b/test/regress/regress0/fp/wrong-model.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; COMMAND-LINE: --fp-exp
 ; EXPECT: sat
 
diff --git a/test/regress/regress0/issue5370.smt2 b/test/regress/regress0/issue5370.smt2
index 848567e2c..971602e14 100644
--- a/test/regress/regress0/issue5370.smt2
+++ b/test/regress/regress0/issue5370.smt2
@@ -1,5 +1,4 @@
 ; COMMAND-LINE: --bv-to-bool
-; REQUIRES: symfpu
 (set-logic ALL)
 (set-info :status sat)
 (declare-fun c () (Array (_ BitVec 2) (_ BitVec 1)))
diff --git a/test/regress/regress0/parser/to_fp.smt2 b/test/regress/regress0/parser/to_fp.smt2
index 277209ff8..1cd83816a 100644
--- a/test/regress/regress0/parser/to_fp.smt2
+++ b/test/regress/regress0/parser/to_fp.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; COMMAND-LINE: --strict-parsing -q
 ; EXPECT: sat
 (set-logic QF_FP)
diff --git a/test/regress/regress1/fp/rti_3_5_bug_report.smt2 b/test/regress/regress1/fp/rti_3_5_bug_report.smt2
index 3e94e6e05..6c0b68c95 100644
--- a/test/regress/regress1/fp/rti_3_5_bug_report.smt2
+++ b/test/regress/regress1/fp/rti_3_5_bug_report.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; COMMAND-LINE: --fp-exp
 ; EXPECT: unsat
 
diff --git a/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2 b/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2
index 1ee8e6c11..3ab7495ea 100644
--- a/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2
+++ b/test/regress/regress1/quantifiers/fp-cegqi-unsat.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 (set-info :smt-lib-version 2.6)
 (set-logic FP)
 (set-info :status unsat)
diff --git a/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2
index 796d7e753..d30bd563d 100644
--- a/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2
+++ b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2
@@ -1,5 +1,4 @@
 ; COMMAND-LINE: --no-jh-rlv-order
-; REQUIRES: symfpu
 ; EXPECT: unsat
 (set-logic AUFBVFPDTNIRA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy
index 30828ca76..2970fd0de 100644
--- a/test/regress/regress1/rr-verify/fp-arith.sy
+++ b/test/regress/regress1/rr-verify/fp-arith.sy
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy
index 6704198c3..e4b3a0fac 100644
--- a/test/regress/regress1/rr-verify/fp-bool.sy
+++ b/test/regress/regress1/rr-verify/fp-bool.sy
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
diff --git a/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy b/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy
index fa8bdc2d7..385ade07f 100644
--- a/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy
+++ b/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; EXPECT: unsat
 ; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic ALL)
diff --git a/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 b/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2
index c674c4039..4648c327a 100644
--- a/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2
+++ b/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; COMMAND-LINE: --decision=internal -q
 ; COMMAND-LINE: --decision=justification -q
 ; EXPECT: sat
diff --git a/test/regress/regress2/sygus/min_IC_1.sy b/test/regress/regress2/sygus/min_IC_1.sy
index c0cae0025..8c0e2d82b 100644
--- a/test/regress/regress2/sygus/min_IC_1.sy
+++ b/test/regress/regress2/sygus/min_IC_1.sy
@@ -1,4 +1,3 @@
-; REQUIRES: symfpu
 ; EXPECT: unsat
 ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --fp-exp
 (set-logic ALL)
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 018207293..20e0977f8 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -35,15 +35,7 @@ TEST_F(TestApiBlackSolver, recoverableException)
 
 TEST_F(TestApiBlackSolver, supportsFloatingPoint)
 {
-  if (d_solver.supportsFloatingPoint())
-  {
-    ASSERT_NO_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN));
-  }
-  else
-  {
-    ASSERT_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN),
-                 CVC5ApiException);
-  }
+  ASSERT_NO_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN));
 }
 
 TEST_F(TestApiBlackSolver, getBooleanSort)
@@ -78,14 +70,7 @@ TEST_F(TestApiBlackSolver, getStringSort)
 
 TEST_F(TestApiBlackSolver, getRoundingModeSort)
 {
-  if (d_solver.supportsFloatingPoint())
-  {
-    ASSERT_NO_THROW(d_solver.getRoundingModeSort());
-  }
-  else
-  {
-    ASSERT_THROW(d_solver.getRoundingModeSort(), CVC5ApiException);
-  }
+  ASSERT_NO_THROW(d_solver.getRoundingModeSort());
 }
 
 TEST_F(TestApiBlackSolver, mkArraySort)
@@ -101,12 +86,9 @@ TEST_F(TestApiBlackSolver, mkArraySort)
   ASSERT_NO_THROW(d_solver.mkArraySort(boolSort, intSort));
   ASSERT_NO_THROW(d_solver.mkArraySort(realSort, bvSort));
 
-  if (d_solver.supportsFloatingPoint())
-  {
-    Sort fpSort = d_solver.mkFloatingPointSort(3, 5);
-    ASSERT_NO_THROW(d_solver.mkArraySort(fpSort, fpSort));
-    ASSERT_NO_THROW(d_solver.mkArraySort(bvSort, fpSort));
-  }
+  Sort fpSort = d_solver.mkFloatingPointSort(3, 5);
+  ASSERT_NO_THROW(d_solver.mkArraySort(fpSort, fpSort));
+  ASSERT_NO_THROW(d_solver.mkArraySort(bvSort, fpSort));
 
   Solver slv;
   ASSERT_THROW(slv.mkArraySort(boolSort, boolSort), CVC5ApiException);
@@ -120,16 +102,9 @@ TEST_F(TestApiBlackSolver, mkBitVectorSort)
 
 TEST_F(TestApiBlackSolver, mkFloatingPointSort)
 {
-  if (d_solver.supportsFloatingPoint())
-  {
-    ASSERT_NO_THROW(d_solver.mkFloatingPointSort(4, 8));
-    ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC5ApiException);
-    ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC5ApiException);
-  }
-  else
-  {
-    ASSERT_THROW(d_solver.mkFloatingPointSort(4, 8), CVC5ApiException);
-  }
+  ASSERT_NO_THROW(d_solver.mkFloatingPointSort(4, 8));
+  ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkDatatypeSort)
@@ -377,15 +352,7 @@ TEST_F(TestApiBlackSolver, mkBoolean)
 
 TEST_F(TestApiBlackSolver, mkRoundingMode)
 {
-  if (d_solver.supportsFloatingPoint())
-  {
-    ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
-  }
-  else
-  {
-    ASSERT_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO),
-                 CVC5ApiException);
-  }
+  ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
 }
 
 TEST_F(TestApiBlackSolver, mkUninterpretedConst)
@@ -420,25 +387,15 @@ TEST_F(TestApiBlackSolver, mkFloatingPoint)
   Term t1 = d_solver.mkBitVector(8);
   Term t2 = d_solver.mkBitVector(4);
   Term t3 = d_solver.mkInteger(2);
-  if (d_solver.supportsFloatingPoint())
-  {
-    ASSERT_NO_THROW(d_solver.mkFloatingPoint(3, 5, t1));
-  }
-  else
-  {
-    ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t1), CVC5ApiException);
-  }
+  ASSERT_NO_THROW(d_solver.mkFloatingPoint(3, 5, t1));
   ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, Term()), CVC5ApiException);
   ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, t1), CVC5ApiException);
   ASSERT_THROW(d_solver.mkFloatingPoint(3, 0, t1), CVC5ApiException);
   ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC5ApiException);
   ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC5ApiException);
 
-  if (d_solver.supportsFloatingPoint())
-  {
-    Solver slv;
-    ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC5ApiException);
-  }
+  Solver slv;
+  ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkEmptySet)
@@ -478,64 +435,26 @@ TEST_F(TestApiBlackSolver, mkFalse)
   ASSERT_NO_THROW(d_solver.mkFalse());
 }
 
-TEST_F(TestApiBlackSolver, mkNaN)
-{
-  if (d_solver.supportsFloatingPoint())
-  {
-    ASSERT_NO_THROW(d_solver.mkNaN(3, 5));
-  }
-  else
-  {
-    ASSERT_THROW(d_solver.mkNaN(3, 5), CVC5ApiException);
-  }
-}
+TEST_F(TestApiBlackSolver, mkNaN) { ASSERT_NO_THROW(d_solver.mkNaN(3, 5)); }
 
 TEST_F(TestApiBlackSolver, mkNegZero)
 {
-  if (d_solver.supportsFloatingPoint())
-  {
-    ASSERT_NO_THROW(d_solver.mkNegZero(3, 5));
-  }
-  else
-  {
-    ASSERT_THROW(d_solver.mkNegZero(3, 5), CVC5ApiException);
-  }
+  ASSERT_NO_THROW(d_solver.mkNegZero(3, 5));
 }
 
 TEST_F(TestApiBlackSolver, mkNegInf)
 {
-  if (d_solver.supportsFloatingPoint())
-  {
-    ASSERT_NO_THROW(d_solver.mkNegInf(3, 5));
-  }
-  else
-  {
-    ASSERT_THROW(d_solver.mkNegInf(3, 5), CVC5ApiException);
-  }
+  ASSERT_NO_THROW(d_solver.mkNegInf(3, 5));
 }
 
 TEST_F(TestApiBlackSolver, mkPosInf)
 {
-  if (d_solver.supportsFloatingPoint())
-  {
-    ASSERT_NO_THROW(d_solver.mkPosInf(3, 5));
-  }
-  else
-  {
-    ASSERT_THROW(d_solver.mkPosInf(3, 5), CVC5ApiException);
-  }
+  ASSERT_NO_THROW(d_solver.mkPosInf(3, 5));
 }
 
 TEST_F(TestApiBlackSolver, mkPosZero)
 {
-  if (d_solver.supportsFloatingPoint())
-  {
-    ASSERT_NO_THROW(d_solver.mkPosZero(3, 5));
-  }
-  else
-  {
-    ASSERT_THROW(d_solver.mkPosZero(3, 5), CVC5ApiException);
-  }
+  ASSERT_NO_THROW(d_solver.mkPosZero(3, 5));
 }
 
 TEST_F(TestApiBlackSolver, mkOp)
diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp
index d1b096bda..757bacad6 100644
--- a/test/unit/api/sort_black.cpp
+++ b/test/unit/api/sort_black.cpp
@@ -95,11 +95,8 @@ TEST_F(TestApiBlackSort, isRegExp)
 
 TEST_F(TestApiBlackSort, isRoundingMode)
 {
-  if (d_solver.supportsFloatingPoint())
-  {
-    ASSERT_TRUE(d_solver.getRoundingModeSort().isRoundingMode());
-    ASSERT_NO_THROW(Sort().isRoundingMode());
-  }
+  ASSERT_TRUE(d_solver.getRoundingModeSort().isRoundingMode());
+  ASSERT_NO_THROW(Sort().isRoundingMode());
 }
 
 TEST_F(TestApiBlackSort, isBitVector)
@@ -110,11 +107,8 @@ TEST_F(TestApiBlackSort, isBitVector)
 
 TEST_F(TestApiBlackSort, isFloatingPoint)
 {
-  if (d_solver.supportsFloatingPoint())
-  {
-    ASSERT_TRUE(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint());
-    ASSERT_NO_THROW(Sort().isFloatingPoint());
-  }
+  ASSERT_TRUE(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint());
+  ASSERT_NO_THROW(Sort().isFloatingPoint());
 }
 
 TEST_F(TestApiBlackSort, isDatatype)
@@ -486,24 +480,18 @@ TEST_F(TestApiBlackSort, getBVSize)
 
 TEST_F(TestApiBlackSort, getFPExponentSize)
 {
-  if (d_solver.supportsFloatingPoint())
-  {
-    Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
-    ASSERT_NO_THROW(fpSort.getFPExponentSize());
-    Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-    ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException);
-  }
+  Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
+  ASSERT_NO_THROW(fpSort.getFPExponentSize());
+  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+  ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getFPSignificandSize)
 {
-  if (d_solver.supportsFloatingPoint())
-  {
-    Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
-    ASSERT_NO_THROW(fpSort.getFPSignificandSize());
-    Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-    ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException);
-  }
+  Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
+  ASSERT_NO_THROW(fpSort.getFPSignificandSize());
+  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+  ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getDatatypeParamSorts)
diff --git a/test/unit/theory/logic_info_white.cpp b/test/unit/theory/logic_info_white.cpp
index 7a6e34abb..e999297fd 100644
--- a/test/unit/theory/logic_info_white.cpp
+++ b/test/unit/theory/logic_info_white.cpp
@@ -616,28 +616,14 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic)
   info.arithOnlyLinear();
   info.disableIntegers();
   info.lock();
-  if (cvc5::Configuration::isBuiltWithSymFPU())
-  {
-    ASSERT_EQ(info.getLogicString(), "SEP_AUFBVFPDTLRA");
-  }
-  else
-  {
-    ASSERT_EQ(info.getLogicString(), "SEP_AUFBVDTLRA");
-  }
+  ASSERT_EQ(info.getLogicString(), "SEP_AUFBVFPDTLRA");
 
   info = info.getUnlockedCopy();
   ASSERT_FALSE(info.isLocked());
   info.disableQuantifiers();
   info.disableTheory(THEORY_BAGS);
   info.lock();
-  if (cvc5::Configuration::isBuiltWithSymFPU())
-  {
-    ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA");
-  }
-  else
-  {
-    ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVDTLRA");
-  }
+  ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA");
 
   info = info.getUnlockedCopy();
   ASSERT_FALSE(info.isLocked());
@@ -647,14 +633,7 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic)
   info.enableIntegers();
   info.disableReals();
   info.lock();
-  if (cvc5::Configuration::isBuiltWithSymFPU())
-  {
-    ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFFPLIA");
-  }
-  else
-  {
-    ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFLIA");
-  }
+  ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFFPLIA");
 
   info = info.getUnlockedCopy();
   ASSERT_FALSE(info.isLocked());
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index 26ab40614..c1630a203 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -24,9 +24,7 @@ cvc5_add_unit_test_white(check_white util)
 cvc5_add_unit_test_black(configuration_black util)
 cvc5_add_unit_test_black(datatype_black util)
 cvc5_add_unit_test_black(exception_black util)
-if(CVC5_USE_SYMFPU)
 cvc5_add_unit_test_black(floatingpoint_black util)
-endif()
 cvc5_add_unit_test_black(integer_black util)
 cvc5_add_unit_test_white(integer_white util)
 cvc5_add_unit_test_black(output_black util)
-- 
2.30.2