From e496ca1fd9b400c4d50a34c22f2e9d630d17af3c Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 28 Aug 2018 11:41:42 -0700
Subject: Remove dead code in fp_converter (#2388)

This should fix Coverity issues 1473025 and 1459599.
---
 src/theory/fp/fp_converter.cpp | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'src')

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
-- 
cgit v1.2.3