From a5fd20bfe05e6d1a0a9dfc99bc8a668b613d9a19 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 23 Jun 2021 11:19:13 -0700
Subject: [PATCH] FP: Remove sections guarded with undefined macro
 SYMFPUPROPISBOOL. (#6786)

---
 src/theory/fp/fp_expand_defs.cpp |  8 --------
 src/theory/fp/theory_fp.cpp      | 31 ++++++++++++++-----------------
 2 files changed, 14 insertions(+), 25 deletions(-)

diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp
index 11bb05c70..a499b9666 100644
--- a/src/theory/fp/fp_expand_defs.cpp
+++ b/src/theory/fp/fp_expand_defs.cpp
@@ -51,11 +51,7 @@ Node FpExpandDefs::minUF(Node node)
     args[1] = t;
     fun = sm->mkDummySkolem("floatingpoint_min_zero_case",
                             nm->mkFunctionType(args,
-#ifdef SYMFPUPROPISBOOL
-                                               nm->booleanType()
-#else
                                                nm->mkBitVectorType(1U)
-#endif
                                                    ),
                             "floatingpoint_min_zero_case",
                             NodeManager::SKOLEM_EXACT_NAME);
@@ -89,11 +85,7 @@ Node FpExpandDefs::maxUF(Node node)
     args[1] = t;
     fun = sm->mkDummySkolem("floatingpoint_max_zero_case",
                             nm->mkFunctionType(args,
-#ifdef SYMFPUPROPISBOOL
-                                               nm->booleanType()
-#else
                                                nm->mkBitVectorType(1U)
-#endif
                                                    ),
                             "floatingpoint_max_zero_case",
                             NodeManager::SKOLEM_EXACT_NAME);
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 77dba0724..1c8f10f77 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -525,36 +525,32 @@ void TheoryFp::convertAndEquateTerm(TNode node) {
   size_t newAdditionalAssertions = d_conv->d_additionalAssertions.size();
   Assert(oldAdditionalAssertions <= newAdditionalAssertions);
 
-  while (oldAdditionalAssertions < newAdditionalAssertions) {
+  while (oldAdditionalAssertions < newAdditionalAssertions)
+  {
     Node addA = d_conv->d_additionalAssertions[oldAdditionalAssertions];
 
     Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion  "
                             << addA << std::endl;
 
-#ifdef SYMFPUPROPISBOOL
-    handleLemma(addA, false, true);
-#else
-    NodeManager *nm = NodeManager::currentNM();
+    NodeManager* nm = NodeManager::currentNM();
 
     handleLemma(
         nm->mkNode(kind::EQUAL, addA, nm->mkConst(::cvc5::BitVector(1U, 1U))),
         InferenceId::FP_EQUATE_TERM);
-#endif
 
     ++oldAdditionalAssertions;
   }
 
   // Equate the floating-point atom and the converted one.
   // Also adds the bit-vectors to the bit-vector solver.
-  if (node.getType().isBoolean()) {
-    if (converted != node) {
+  if (node.getType().isBoolean())
+  {
+    if (converted != node)
+    {
       Assert(converted.getType().isBitVector());
 
-      NodeManager *nm = NodeManager::currentNM();
+      NodeManager* nm = NodeManager::currentNM();
 
-#ifdef SYMFPUPROPISBOOL
-      handleLemma(nm->mkNode(kind::EQUAL, node, converted));
-#else
       handleLemma(
           nm->mkNode(kind::EQUAL,
                      node,
@@ -562,13 +558,14 @@ void TheoryFp::convertAndEquateTerm(TNode node) {
                                 converted,
                                 nm->mkConst(::cvc5::BitVector(1U, 1U)))),
           InferenceId::FP_EQUATE_TERM);
-#endif
-
-    } else {
+    }
+    else
+    {
       Assert((node.getKind() == kind::EQUAL));
     }
-
-  } else if (node.getType().isBitVector()) {
+  }
+  else if (node.getType().isBitVector())
+  {
     if (converted != node) {
       Assert(converted.getType().isBitVector());
 
-- 
2.30.2