4 files changed, 11 insertions, 18 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.h b/src/theory/fp/theory_fp.h
index 614cbff46..ca80546b8 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -38,21 +38,21 @@ class TheoryFp : public Theory {
   TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out,
            Valuation valuation, const LogicInfo& logicInfo);
 
-  Node expandDefinition(LogicRequest& lr, Node node);
+  Node expandDefinition(LogicRequest& lr, Node node) override;
 
-  void preRegisterTerm(TNode node);
-  void addSharedTerm(TNode node);
+  void preRegisterTerm(TNode node) override;
+  void addSharedTerm(TNode node) override;
 
-  void check(Effort);
+  void check(Effort) override;
 
-  Node getModelValue(TNode var);
+  Node getModelValue(TNode var) override;
   bool collectModelInfo(TheoryModel* m) override;
 
-  std::string identify() const { return "THEORY_FP"; }
+  std::string identify() const override { return "THEORY_FP"; }
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
-  Node explain(TNode n);
+  Node explain(TNode n) override;
 
  protected:
   /** Equality engine */
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/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h
index 0ae6462bc..4b243c224 100644
--- a/src/theory/fp/type_enumerator.h
+++ b/src/theory/fp/type_enumerator.h
@@ -48,7 +48,7 @@ class FloatingPointEnumerator
     return NodeManager::currentNM()->mkConst(createFP());
   }
 
-  FloatingPointEnumerator& operator++() {
+  FloatingPointEnumerator& operator++() override {
     const FloatingPoint current(createFP());
     if (current.isNaN()) {
       d_enumerationComplete = true;
@@ -92,7 +92,7 @@ class RoundingModeEnumerator
     return NodeManager::currentNM()->mkConst(d_rm);
   }
 
-  RoundingModeEnumerator& operator++() {
+  RoundingModeEnumerator& operator++() override {
     switch (d_rm) {
       case roundNearestTiesToEven:
         d_rm = roundTowardPositive;