Removing structurally dead code. (#1540)

6 files changed, 1 insertions, 14 deletions

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 8001ca3df..9e61e713b 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -319,10 +319,8 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
   }
   case kind::SEXPR_TYPE:
     Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
-    return TypeNode();
   default:
     Unimplemented("don't have a commonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str());
-    return TypeNode();
   }
 }
 
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 3e767b6db..c67af2a5d 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -138,7 +138,6 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){
     break;
   }
   Unreachable();
-  return Node::null();
 }
 
 ArithIteUtils::ArithIteUtils(ContainsTermITEVisitor& contains,
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index b47cb1e60..b862e7604 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -592,7 +592,6 @@ RewriteResponse ArithRewriter::postRewrite(TNode t){
     return response;
   }else{
     Unreachable();
-    return RewriteResponse(REWRITE_DONE, Node::null());
   }
 }
 
@@ -603,7 +602,6 @@ RewriteResponse ArithRewriter::preRewrite(TNode t){
     return preRewriteAtom(t);
   }else{
     Unreachable();
-    return RewriteResponse(REWRITE_DONE, Node::null());
   }
 }
 
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");
   }
 
 
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index fe58f658d..d13003581 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -251,7 +251,6 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
   }
 
   Unreachable();
-  return Node::null();
 }/* Rewriter::rewriteTo() */
 
 void Rewriter::clearCaches() {