1 files changed, 1 insertions, 47 deletions
diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp
index 1fc893a30..dac0d5136 100644
--- a/src/theory/fp/fp_expand_defs.cpp
+++ b/src/theory/fp/fp_expand_defs.cpp
@@ -21,48 +21,6 @@ namespace cvc5 {
 namespace theory {
 namespace fp {
 
-namespace removeToFPGeneric {
-
-Node removeToFPGeneric(TNode node)
-{
-  Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC);
-
-  FloatingPointToFPGeneric info =
-      node.getOperator().getConst<FloatingPointToFPGeneric>();
-
-  size_t children = node.getNumChildren();
-
-  Node op;
-  NodeManager* nm = NodeManager::currentNM();
-
-  if (children == 1)
-  {
-    op = nm->mkConst(FloatingPointToFPIEEEBitVector(info));
-    return nm->mkNode(op, node[0]);
-  }
-  Assert(children == 2);
-  Assert(node[0].getType().isRoundingMode());
-
-  TypeNode t = node[1].getType();
-
-  if (t.isFloatingPoint())
-  {
-    op = nm->mkConst(FloatingPointToFPFloatingPoint(info));
-  }
-  else if (t.isReal())
-  {
-    op = nm->mkConst(FloatingPointToFPReal(info));
-  }
-  else
-  {
-    Assert(t.isBitVector());
-    op = nm->mkConst(FloatingPointToFPSignedBitVector(info));
-  }
-
-  return nm->mkNode(op, node[0], node[1]);
-}
-}  // namespace removeToFPGeneric
-
 FpExpandDefs::FpExpandDefs(context::UserContext* u)
     :
 
@@ -251,11 +209,7 @@ TrustNode FpExpandDefs::expandDefinition(Node node)
   Node res = node;
   Kind kind = node.getKind();
 
-  if (kind == kind::FLOATINGPOINT_TO_FP_GENERIC)
-  {
-    res = removeToFPGeneric::removeToFPGeneric(node);
-  }
-  else if (kind == kind::FLOATINGPOINT_MIN)
+  if (kind == kind::FLOATINGPOINT_MIN)
   {
     res = NodeManager::currentNM()->mkNode(
         kind::FLOATINGPOINT_MIN_TOTAL, node[0], node[1], minUF(node));