From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 28 Aug 2018 18:41:42 +0000 (-0700)
Subject: Remove dead code in fp_converter (#2388)
X-Git-Tag: cvc5-1.0.0~4707
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e496ca1fd9b400c4d50a34c22f2e9d630d17af3c;p=cvc5.git

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 afee609cf..b73108b1a 100644
--- 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