diff options
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/fp_converter.cpp | 2 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 7 |
2 files changed, 1 insertions, 8 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 6ce2195cb..aba95d2ec 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -25,12 +25,10 @@ FpConverter::FpConverter(context::UserContext *user) Node FpConverter::convert(TNode node) { Unimplemented("Conversion not implemented."); - return node; } Node FpConverter::getValue(Valuation &val, TNode var) { Unimplemented("Conversion not implemented."); - return Node::null(); } } // namespace fp diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 98ac536ec..9fda5c2f6 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -63,7 +63,6 @@ namespace rewrite { RewriteResponse type (TNode node, bool) { Unreachable("sort kind (%d) found in expression?",node.getKind()); - return RewriteResponse(REWRITE_DONE, node); } RewriteResponse removeDoubleNegation (TNode node, bool) { @@ -143,7 +142,6 @@ namespace rewrite { RewriteResponse removed (TNode node, bool) { Unreachable("kind (%s) should have been removed?",kindToString(node.getKind()).c_str()); - return RewriteResponse(REWRITE_DONE, node); } RewriteResponse variable (TNode node, bool) { @@ -492,11 +490,8 @@ namespace constantFold { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 == arg2)); - } else { - Unreachable("Equality of unknown type"); } - - return RewriteResponse(REWRITE_DONE, node); + Unreachable("Equality of unknown type"); } |