Remove dead code in fp_converter (#2388)

This should fix Coverity issues 1473025 and 1459599.

diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index afee609cf64b82e8c4f755a4d3ebfeeeff4cac04..b73108b1ac1df1fbc65d6701807e7be6b93a7a25 100644 (file)
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -1128,12 +1128,6 @@ Node FpConverter::convert(TNode node)
                   Unreachable(
                       "Floating-point subtraction should be removed by the "
                       "rewriter.");
-                  f.insert(current,
-                           symfpu::add<traits>(fpt(current.getType()),
-                                               (*mode).second,
-                                               (*arg1).second,
-                                               (*arg2).second,
-                                               prop(false)));
                   break;
 
                 case kind::FLOATINGPOINT_MULT:
@@ -1728,8 +1722,6 @@ Node FpConverter::getValue(Valuation &val, TNode var)
 #else
   Unimplemented("Conversion is dependent on SymFPU");
 #endif
-
-  return Node::null();
 }
 
 }  // namespace fp