diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-28 11:41:42 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-28 11:41:42 -0700 |
| commit | e496ca1fd9b400c4d50a34c22f2e9d630d17af3c (patch) | |
| tree | 78d0d63b10b19c0cc409ba7c29d93239a51c9cd2 /src | |
| parent | 421a093844d9249f2735ff4b0b44f6d2b086d81d (diff) | |
Remove dead code in fp_converter (#2388)
This should fix Coverity issues 1473025 and 1459599.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/fp/fp_converter.cpp | 8 |
1 files changed, 0 insertions, 8 deletions
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 |