From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 16 Jun 2021 21:04:09 +0000 (-0700)
Subject: Make symfpu a required dependency. (#6749)
X-Git-Tag: cvc5-1.0.0~1593
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b8d09076cfeb124bfaa6e1c3f0f37e3df1b1b516;p=cvc5.git

Make symfpu a required dependency. (#6749)
---

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 b/src/util/floatingpoint_literal_symfpu.h
new file mode 100644
index 000000000..5b2b0f7c8
--- /dev/null
+++ b/src/util/floatingpoint_literal_symfpu.h
@@ -0,0 +1,226 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * SymFPU glue code for floating-point values.
+ *
+ * !!! This header is not to be included in any other headers !!!
+ */
+#include "cvc5_public.h"
+
+#ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
+#define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
+
+#include "util/bitvector.h"
+#include "util/floatingpoint_literal_symfpu_traits.h"
+#include "util/floatingpoint_size.h"
+#include "util/roundingmode.h"
+
+/* -------------------------------------------------------------------------- */
+
+namespace cvc5 {
+
+using SymFPUUnpackedFloatLiteral =
+    ::symfpu::unpackedFloat<symfpuLiteral::traits>;
+
+class FloatingPointLiteral
+{
+  friend class FloatingPoint;
+
+ public:
+  /**
+   * The kind of floating-point special constants that can be created via the
+   * corresponding constructor.
+   * These are prefixed with FP because of name clashes with NAN.
+   */
+  enum SpecialConstKind
+  {
+    FPINF,   // +-oo
+    FPNAN,   // NaN
+    FPZERO,  // +-zero
+  };
+
+  /**
+   * Get the number of exponent bits in the unpacked format corresponding to a
+   * given packed format.  This is the unpacked counter-part of
+   * FloatingPointSize::exponentWidth().
+   */
+  static uint32_t getUnpackedExponentWidth(FloatingPointSize& size);
+  /**
+   * Get the number of exponent bits in the unpacked format corresponding to a
+   * given packed format.  This is the unpacked counter-part of
+   * FloatingPointSize::significandWidth().
+   */
+  static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size);
+
+  /** Constructors. */
+
+  /** Create a FP literal from its IEEE bit-vector representation. */
+  FloatingPointLiteral(uint32_t exp_size,
+                       uint32_t sig_size,
+                       const BitVector& bv);
+  FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv);
+
+  /** Create a FP literal that represents a special constants. */
+  FloatingPointLiteral(const FloatingPointSize& size, SpecialConstKind kind);
+  FloatingPointLiteral(const FloatingPointSize& size,
+                       SpecialConstKind kind,
+                       bool sign);
+
+  /**
+   * Create a FP literal from a signed or unsigned bit-vector value with
+   * respect to given rounding mode.
+   */
+  FloatingPointLiteral(const FloatingPointSize& size,
+                       const RoundingMode& rm,
+                       const BitVector& bv,
+                       bool signedBV);
+
+  ~FloatingPointLiteral() {}
+
+  /** Return the size of this FP literal. */
+  const FloatingPointSize& getSize() const { return d_fp_size; };
+
+  /** Return the packed (IEEE-754) representation of this literal. */
+  BitVector pack(void) const;
+
+  /** Floating-point absolute value literal. */
+  FloatingPointLiteral absolute(void) const;
+  /** Floating-point negation literal. */
+  FloatingPointLiteral negate(void) const;
+  /** Floating-point addition literal. */
+  FloatingPointLiteral add(const RoundingMode& rm,
+                           const FloatingPointLiteral& arg) const;
+  /** Floating-point subtraction literal. */
+  FloatingPointLiteral sub(const RoundingMode& rm,
+                           const FloatingPointLiteral& arg) const;
+  /** Floating-point multiplication literal. */
+  FloatingPointLiteral mult(const RoundingMode& rm,
+                            const FloatingPointLiteral& arg) const;
+  /** Floating-point division literal. */
+  FloatingPointLiteral div(const RoundingMode& rm,
+                           const FloatingPointLiteral& arg) const;
+  /** Floating-point fused multiplication and addition literal. */
+  FloatingPointLiteral fma(const RoundingMode& rm,
+                           const FloatingPointLiteral& arg1,
+                           const FloatingPointLiteral& arg2) const;
+  /** Floating-point square root literal. */
+  FloatingPointLiteral sqrt(const RoundingMode& rm) const;
+  /** Floating-point round to integral literal. */
+  FloatingPointLiteral rti(const RoundingMode& rm) const;
+  /** Floating-point remainder literal. */
+  FloatingPointLiteral rem(const FloatingPointLiteral& arg) const;
+
+  /**
+   * Floating-point max literal (total version).
+   * zeroCase: true to return the left (rather than the right operand) in case
+   *           of max(-0,+0) or max(+0,-0).
+   */
+  FloatingPointLiteral maxTotal(const FloatingPointLiteral& arg,
+                                bool zeroCaseLeft) const;
+  /**
+   * Floating-point min literal (total version).
+   * zeroCase: true to return the left (rather than the right operand) in case
+   *           of min(-0,+0) or min(+0,-0).
+   */
+  FloatingPointLiteral minTotal(const FloatingPointLiteral& arg,
+                                bool zeroCaseLeft) const;
+
+  /** Equality literal (NOT: fp.eq but =) over floating-point values. */
+  bool operator==(const FloatingPointLiteral& fp) const;
+  /** Floating-point less or equal than literal. */
+  bool operator<=(const FloatingPointLiteral& arg) const;
+  /** Floating-point less than literal. */
+  bool operator<(const FloatingPointLiteral& arg) const;
+
+  /** Get the exponent of this floating-point value. */
+  BitVector getExponent() const;
+  /** Get the significand of this floating-point value. */
+  BitVector getSignificand() const;
+  /** True if this value is a negative value. */
+  bool getSign() const;
+
+  /** Return true if this literal represents a normal value. */
+  bool isNormal(void) const;
+  /** Return true if this  literal represents a subnormal value. */
+  bool isSubnormal(void) const;
+  /** Return true if this literal represents a zero value. */
+  bool isZero(void) const;
+  /** Return true if this literal represents an infinite value. */
+  bool isInfinite(void) const;
+  /** Return true if this literal represents a NaN value. */
+  bool isNaN(void) const;
+  /** Return true if this literal represents a negative value. */
+  bool isNegative(void) const;
+  /** Return true if this literal represents a positive value. */
+  bool isPositive(void) const;
+
+  /**
+   * Convert this floating-point literal to a literal of given size, with
+   * respect to given rounding mode.
+   */
+  FloatingPointLiteral convert(const FloatingPointSize& target,
+                               const RoundingMode& rm) const;
+
+  /**
+   * Convert this floating-point literal to a signed bit-vector of given size,
+   * with respect to given rounding mode (total version).
+   * Returns given bit-vector 'undefinedCase' in the undefined case.
+   */
+  BitVector convertToSBVTotal(BitVectorSize width,
+                              const RoundingMode& rm,
+                              BitVector undefinedCase) const;
+  /**
+   * Convert this floating-point literal to an unsigned bit-vector of given
+   * size, with respect to given rounding mode (total version).
+   * Returns given bit-vector 'undefinedCase' in the undefined case.
+   */
+  BitVector convertToUBVTotal(BitVectorSize width,
+                              const RoundingMode& rm,
+                              BitVector undefinedCase) const;
+  /** Return wrapped floating-point literal. */
+  const SymFPUUnpackedFloatLiteral& getSymUF() const { return d_symuf; }
+
+ private:
+  /**
+   * Create a FP literal from unpacked representation.
+   *
+   * This unpacked representation accounts for additional bits required for the
+   * exponent to allow subnormals to be normalized.
+   *
+   * This should NOT be used to create a literal from its IEEE bit-vector
+   * representation -- for this, the above constructor is to be used while
+   * creating a SymFPUUnpackedFloatLiteral via symfpu::unpack.
+   */
+  FloatingPointLiteral(const FloatingPointSize& size,
+                       const bool sign,
+                       const BitVector& exp,
+                       const BitVector& sig)
+      : d_fp_size(size), d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig))
+  {
+  }
+
+  /** Create a FP literal from a symFPU unpacked float. */
+  FloatingPointLiteral(const FloatingPointSize& size,
+                       SymFPUUnpackedFloatLiteral symuf)
+      : d_fp_size(size), d_symuf(symuf){};
+
+  /** The floating-point size of this floating-point literal. */
+  FloatingPointSize d_fp_size;
+  /** The actual floating-point value, a SymFPU unpackedFloat. */
+  SymFPUUnpackedFloatLiteral d_symuf;
+};
+
+/* -------------------------------------------------------------------------- */
+
+}  // namespace cvc5
+
+#endif
diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h.in
deleted file mode 100644
index 54827a308..000000000
--- a/src/util/floatingpoint_literal_symfpu.h.in
+++ /dev/null
@@ -1,260 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Aina Niemetz, Andres Noetzli
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * SymFPU glue code for floating-point values.
- *
- * !!! This header is not to be included in any other headers !!!
- */
-#include "cvc5_public.h"
-
-#ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
-#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/roundingmode.h"
-
-/* -------------------------------------------------------------------------- */
-
-namespace cvc5 {
-
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-// clang-format on
-using SymFPUUnpackedFloatLiteral =
-    ::symfpu::unpackedFloat<symfpuLiteral::traits>;
-#endif
-
-class FloatingPointLiteral
-{
-  friend class FloatingPoint;
-
- public:
-  /**
-   * The kind of floating-point special constants that can be created via the
-   * corresponding constructor.
-   * These are prefixed with FP because of name clashes with NAN.
-   */
-  enum SpecialConstKind
-  {
-    FPINF,   // +-oo
-    FPNAN,   // NaN
-    FPZERO,  // +-zero
-  };
-
-  /**
-   * Get the number of exponent bits in the unpacked format corresponding to a
-   * given packed format.  This is the unpacked counter-part of
-   * FloatingPointSize::exponentWidth().
-   */
-  static uint32_t getUnpackedExponentWidth(FloatingPointSize& size);
-  /**
-   * Get the number of exponent bits in the unpacked format corresponding to a
-   * given packed format.  This is the unpacked counter-part of
-   * FloatingPointSize::significandWidth().
-   */
-  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. */
-  FloatingPointLiteral(uint32_t exp_size,
-                       uint32_t sig_size,
-                       const BitVector& bv);
-  FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv);
-
-  /** Create a FP literal that represents a special constants. */
-  FloatingPointLiteral(const FloatingPointSize& size, SpecialConstKind kind);
-  FloatingPointLiteral(const FloatingPointSize& size,
-                       SpecialConstKind kind,
-                       bool sign);
-
-  /**
-   * Create a FP literal from a signed or unsigned bit-vector value with
-   * respect to given rounding mode.
-   */
-  FloatingPointLiteral(const FloatingPointSize& size,
-                       const RoundingMode& rm,
-                       const BitVector& bv,
-                       bool signedBV);
-
-  ~FloatingPointLiteral() {}
-
-  /** Return the size of this FP literal. */
-  const FloatingPointSize& getSize() const { return d_fp_size; };
-
-  /** Return the packed (IEEE-754) representation of this literal. */
-  BitVector pack(void) const;
-
-  /** Floating-point absolute value literal. */
-  FloatingPointLiteral absolute(void) const;
-  /** Floating-point negation literal. */
-  FloatingPointLiteral negate(void) const;
-  /** Floating-point addition literal. */
-  FloatingPointLiteral add(const RoundingMode& rm,
-                           const FloatingPointLiteral& arg) const;
-  /** Floating-point subtraction literal. */
-  FloatingPointLiteral sub(const RoundingMode& rm,
-                           const FloatingPointLiteral& arg) const;
-  /** Floating-point multiplication literal. */
-  FloatingPointLiteral mult(const RoundingMode& rm,
-                            const FloatingPointLiteral& arg) const;
-  /** Floating-point division literal. */
-  FloatingPointLiteral div(const RoundingMode& rm,
-                           const FloatingPointLiteral& arg) const;
-  /** Floating-point fused multiplication and addition literal. */
-  FloatingPointLiteral fma(const RoundingMode& rm,
-                           const FloatingPointLiteral& arg1,
-                           const FloatingPointLiteral& arg2) const;
-  /** Floating-point square root literal. */
-  FloatingPointLiteral sqrt(const RoundingMode& rm) const;
-  /** Floating-point round to integral literal. */
-  FloatingPointLiteral rti(const RoundingMode& rm) const;
-  /** Floating-point remainder literal. */
-  FloatingPointLiteral rem(const FloatingPointLiteral& arg) const;
-
-  /**
-   * Floating-point max literal (total version).
-   * zeroCase: true to return the left (rather than the right operand) in case
-   *           of max(-0,+0) or max(+0,-0).
-   */
-  FloatingPointLiteral maxTotal(const FloatingPointLiteral& arg,
-                                bool zeroCaseLeft) const;
-  /**
-   * Floating-point min literal (total version).
-   * zeroCase: true to return the left (rather than the right operand) in case
-   *           of min(-0,+0) or min(+0,-0).
-   */
-  FloatingPointLiteral minTotal(const FloatingPointLiteral& arg,
-                                bool zeroCaseLeft) const;
-
-  /** Equality literal (NOT: fp.eq but =) over floating-point values. */
-  bool operator==(const FloatingPointLiteral& fp) const;
-  /** Floating-point less or equal than literal. */
-  bool operator<=(const FloatingPointLiteral& arg) const;
-  /** Floating-point less than literal. */
-  bool operator<(const FloatingPointLiteral& arg) const;
-
-  /** Get the exponent of this floating-point value. */
-  BitVector getExponent() const;
-  /** Get the significand of this floating-point value. */
-  BitVector getSignificand() const;
-  /** True if this value is a negative value. */
-  bool getSign() const;
-
-  /** Return true if this literal represents a normal value. */
-  bool isNormal(void) const;
-  /** Return true if this  literal represents a subnormal value. */
-  bool isSubnormal(void) const;
-  /** Return true if this literal represents a zero value. */
-  bool isZero(void) const;
-  /** Return true if this literal represents an infinite value. */
-  bool isInfinite(void) const;
-  /** Return true if this literal represents a NaN value. */
-  bool isNaN(void) const;
-  /** Return true if this literal represents a negative value. */
-  bool isNegative(void) const;
-  /** Return true if this literal represents a positive value. */
-  bool isPositive(void) const;
-
-  /**
-   * Convert this floating-point literal to a literal of given size, with
-   * respect to given rounding mode.
-   */
-  FloatingPointLiteral convert(const FloatingPointSize& target,
-                               const RoundingMode& rm) const;
-
-  /**
-   * Convert this floating-point literal to a signed bit-vector of given size,
-   * with respect to given rounding mode (total version).
-   * Returns given bit-vector 'undefinedCase' in the undefined case.
-   */
-  BitVector convertToSBVTotal(BitVectorSize width,
-                              const RoundingMode& rm,
-                              BitVector undefinedCase) const;
-  /**
-   * Convert this floating-point literal to an unsigned bit-vector of given
-   * size, with respect to given rounding mode (total version).
-   * Returns given bit-vector 'undefinedCase' in the undefined case.
-   */
-  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.
-   *
-   * This unpacked representation accounts for additional bits required for the
-   * exponent to allow subnormals to be normalized.
-   *
-   * This should NOT be used to create a literal from its IEEE bit-vector
-   * representation -- for this, the above constructor is to be used while
-   * creating a SymFPUUnpackedFloatLiteral via symfpu::unpack.
-   */
-  FloatingPointLiteral(const FloatingPointSize& size,
-                       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
-  {
-  }
-
-// 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
-};
-
-/* -------------------------------------------------------------------------- */
-
-}  // namespace cvc5
-
-#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 b/src/util/floatingpoint_literal_symfpu_traits.h
new file mode 100644
index 000000000..bc5caaf88
--- /dev/null
+++ b/src/util/floatingpoint_literal_symfpu_traits.h
@@ -0,0 +1,259 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Martin Brain, Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * SymFPU glue code for floating-point values.
+ *
+ * !!! This header is only to be included in floating-point literal headers !!!
+ *
+ * This is a symfpu literal "back-end".  It allows the library to be used as
+ * an arbitrary precision floating-point implementation.  This is effectively
+ * the glue between symfpu's notion of "signed bit-vector" and cvc5's
+ * BitVector.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
+#define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
+
+#include <symfpu/core/unpackedFloat.h>
+
+#include "util/bitvector.h"
+#include "util/floatingpoint_size.h"
+#include "util/roundingmode.h"
+
+/* -------------------------------------------------------------------------- */
+
+namespace cvc5 {
+namespace symfpuLiteral {
+
+/**
+ * Forward declaration of wrapper so that traits can be defined early and so
+ * used in the implementation of wrappedBitVector.
+ */
+template <bool T>
+class wrappedBitVector;
+
+using Cvc5BitWidth = uint32_t;
+using Cvc5Prop = bool;
+using Cvc5RM = ::cvc5::RoundingMode;
+using Cvc5FPSize = ::cvc5::FloatingPointSize;
+using Cvc5UnsignedBitVector = wrappedBitVector<false>;
+using Cvc5SignedBitVector = wrappedBitVector<true>;
+
+/**
+ * This is the template parameter for symfpu's templates.
+ */
+class traits
+{
+ public:
+  /** The six key types that symfpu uses. */
+  using bwt = Cvc5BitWidth;           // bit-width type
+  using prop = Cvc5Prop;              // boolean type
+  using rm = Cvc5RM;                  // rounding-mode type
+  using fpt = Cvc5FPSize;             // floating-point format type
+  using ubv = Cvc5UnsignedBitVector;  // unsigned bit-vector type
+  using sbv = Cvc5SignedBitVector;    // signed bit-vector type
+
+  /** Give concrete instances of each rounding mode, mainly for comparisons. */
+  static rm RNE(void);
+  static rm RNA(void);
+  static rm RTP(void);
+  static rm RTN(void);
+  static rm RTZ(void);
+
+  /** The sympfu properties. */
+  static void precondition(const prop& p);
+  static void postcondition(const prop& p);
+  static void invariant(const prop& p);
+};
+
+/**
+ * Type function for mapping between types.
+ */
+template <bool T>
+struct signedToLiteralType;
+
+template <>
+struct signedToLiteralType<true>
+{
+  using literalType = int32_t;
+};
+template <>
+struct signedToLiteralType<false>
+{
+  using literalType = uint32_t;
+};
+
+/**
+ * This extends the interface for cvc5::BitVector for compatibility with symFPU.
+ * The template parameter distinguishes signed and unsigned bit-vectors, a
+ * distinction symfpu uses.
+ */
+template <bool isSigned>
+class wrappedBitVector : public BitVector
+{
+ protected:
+  using literalType = typename signedToLiteralType<isSigned>::literalType;
+  friend wrappedBitVector<!isSigned>;  // To allow conversion between types
+
+  friend ::symfpu::ite<Cvc5Prop, wrappedBitVector<isSigned> >;  // For ITE
+
+ public:
+  /** Constructors. */
+  wrappedBitVector(const Cvc5BitWidth w, const uint32_t v) : BitVector(w, v) {}
+  wrappedBitVector(const Cvc5Prop& p) : BitVector(1, p ? 1U : 0U) {}
+  wrappedBitVector(const wrappedBitVector<isSigned>& old) : BitVector(old) {}
+  wrappedBitVector(const BitVector& old) : BitVector(old) {}
+
+  /** Get the bit-width of this wrapped bit-vector. */
+  Cvc5BitWidth getWidth(void) const { return getSize(); }
+
+  /** Create a zero value of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> one(const Cvc5BitWidth& w);
+  /** Create a one value of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> zero(const Cvc5BitWidth& w);
+  /** Create a ones value (all bits 1) of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> allOnes(const Cvc5BitWidth& w);
+  /** Create a maximum signed/unsigned value of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> maxValue(const Cvc5BitWidth& w);
+  /** Create a minimum signed/unsigned value of given bit-width 'w'. */
+  static wrappedBitVector<isSigned> minValue(const Cvc5BitWidth& w);
+
+  /** Return true if this a bit-vector representing a ones value. */
+  Cvc5Prop isAllOnes() const;
+  /** Return true if this a bit-vector representing a zero value. */
+  Cvc5Prop isAllZeros() const;
+
+  /** Left shift. */
+  wrappedBitVector<isSigned> operator<<(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Logical (unsigned) and arithmetic (signed) right shift. */
+  wrappedBitVector<isSigned> operator>>(
+      const wrappedBitVector<isSigned>& op) const;
+
+  /**
+   * Inherited but ...
+   * *sigh* if we use the inherited version then it will return a
+   * cvc5::BitVector which can be converted back to a
+   * wrappedBitVector<isSigned> but isn't done automatically when working
+   * out types for templates instantiation.  ITE is a particular
+   * problem as expressions and constants no longer derive the
+   * same type.  There aren't any good solutions in C++, we could
+   * use CRTP but Liana wouldn't appreciate that, so the following
+   * pointless wrapping functions are needed.
+   */
+
+  /** Bit-wise or. */
+  wrappedBitVector<isSigned> operator|(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-wise and. */
+  wrappedBitVector<isSigned> operator&(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector addition. */
+  wrappedBitVector<isSigned> operator+(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector subtraction. */
+  wrappedBitVector<isSigned> operator-(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector multiplication. */
+  wrappedBitVector<isSigned> operator*(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector signed/unsigned division. */
+  wrappedBitVector<isSigned> operator/(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector signed/unsigned remainder. */
+  wrappedBitVector<isSigned> operator%(
+      const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector negation. */
+  wrappedBitVector<isSigned> operator-(void) const;
+  /** Bit-wise not. */
+  wrappedBitVector<isSigned> operator~(void) const;
+
+  /** Bit-vector increment. */
+  wrappedBitVector<isSigned> increment() const;
+  /** Bit-vector decrement. */
+  wrappedBitVector<isSigned> decrement() const;
+  /**
+   * Bit-vector logical/arithmetic right shift where 'op' extended to the
+   * bit-width of this wrapped bit-vector.
+   */
+  wrappedBitVector<isSigned> signExtendRightShift(
+      const wrappedBitVector<isSigned>& op) const;
+
+  /**
+   * Modular operations.
+   * Note: No overflow checking so these are the same as other operations.
+   */
+  wrappedBitVector<isSigned> modularLeftShift(
+      const wrappedBitVector<isSigned>& op) const;
+  wrappedBitVector<isSigned> modularRightShift(
+      const wrappedBitVector<isSigned>& op) const;
+  wrappedBitVector<isSigned> modularIncrement() const;
+  wrappedBitVector<isSigned> modularDecrement() const;
+  wrappedBitVector<isSigned> modularAdd(
+      const wrappedBitVector<isSigned>& op) const;
+  wrappedBitVector<isSigned> modularNegate() const;
+
+  /** Bit-vector equality. */
+  Cvc5Prop operator==(const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector signed/unsigned less or equal than. */
+  Cvc5Prop operator<=(const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector sign/unsigned greater or equal than. */
+  Cvc5Prop operator>=(const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector signed/unsigned less than. */
+  Cvc5Prop operator<(const wrappedBitVector<isSigned>& op) const;
+  /** Bit-vector sign/unsigned greater or equal than. */
+  Cvc5Prop operator>(const wrappedBitVector<isSigned>& op) const;
+
+  /** Convert this bit-vector to a signed bit-vector. */
+  wrappedBitVector<true> toSigned(void) const;
+  /** Convert this bit-vector to an unsigned bit-vector. */
+  wrappedBitVector<false> toUnsigned(void) const;
+
+  /** Bit-vector signed/unsigned (zero) extension. */
+  wrappedBitVector<isSigned> extend(Cvc5BitWidth extension) const;
+
+  /**
+   * Create a "contracted" bit-vector by cutting off the 'reduction' number of
+   * most significant bits, i.e., by extracting the (bit-width - reduction)
+   * least significant bits.
+   */
+  wrappedBitVector<isSigned> contract(Cvc5BitWidth reduction) const;
+
+  /**
+   * Create a "resized" bit-vector of given size bei either extending (if new
+   * size is larger) or contracting (if it is smaller) this wrapped bit-vector.
+   */
+  wrappedBitVector<isSigned> resize(Cvc5BitWidth newSize) const;
+
+  /**
+   * Create an extension of this bit-vector that matches the bit-width of the
+   * given bit-vector.
+   *
+   * Note: The size of the given bit-vector may not be larger than the size of
+   *       this bit-vector.
+   */
+  wrappedBitVector<isSigned> matchWidth(
+      const wrappedBitVector<isSigned>& op) const;
+
+  /** Bit-vector concatenation. */
+  wrappedBitVector<isSigned> append(const wrappedBitVector<isSigned>& op) const;
+
+  /** Inclusive of end points, thus if the same, extracts just one bit. */
+  wrappedBitVector<isSigned> extract(Cvc5BitWidth upper,
+                                     Cvc5BitWidth lower) const;
+};
+}  // namespace symfpuLiteral
+}  // namespace cvc5
+
+#endif
diff --git a/src/util/floatingpoint_literal_symfpu_traits.h.in b/src/util/floatingpoint_literal_symfpu_traits.h.in
deleted file mode 100644
index 76d2f47e2..000000000
--- a/src/util/floatingpoint_literal_symfpu_traits.h.in
+++ /dev/null
@@ -1,264 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Aina Niemetz, Martin Brain, Andres Noetzli
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * SymFPU glue code for floating-point values.
- *
- * !!! This header is only to be included in floating-point literal headers !!!
- *
- * This is a symfpu literal "back-end".  It allows the library to be used as
- * an arbitrary precision floating-point implementation.  This is effectively
- * the glue between symfpu's notion of "signed bit-vector" and cvc5's
- * BitVector.
- */
-
-#include "cvc5_private.h"
-
-#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 "util/bitvector.h"
-#include "util/floatingpoint_size.h"
-#include "util/roundingmode.h"
-
-#include <symfpu/core/unpackedFloat.h>
-
-/* -------------------------------------------------------------------------- */
-
-namespace cvc5 {
-namespace symfpuLiteral {
-
-/**
- * Forward declaration of wrapper so that traits can be defined early and so
- * used in the implementation of wrappedBitVector.
- */
-template <bool T>
-class wrappedBitVector;
-
-using Cvc5BitWidth = uint32_t;
-using Cvc5Prop = bool;
-using Cvc5RM = ::cvc5::RoundingMode;
-using Cvc5FPSize = ::cvc5::FloatingPointSize;
-using Cvc5UnsignedBitVector = wrappedBitVector<false>;
-using Cvc5SignedBitVector = wrappedBitVector<true>;
-
-/**
- * This is the template parameter for symfpu's templates.
- */
-class traits
-{
- public:
-  /** The six key types that symfpu uses. */
-  using bwt = Cvc5BitWidth;           // bit-width type
-  using prop = Cvc5Prop;              // boolean type
-  using rm = Cvc5RM;                  // rounding-mode type
-  using fpt = Cvc5FPSize;             // floating-point format type
-  using ubv = Cvc5UnsignedBitVector;  // unsigned bit-vector type
-  using sbv = Cvc5SignedBitVector;    // signed bit-vector type
-
-  /** Give concrete instances of each rounding mode, mainly for comparisons. */
-  static rm RNE(void);
-  static rm RNA(void);
-  static rm RTP(void);
-  static rm RTN(void);
-  static rm RTZ(void);
-
-  /** The sympfu properties. */
-  static void precondition(const prop& p);
-  static void postcondition(const prop& p);
-  static void invariant(const prop& p);
-};
-
-/**
- * Type function for mapping between types.
- */
-template <bool T>
-struct signedToLiteralType;
-
-template <>
-struct signedToLiteralType<true>
-{
-  using literalType = int32_t;
-};
-template <>
-struct signedToLiteralType<false>
-{
-  using literalType = uint32_t;
-};
-
-/**
- * This extends the interface for cvc5::BitVector for compatibility with symFPU.
- * The template parameter distinguishes signed and unsigned bit-vectors, a
- * distinction symfpu uses.
- */
-template <bool isSigned>
-class wrappedBitVector : public BitVector
-{
- protected:
-  using literalType = typename signedToLiteralType<isSigned>::literalType;
-  friend wrappedBitVector<!isSigned>;  // To allow conversion between types
-
-  friend ::symfpu::ite<Cvc5Prop, wrappedBitVector<isSigned> >;  // For ITE
-
- public:
-  /** Constructors. */
-  wrappedBitVector(const Cvc5BitWidth w, const uint32_t v) : BitVector(w, v) {}
-  wrappedBitVector(const Cvc5Prop& p) : BitVector(1, p ? 1U : 0U) {}
-  wrappedBitVector(const wrappedBitVector<isSigned>& old) : BitVector(old) {}
-  wrappedBitVector(const BitVector& old) : BitVector(old) {}
-
-  /** Get the bit-width of this wrapped bit-vector. */
-  Cvc5BitWidth getWidth(void) const { return getSize(); }
-
-  /** Create a zero value of given bit-width 'w'. */
-  static wrappedBitVector<isSigned> one(const Cvc5BitWidth& w);
-  /** Create a one value of given bit-width 'w'. */
-  static wrappedBitVector<isSigned> zero(const Cvc5BitWidth& w);
-  /** Create a ones value (all bits 1) of given bit-width 'w'. */
-  static wrappedBitVector<isSigned> allOnes(const Cvc5BitWidth& w);
-  /** Create a maximum signed/unsigned value of given bit-width 'w'. */
-  static wrappedBitVector<isSigned> maxValue(const Cvc5BitWidth& w);
-  /** Create a minimum signed/unsigned value of given bit-width 'w'. */
-  static wrappedBitVector<isSigned> minValue(const Cvc5BitWidth& w);
-
-  /** Return true if this a bit-vector representing a ones value. */
-  Cvc5Prop isAllOnes() const;
-  /** Return true if this a bit-vector representing a zero value. */
-  Cvc5Prop isAllZeros() const;
-
-  /** Left shift. */
-  wrappedBitVector<isSigned> operator<<(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Logical (unsigned) and arithmetic (signed) right shift. */
-  wrappedBitVector<isSigned> operator>>(
-      const wrappedBitVector<isSigned>& op) const;
-
-  /**
-   * Inherited but ...
-   * *sigh* if we use the inherited version then it will return a
-   * cvc5::BitVector which can be converted back to a
-   * wrappedBitVector<isSigned> but isn't done automatically when working
-   * out types for templates instantiation.  ITE is a particular
-   * problem as expressions and constants no longer derive the
-   * same type.  There aren't any good solutions in C++, we could
-   * use CRTP but Liana wouldn't appreciate that, so the following
-   * pointless wrapping functions are needed.
-   */
-
-  /** Bit-wise or. */
-  wrappedBitVector<isSigned> operator|(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-wise and. */
-  wrappedBitVector<isSigned> operator&(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector addition. */
-  wrappedBitVector<isSigned> operator+(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector subtraction. */
-  wrappedBitVector<isSigned> operator-(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector multiplication. */
-  wrappedBitVector<isSigned> operator*(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector signed/unsigned division. */
-  wrappedBitVector<isSigned> operator/(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector signed/unsigned remainder. */
-  wrappedBitVector<isSigned> operator%(
-      const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector negation. */
-  wrappedBitVector<isSigned> operator-(void) const;
-  /** Bit-wise not. */
-  wrappedBitVector<isSigned> operator~(void) const;
-
-  /** Bit-vector increment. */
-  wrappedBitVector<isSigned> increment() const;
-  /** Bit-vector decrement. */
-  wrappedBitVector<isSigned> decrement() const;
-  /**
-   * Bit-vector logical/arithmetic right shift where 'op' extended to the
-   * bit-width of this wrapped bit-vector.
-   */
-  wrappedBitVector<isSigned> signExtendRightShift(
-      const wrappedBitVector<isSigned>& op) const;
-
-  /**
-   * Modular operations.
-   * Note: No overflow checking so these are the same as other operations.
-   */
-  wrappedBitVector<isSigned> modularLeftShift(
-      const wrappedBitVector<isSigned>& op) const;
-  wrappedBitVector<isSigned> modularRightShift(
-      const wrappedBitVector<isSigned>& op) const;
-  wrappedBitVector<isSigned> modularIncrement() const;
-  wrappedBitVector<isSigned> modularDecrement() const;
-  wrappedBitVector<isSigned> modularAdd(
-      const wrappedBitVector<isSigned>& op) const;
-  wrappedBitVector<isSigned> modularNegate() const;
-
-  /** Bit-vector equality. */
-  Cvc5Prop operator==(const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector signed/unsigned less or equal than. */
-  Cvc5Prop operator<=(const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector sign/unsigned greater or equal than. */
-  Cvc5Prop operator>=(const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector signed/unsigned less than. */
-  Cvc5Prop operator<(const wrappedBitVector<isSigned>& op) const;
-  /** Bit-vector sign/unsigned greater or equal than. */
-  Cvc5Prop operator>(const wrappedBitVector<isSigned>& op) const;
-
-  /** Convert this bit-vector to a signed bit-vector. */
-  wrappedBitVector<true> toSigned(void) const;
-  /** Convert this bit-vector to an unsigned bit-vector. */
-  wrappedBitVector<false> toUnsigned(void) const;
-
-  /** Bit-vector signed/unsigned (zero) extension. */
-  wrappedBitVector<isSigned> extend(Cvc5BitWidth extension) const;
-
-  /**
-   * Create a "contracted" bit-vector by cutting off the 'reduction' number of
-   * most significant bits, i.e., by extracting the (bit-width - reduction)
-   * least significant bits.
-   */
-  wrappedBitVector<isSigned> contract(Cvc5BitWidth reduction) const;
-
-  /**
-   * Create a "resized" bit-vector of given size bei either extending (if new
-   * size is larger) or contracting (if it is smaller) this wrapped bit-vector.
-   */
-  wrappedBitVector<isSigned> resize(Cvc5BitWidth newSize) const;
-
-  /**
-   * Create an extension of this bit-vector that matches the bit-width of the
-   * given bit-vector.
-   *
-   * Note: The size of the given bit-vector may not be larger than the size of
-   *       this bit-vector.
-   */
-  wrappedBitVector<isSigned> matchWidth(
-      const wrappedBitVector<isSigned>& op) const;
-
-  /** Bit-vector concatenation. */
-  wrappedBitVector<isSigned> append(const wrappedBitVector<isSigned>& op) const;
-
-  /** Inclusive of end points, thus if the same, extracts just one bit. */
-  wrappedBitVector<isSigned> extract(Cvc5BitWidth upper,
-                                     Cvc5BitWidth lower) const;
-};
-}  // namespace symfpuLiteral
-}
-
-#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)