Removing structurally dead code. (#1540)

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 8001ca3df5475d0f5f49fbcea3d95dd34dd6c12c..9e61e713b7db5479bfbe92e6c0c3e50b539e86cf 100644 (file)
--- 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 3e767b6db1e7751795a6d613eb63f0434c3fe252..c67af2a5d670796a538a555e1e93d1944ce66ae4 100644 (file)
--- 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 b47cb1e608e266cb141b95367320e2f42feea9a1..b862e7604fb51aa437277d087d4988b5bd9112e6 100644 (file)
--- 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 6ce2195cbd61e21a0ac20bdff95808824386d74b..aba95d2ec796b27c7aa2a41395198f876e233fc6 100644 (file)
--- 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 98ac536ec71e6b5e3a79cf492f5da27bfe089c95..9fda5c2f68a56a1455460fd7df5647c9f964bd88 100644 (file)
--- 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 fe58f658df748edfa7d35db67d339132f04864ff..d1300358157d9a3cdb669101614fffefc5396557 100644 (file)
--- 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() {