Enable -Wsuggest-override by default. (#1643)

Adds missing override keywords.

64 files changed, 694 insertions, 534 deletions

diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h
index 73798f94c..fa65214e7 100644
--- a/src/theory/arith/attempt_solution_simplex.h
+++ b/src/theory/arith/attempt_solution_simplex.h
@@ -67,11 +67,9 @@ public:
 
   Result::Sat attempt(const ApproximateSimplex::Solution& sol);
 
-  Result::Sat findModel(bool exactResult){
-    Unreachable();
-  }
+  Result::Sat findModel(bool exactResult) override { Unreachable(); }
 
-private:
+ private:
   bool matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const;
 
   bool processSignals(){
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index 3710ac5c0..f84550dcc 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -73,7 +73,7 @@ private:
   TheoryArithPrivate& d_arith;
 public:
   SetupLiteralCallBack(TheoryArithPrivate& ta);
-  void operator()(TNode lit);
+  void operator()(TNode lit) override;
 };
 
 class DeltaComputeCallback : public RationalCallBack {
@@ -81,7 +81,7 @@ private:
   const TheoryArithPrivate& d_ta;
 public:
   DeltaComputeCallback(const TheoryArithPrivate& ta);
-  Rational operator()() const;
+  Rational operator()() const override;
 };
 
 class BasicVarModelUpdateCallBack : public ArithVarCallBack{
@@ -89,7 +89,7 @@ private:
   TheoryArithPrivate& d_ta;
 public:
   BasicVarModelUpdateCallBack(TheoryArithPrivate& ta);
-  void operator()(ArithVar x);
+  void operator()(ArithVar x) override;
 };
 
 class TempVarMalloc : public ArithVarMalloc {
@@ -97,8 +97,8 @@ private:
   TheoryArithPrivate& d_ta;
 public:
   TempVarMalloc(TheoryArithPrivate& ta);
-  ArithVar request();
-  void release(ArithVar v);
+  ArithVar request() override;
+  void release(ArithVar v) override;
 };
 
 class RaiseConflict {
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 228f29838..5085dc841 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -61,17 +61,20 @@ private:
   public:
     ArithCongruenceNotify(ArithCongruenceManager& acm);
 
-    bool eqNotifyTriggerEquality(TNode equality, bool value);
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override;
 
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value);
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
 
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
+    bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override;
 
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2);
-    void eqNotifyNewClass(TNode t);
-    void eqNotifyPreMerge(TNode t1, TNode t2);
-    void eqNotifyPostMerge(TNode t1, TNode t2);
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
+    void eqNotifyNewClass(TNode t) override;
+    void eqNotifyPreMerge(TNode t1, TNode t2) override;
+    void eqNotifyPostMerge(TNode t1, TNode t2) override;
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
   };
   ArithCongruenceNotify d_notify;
   
diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h
index 2911592c7..10d18170e 100644
--- a/src/theory/arith/dual_simplex.h
+++ b/src/theory/arith/dual_simplex.h
@@ -63,7 +63,8 @@ class DualSimplexDecisionProcedure : public SimplexDecisionProcedure{
 public:
   DualSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
 
-  Result::Sat findModel(bool exactResult) {
+  Result::Sat findModel(bool exactResult) override
+  {
     return dualFindModel(exactResult);
   }
 
diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index c4f996f9f..a93fa88e8 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -66,7 +66,7 @@ class FCSimplexDecisionProcedure : public SimplexDecisionProcedure{
 public:
   FCSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
 
-  Result::Sat findModel(bool exactResult);
+  Result::Sat findModel(bool exactResult) override;
 
   // other error variables are dropping
   WitnessImprovement dualLikeImproveError(ArithVar evar);
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index c2fa99e31..0f2862a72 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -588,13 +588,16 @@ private:
     LinearEqualityModule* d_linEq;
   public:
     TrackingCallback(LinearEqualityModule* le) : d_linEq(le) {}
-    void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn){
+    void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) override
+    {
       d_linEq->trackingCoefficientChange(ridx, nb, oldSgn, currSgn);
     }
-    void multiplyRow(RowIndex ridx, int sgn){
+    void multiplyRow(RowIndex ridx, int sgn) override
+    {
       d_linEq->trackingMultiplyRow(ridx, sgn);
     }
-    bool canUseRow(RowIndex ridx) const {
+    bool canUseRow(RowIndex ridx) const override
+    {
       ArithVar basic = d_linEq->getTableau().rowIndexToBasic(ridx);
       return d_linEq->basicIsTracked(basic);
     }
@@ -746,7 +749,8 @@ private:
   LinearEqualityModule* d_mod;
 public:
   UpdateTrackingCallback(LinearEqualityModule* mod): d_mod(mod){}
-  void operator()(ArithVar v, const BoundsInfo& bi){
+  void operator()(ArithVar v, const BoundsInfo& bi) override
+  {
     d_mod->includeBoundUpdate(v, bi);
   }
 };
diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h
index 2e0a1ebb2..eda5b9dac 100644
--- a/src/theory/arith/matrix.h
+++ b/src/theory/arith/matrix.h
@@ -48,9 +48,9 @@ public:
 
 class NoEffectCCCB : public CoefficientChangeCallback {
 public:
-  void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn);
-  void multiplyRow(RowIndex ridx, int Sgn);
-  bool canUseRow(RowIndex ridx) const;
+ void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) override;
+ void multiplyRow(RowIndex ridx, int Sgn) override;
+ bool canUseRow(RowIndex ridx) const override;
 };
 
 template<class T>
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index 5f2233b3f..54a47ac4d 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -66,7 +66,7 @@ class SumOfInfeasibilitiesSPD : public SimplexDecisionProcedure {
 public:
   SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
 
-  Result::Sat findModel(bool exactResult);
+  Result::Sat findModel(bool exactResult) override;
 
   // other error variables are dropping
   WitnessImprovement dualLikeImproveError(ArithVar evar);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index caf466c0c..70cb574a8 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -277,7 +277,8 @@ class TheoryArrays : public Theory {
   public:
     NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {}
 
-    bool eqNotifyTriggerEquality(TNode equality, bool value) {
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override
+    {
       Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
       // Just forward to arrays
       if (value) {
@@ -287,7 +288,8 @@ class TheoryArrays : public Theory {
       }
     }
 
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+    {
       Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
       // Just forward to arrays
       if (value) {
@@ -297,7 +299,11 @@ class TheoryArrays : public Theory {
       }
     }
 
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+    bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override
+    {
       Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
       if (value) {
         if (t1.getType().isArray()) {
@@ -318,19 +324,21 @@ class TheoryArrays : public Theory {
       return true;
     }
 
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
+    {
       Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
       d_arrays.conflict(t1, t2);
     }
 
-    void eqNotifyNewClass(TNode t) { }
-    void eqNotifyPreMerge(TNode t1, TNode t2) { }
-    void eqNotifyPostMerge(TNode t1, TNode t2) {
+    void eqNotifyNewClass(TNode t) override {}
+    void eqNotifyPreMerge(TNode t1, TNode t2) override {}
+    void eqNotifyPostMerge(TNode t1, TNode t2) override
+    {
       if (t1.getType().isArray()) {
         d_arrays.mergeArrays(t1, t2);
       }
     }
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
   };
 
   /** The notify class for d_equalityEngine */
@@ -386,10 +394,12 @@ class TheoryArrays : public Theory {
     context::Context* d_satContext;
     context::Context* d_contextToPop;
   protected:
-    void contextNotifyPop() {
-      if (d_contextToPop->getLevel() > d_satContext->getLevel()) {
-        d_contextToPop->pop();
-      }
+   void contextNotifyPop() override
+   {
+     if (d_contextToPop->getLevel() > d_satContext->getLevel())
+     {
+       d_contextToPop->pop();
+     }
     }
   public:
     ContextPopper(context::Context* context, context::Context* contextToPop)
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 78e01f690..7c60505a5 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -79,10 +79,11 @@ private:
   class DataClearer : context::ContextNotifyObj {
     T& d_data;
   protected:
-    void contextNotifyPop() {
-      Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data "
-                            << "(size was " << d_data.size() << ")" << std::endl;
-      d_data.clear();
+   void contextNotifyPop() override
+   {
+     Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data "
+                           << "(size was " << d_data.size() << ")" << std::endl;
+     d_data.clear();
     }
   public:
     DataClearer(context::Context* context, T& data) :
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 9d5966628..cd9a9f904 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -33,11 +33,11 @@ public:
       : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo)
   {}
 
-  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 
   //void check(Effort);
-  
-  std::string identify() const { return std::string("TheoryBool"); }
+
+  std::string identify() const override { return std::string("TheoryBool"); }
 };/* class TheoryBool */
 
 }/* CVC4::theory::booleans namespace */
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index cfc59272c..14a38660b 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -31,7 +31,7 @@ public:
                 OutputChannel& out, Valuation valuation,
                 const LogicInfo& logicInfo)
       : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {}
-  std::string identify() const { return std::string("TheoryBuiltin"); }
+  std::string identify() const override { return std::string("TheoryBuiltin"); }
 };/* class TheoryBuiltin */
 
 }/* CVC4::theory::builtin namespace */
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 1dc2d8b1e..3bb701fdf 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -169,15 +169,15 @@ class TLazyBitblaster :  public TBitblaster<Node> {
 
   void addAtom(TNode atom);
   bool hasValue(TNode a);
-  Node getModelFromSatSolver(TNode a, bool fullModel);
+  Node getModelFromSatSolver(TNode a, bool fullModel) override;
 
-public:
-  void bbTerm(TNode node, Bits&  bits);
-  void bbAtom(TNode node);
-  Node getBBAtom(TNode atom) const;
-  void storeBBAtom(TNode atom, Node atom_bb);
-  void storeBBTerm(TNode node, const Bits& bits);
-  bool hasBBAtom(TNode atom) const; 
+ public:
+  void bbTerm(TNode node, Bits& bits) override;
+  void bbAtom(TNode node) override;
+  Node getBBAtom(TNode atom) const override;
+  void storeBBAtom(TNode atom, Node atom_bb) override;
+  void storeBBTerm(TNode node, const Bits& bits) override;
+  bool hasBBAtom(TNode atom) const override;
 
   TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
   ~TLazyBitblaster();
@@ -219,7 +219,7 @@ public:
    *
    * @param var
    */
-  void makeVariable(TNode var, Bits& bits);
+  void makeVariable(TNode var, Bits& bits) override;
 
   bool isSharedTerm(TNode node);
   uint64_t computeAtomWeight(TNode node, NodeSet& seen);
@@ -274,7 +274,7 @@ class EagerBitblaster : public TBitblaster<Node> {
   // This is either an MinisatEmptyNotify or NULL.
   MinisatEmptyNotify* d_notify;
 
-  Node getModelFromSatSolver(TNode a, bool fullModel);
+  Node getModelFromSatSolver(TNode a, bool fullModel) override;
   bool isSharedTerm(TNode node);
 
 public:
@@ -282,14 +282,14 @@ public:
   ~EagerBitblaster();
 
   void addAtom(TNode atom);
-  void makeVariable(TNode node, Bits& bits);
-  void bbTerm(TNode node, Bits&  bits);
-  void bbAtom(TNode node);
-  Node getBBAtom(TNode node) const;
-  bool hasBBAtom(TNode atom) const;
+  void makeVariable(TNode node, Bits& bits) override;
+  void bbTerm(TNode node, Bits& bits) override;
+  void bbAtom(TNode node) override;
+  Node getBBAtom(TNode node) const override;
+  bool hasBBAtom(TNode atom) const override;
   void bbFormula(TNode formula);
-  void storeBBAtom(TNode atom, Node atom_bb);
-  void storeBBTerm(TNode node, const Bits& bits);
+  void storeBBAtom(TNode atom, Node atom_bb) override;
+  void storeBBTerm(TNode node, const Bits& bits) override;
 
   bool assertToSat(TNode node, bool propagate = true);
   bool solve();
@@ -303,7 +303,7 @@ public:
   BitblastingRegistrar(EagerBitblaster* bb)
     : d_bitblaster(bb)
   {}
-  void preRegister(Node n);
+  void preRegister(Node n) override;
 }; /* class Registrar */
 
 class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
@@ -322,9 +322,9 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
 
   void addAtom(TNode atom);
   void simplifyAig();
-  void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb);
-  Abc_Obj_t* getBBAtom(TNode atom) const;
-  bool hasBBAtom(TNode atom) const;
+  void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override;
+  Abc_Obj_t* getBBAtom(TNode atom) const override;
+  bool hasBBAtom(TNode atom) const override;
   void cacheAig(TNode node, Abc_Obj_t* aig);
   bool hasAig(TNode node);
   Abc_Obj_t* getAig(TNode node);
@@ -332,14 +332,18 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
   bool hasInput(TNode input);
   void convertToCnfAndAssert();
   void assertToSatSolver(Cnf_Dat_t* pCnf);
-  Node getModelFromSatSolver(TNode a, bool fullModel) { Unreachable(); }
-public:
+  Node getModelFromSatSolver(TNode a, bool fullModel) override
+  {
+    Unreachable();
+  }
+
+ public:
   AigBitblaster();
   ~AigBitblaster();
 
-  void makeVariable(TNode node, Bits& bits);
-  void bbTerm(TNode node, Bits&  bits);
-  void bbAtom(TNode node);
+  void makeVariable(TNode node, Bits& bits) override;
+  void bbTerm(TNode node, Bits& bits) override;
+  void bbAtom(TNode node) override;
   Abc_Obj_t* bbFormula(TNode formula);
   bool solve(TNode query); 
   static Abc_Aig_t* currentAigM();
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 30270b3c3..deba84631 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -201,11 +201,9 @@ class InequalityGraph : public context::ContextNotifyObj{
   Node makeDiseqSplitLemma(TNode diseq); 
   /** Backtracking mechanisms **/
   std::vector<std::pair<TermId, InequalityEdge> > d_undoStack;
-  context::CDO<unsigned> d_undoStackIndex; 
-  
-  void contextNotifyPop() {
-    backtrack();
-  }
+  context::CDO<unsigned> d_undoStackIndex;
+
+  void contextNotifyPop() override { backtrack(); }
 
   void backtrack(); 
 
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index 0534c0f17..c963f15d7 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -224,16 +224,19 @@ public:
   AlgebraicSolver(context::Context* c, TheoryBV* bv);
   ~AlgebraicSolver();
 
-  void  preRegister(TNode node) {}
-  bool  check(Theory::Effort e);
-  void  explain(TNode literal, std::vector<TNode>& assumptions) {Unreachable("AlgebraicSolver does not propagate.\n");}
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
-  bool collectModelInfo(TheoryModel* m, bool fullModel);
-  Node getModelValue(TNode node); 
-  bool isComplete();
-  virtual void assertFact(TNode fact);
+  void preRegister(TNode node) override {}
+  bool check(Theory::Effort e) override;
+  void explain(TNode literal, std::vector<TNode>& assumptions) override
+  {
+    Unreachable("AlgebraicSolver does not propagate.\n");
+  }
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+  bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+  Node getModelValue(TNode node) override;
+  bool isComplete() override;
+  void assertFact(TNode fact) override;
 };
 
-}
-}
-}
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 5927feddc..f88810fca 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -65,17 +65,17 @@ public:
   BitblastSolver(context::Context* c, TheoryBV* bv);
   ~BitblastSolver();
 
-  void  preRegister(TNode node);
-  bool  check(Theory::Effort e);
-  void  explain(TNode literal, std::vector<TNode>& assumptions);
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
-  bool collectModelInfo(TheoryModel* m, bool fullModel);
-  Node getModelValue(TNode node);
-  bool isComplete() { return true; }
+  void preRegister(TNode node) override;
+  bool check(Theory::Effort e) override;
+  void explain(TNode literal, std::vector<TNode>& assumptions) override;
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+  bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+  Node getModelValue(TNode node) override;
+  bool isComplete() override { return true; }
   void bitblastQueue();
   void setAbstraction(AbstractionModule* module);
   uint64_t computeAtomWeight(TNode atom);
-  void setProofLog( BitVectorProof * bvp );
+  void setProofLog(BitVectorProof* bvp) override;
 };
 
 } /* namespace CVC4::theory::bv */
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 6cc6253ff..05c9535c3 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -53,14 +53,17 @@ class CoreSolver : public SubtheorySolver {
 
   public:
     NotifyClass(CoreSolver& solver): d_solver(solver) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value);
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value);
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2);
-    void eqNotifyNewClass(TNode t);
-    void eqNotifyPreMerge(TNode t1, TNode t2) { }
-    void eqNotifyPostMerge(TNode t1, TNode t2) { }
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override;
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
+    bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override;
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
+    void eqNotifyNewClass(TNode t) override;
+    void eqNotifyPreMerge(TNode t1, TNode t2) override {}
+    void eqNotifyPostMerge(TNode t1, TNode t2) override {}
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
   };
 
 
@@ -100,17 +103,19 @@ class CoreSolver : public SubtheorySolver {
 public:
   CoreSolver(context::Context* c, TheoryBV* bv);
   ~CoreSolver();
-  bool  isComplete() { return d_isComplete; }
+  bool isComplete() override { return d_isComplete; }
   void  setMasterEqualityEngine(eq::EqualityEngine* eq);
-  void  preRegister(TNode node);
-  bool  check(Theory::Effort e);
-  void  explain(TNode literal, std::vector<TNode>& assumptions);
-  bool collectModelInfo(TheoryModel* m, bool fullModel);
-  Node  getModelValue(TNode var);
-  void  addSharedTerm(TNode t) {
+  void preRegister(TNode node) override;
+  bool check(Theory::Effort e) override;
+  void explain(TNode literal, std::vector<TNode>& assumptions) override;
+  bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+  Node getModelValue(TNode var) override;
+  void addSharedTerm(TNode t) override
+  {
     d_equalityEngine.addTriggerTerm(t, THEORY_BV);
   }
-  EqualityStatus getEqualityStatus(TNode a, TNode b) {
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override
+  {
     if (d_equalityEngine.areEqual(a, b)) {
       // The terms are implied to be equal
       return EQUALITY_TRUE;
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index be0492125..620cd075b 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -65,15 +65,15 @@ public:
       d_statistics()
   {}
 
-  bool check(Theory::Effort e);
-  void propagate(Theory::Effort e);
-  void explain(TNode literal, std::vector<TNode>& assumptions);
-  bool isComplete() { return d_isComplete; }
-  bool collectModelInfo(TheoryModel* m, bool fullModel);
-  Node getModelValue(TNode var);
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
-  void assertFact(TNode fact);
-  void preRegister(TNode node);
+  bool check(Theory::Effort e) override;
+  void propagate(Theory::Effort e) override;
+  void explain(TNode literal, std::vector<TNode>& assumptions) override;
+  bool isComplete() override { return d_isComplete; }
+  bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+  Node getModelValue(TNode var) override;
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+  void assertFact(TNode fact) override;
+  void preRegister(TNode node) override;
 };
 
 }
diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index 718121499..dd65fc08f 100644
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -42,20 +42,21 @@ public:
     d_bits(0) {
   }
 
-  Node operator*() {
+  Node operator*() override
+  {
     if(d_bits != d_bits.modByPow2(d_size)) {
       throw NoMoreValuesException(getType());
     }
     return utils::mkConst(d_size, d_bits);
   }
 
-  BitVectorEnumerator& operator++()
+  BitVectorEnumerator& operator++() override
   {
     d_bits += 1;
     return *this;
   }
 
-  bool isFinished() { return d_bits != d_bits.modByPow2(d_size); }
+  bool isFinished() override { return d_bits != d_bits.modByPow2(d_size); }
 };/* BitVectorEnumerator */
 
 }/* CVC4::theory::bv namespace */
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 8052df59a..a27fd5543 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -64,7 +64,8 @@ class TheoryDatatypes : public Theory {
     TheoryDatatypes& d_dt;
   public:
     NotifyClass(TheoryDatatypes& dt): d_dt(dt) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value) {
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override
+    {
       Debug("dt") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
       if (value) {
         return d_dt.propagate(equality);
@@ -73,7 +74,8 @@ class TheoryDatatypes : public Theory {
         return d_dt.propagate(equality.notNode());
       }
     }
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+    {
       Debug("dt") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
       if (value) {
         return d_dt.propagate(predicate);
@@ -81,7 +83,11 @@ class TheoryDatatypes : public Theory {
        return d_dt.propagate(predicate.notNode());
       }
     }
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+    bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override
+    {
       Debug("dt") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
       if (value) {
         return d_dt.propagate(t1.eqNode(t2));
@@ -89,23 +95,28 @@ class TheoryDatatypes : public Theory {
         return d_dt.propagate(t1.eqNode(t2).notNode());
       }
     }
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
+    {
       Debug("dt") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
       d_dt.conflict(t1, t2);
     }
-    void eqNotifyNewClass(TNode t) {
+    void eqNotifyNewClass(TNode t) override
+    {
       Debug("dt") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl;
       d_dt.eqNotifyNewClass(t);
     }
-    void eqNotifyPreMerge(TNode t1, TNode t2) {
+    void eqNotifyPreMerge(TNode t1, TNode t2) override
+    {
       Debug("dt") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl;
       d_dt.eqNotifyPreMerge(t1, t2);
     }
-    void eqNotifyPostMerge(TNode t1, TNode t2) {
+    void eqNotifyPostMerge(TNode t1, TNode t2) override
+    {
       Debug("dt") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl;
       d_dt.eqNotifyPostMerge(t1, t2);
     }
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
+    {
       Debug("dt") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl;
       d_dt.eqNotifyDisequal(t1, t2, reason);
     }
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index ca80546b8..688c6e600 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -62,15 +62,17 @@ class TheoryFp : public Theory {
 
    public:
     NotifyClass(TheoryFp& solver) : d_theorySolver(solver) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value);
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value);
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2,
-                                     bool value);
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2);
-    void eqNotifyNewClass(TNode t) {}
-    void eqNotifyPreMerge(TNode t1, TNode t2) {}
-    void eqNotifyPostMerge(TNode t1, TNode t2) {}
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {}
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override;
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
+    bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override;
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
+    void eqNotifyNewClass(TNode t) override {}
+    void eqNotifyPreMerge(TNode t1, TNode t2) override {}
+    void eqNotifyPostMerge(TNode t1, TNode t2) override {}
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
   };
   friend NotifyClass;
 
diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h
index 625770869..7b05fc890 100644
--- a/src/theory/idl/theory_idl.h
+++ b/src/theory/idl/theory_idl.h
@@ -48,13 +48,13 @@ public:
             Valuation valuation, const LogicInfo& logicInfo);
 
   /** Pre-processing of input atoms */
-  Node ppRewrite(TNode atom);
+  Node ppRewrite(TNode atom) override;
 
   /** Check the assertions for satisfiability */
-  void check(Effort effort);
+  void check(Effort effort) override;
 
   /** Identity string */
-  std::string identify() const { return "THEORY_IDL"; }
+  std::string identify() const override { return "THEORY_IDL"; }
 
 };/* class TheoryIdl */
 
diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h
index bf8b99f1c..6967c6c42 100644
--- a/src/theory/quantifiers/anti_skolem.h
+++ b/src/theory/quantifiers/anti_skolem.h
@@ -40,12 +40,12 @@ public:
                                bool pconnected = true );
 
   /* Call during quantifier engine's check */
-  void check(Theory::Effort e, QEffort quant_e);
+  void check(Theory::Effort e, QEffort quant_e) override;
   /* Called for new quantifiers */
-  void registerQuantifier( Node q ) {}
-  void assertNode( Node n ) {}
+  void registerQuantifier(Node q) override {}
+  void assertNode(Node n) override {}
   /** Identify this module (for debugging, dynamic configuration, etc..) */
-  std::string identify() const { return "QuantAntiSkolem"; }
+  std::string identify() const override { return "QuantAntiSkolem"; }
 
  private:
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index 03983fe1a..c12890b83 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -748,11 +748,11 @@ public:
   bool useModelValue(CegInstantiator* ci,
                      SolvedForm& sf,
                      Node pv,
-                     CegInstEffort effort)
+                     CegInstEffort effort) override
   {
     return true;
   }
-  std::string identify() const { return "ModelValue"; }
+  std::string identify() const override { return "ModelValue"; }
 };
 
 /** instantiator preprocess
diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
index e6e64201e..bb210edcc 100644
--- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
@@ -934,11 +934,13 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery
   }
   ~CegInstantiatorBvInverterQuery() {}
   /** return the model value of n */
-  Node getModelValue( Node n ) {
-    return d_ci->getModelValue( n );
-  }
+  Node getModelValue(Node n) override { return d_ci->getModelValue(n); }
   /** get bound variable of type tn */
-  Node getBoundVariable(TypeNode tn) { return d_ci->getBoundVariable(tn); }
+  Node getBoundVariable(TypeNode tn) override
+  {
+    return d_ci->getBoundVariable(tn);
+  }
+
  protected:
   // pointer to class that is able to query model values
   CegInstantiator * d_ci;
diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.h b/src/theory/quantifiers/cegqi/ceg_t_instantiator.h
index b9c7e2024..eee6747ec 100644
--- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.h
@@ -33,57 +33,56 @@ class ArithInstantiator : public Instantiator {
  public:
   ArithInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
   virtual ~ArithInstantiator(){}
-  virtual void reset(CegInstantiator* ci,
-                     SolvedForm& sf,
-                     Node pv,
-                     CegInstEffort effort) override;
-  virtual bool hasProcessEquality(CegInstantiator* ci,
-                                  SolvedForm& sf,
-                                  Node pv,
-                                  CegInstEffort effort) override
+  void reset(CegInstantiator* ci,
+             SolvedForm& sf,
+             Node pv,
+             CegInstEffort effort) override;
+  bool hasProcessEquality(CegInstantiator* ci,
+                          SolvedForm& sf,
+                          Node pv,
+                          CegInstEffort effort) override
   {
     return true;
   }
-  virtual bool processEquality(CegInstantiator* ci,
-                               SolvedForm& sf,
-                               Node pv,
-                               std::vector<TermProperties>& term_props,
-                               std::vector<Node>& terms,
-                               CegInstEffort effort) override;
-  virtual bool hasProcessAssertion(CegInstantiator* ci,
-                                   SolvedForm& sf,
-                                   Node pv,
-                                   CegInstEffort effort) override
+  bool processEquality(CegInstantiator* ci,
+                       SolvedForm& sf,
+                       Node pv,
+                       std::vector<TermProperties>& term_props,
+                       std::vector<Node>& terms,
+                       CegInstEffort effort) override;
+  bool hasProcessAssertion(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           CegInstEffort effort) override
   {
     return true;
   }
-  virtual Node hasProcessAssertion(CegInstantiator* ci,
-                                   SolvedForm& sf,
-                                   Node pv,
-                                   Node lit,
-                                   CegInstEffort effort) override;
-  virtual bool processAssertion(CegInstantiator* ci,
-                                SolvedForm& sf,
-                                Node pv,
-                                Node lit,
-                                Node alit,
-                                CegInstEffort effort) override;
-  virtual bool processAssertions(CegInstantiator* ci,
-                                 SolvedForm& sf,
-                                 Node pv,
-                                 CegInstEffort effort) override;
-  virtual bool needsPostProcessInstantiationForVariable(
-      CegInstantiator* ci,
-      SolvedForm& sf,
-      Node pv,
-      CegInstEffort effort) override;
-  virtual bool postProcessInstantiationForVariable(
-      CegInstantiator* ci,
-      SolvedForm& sf,
-      Node pv,
-      CegInstEffort effort,
-      std::vector<Node>& lemmas) override;
-  virtual std::string identify() const override { return "Arith"; }
+  Node hasProcessAssertion(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           Node lit,
+                           CegInstEffort effort) override;
+  bool processAssertion(CegInstantiator* ci,
+                        SolvedForm& sf,
+                        Node pv,
+                        Node lit,
+                        Node alit,
+                        CegInstEffort effort) override;
+  bool processAssertions(CegInstantiator* ci,
+                         SolvedForm& sf,
+                         Node pv,
+                         CegInstEffort effort) override;
+  bool needsPostProcessInstantiationForVariable(CegInstantiator* ci,
+                                                SolvedForm& sf,
+                                                Node pv,
+                                                CegInstEffort effort) override;
+  bool postProcessInstantiationForVariable(CegInstantiator* ci,
+                                           SolvedForm& sf,
+                                           Node pv,
+                                           CegInstEffort effort,
+                                           std::vector<Node>& lemmas) override;
+  std::string identify() const override { return "Arith"; }
+
  private:
   Node d_vts_sym[2];
   std::vector<Node> d_mbp_bounds[2];
@@ -113,29 +112,30 @@ class DtInstantiator : public Instantiator {
 public:
   DtInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
   virtual ~DtInstantiator(){}
-  virtual void reset(CegInstantiator* ci,
-                     SolvedForm& sf,
-                     Node pv,
-                     CegInstEffort effort) override;
-  virtual bool processEqualTerms(CegInstantiator* ci,
-                                 SolvedForm& sf,
-                                 Node pv,
-                                 std::vector<Node>& eqc,
-                                 CegInstEffort effort) override;
-  virtual bool hasProcessEquality(CegInstantiator* ci,
-                                  SolvedForm& sf,
-                                  Node pv,
-                                  CegInstEffort effort) override
+  void reset(CegInstantiator* ci,
+             SolvedForm& sf,
+             Node pv,
+             CegInstEffort effort) override;
+  bool processEqualTerms(CegInstantiator* ci,
+                         SolvedForm& sf,
+                         Node pv,
+                         std::vector<Node>& eqc,
+                         CegInstEffort effort) override;
+  bool hasProcessEquality(CegInstantiator* ci,
+                          SolvedForm& sf,
+                          Node pv,
+                          CegInstEffort effort) override
   {
     return true;
   }
-  virtual bool processEquality(CegInstantiator* ci,
-                               SolvedForm& sf,
-                               Node pv,
-                               std::vector<TermProperties>& term_props,
-                               std::vector<Node>& terms,
-                               CegInstEffort effort) override;
-  virtual std::string identify() const override { return "Dt"; }
+  bool processEquality(CegInstantiator* ci,
+                       SolvedForm& sf,
+                       Node pv,
+                       std::vector<TermProperties>& term_props,
+                       std::vector<Node>& terms,
+                       CegInstEffort effort) override;
+  std::string identify() const override { return "Dt"; }
+
  private:
   Node solve_dt(Node v, Node a, Node b, Node sa, Node sb);
 };
@@ -146,22 +146,23 @@ class EprInstantiator : public Instantiator {
  public:
   EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
   virtual ~EprInstantiator(){}
-  virtual void reset(CegInstantiator* ci,
-                     SolvedForm& sf,
-                     Node pv,
-                     CegInstEffort effort) override;
-  virtual bool processEqualTerm(CegInstantiator* ci,
-                                SolvedForm& sf,
-                                Node pv,
-                                TermProperties& pv_prop,
-                                Node n,
-                                CegInstEffort effort) override;
-  virtual bool processEqualTerms(CegInstantiator* ci,
-                                 SolvedForm& sf,
-                                 Node pv,
-                                 std::vector<Node>& eqc,
-                                 CegInstEffort effort) override;
-  virtual std::string identify() const override { return "Epr"; }
+  void reset(CegInstantiator* ci,
+             SolvedForm& sf,
+             Node pv,
+             CegInstEffort effort) override;
+  bool processEqualTerm(CegInstantiator* ci,
+                        SolvedForm& sf,
+                        Node pv,
+                        TermProperties& pv_prop,
+                        Node n,
+                        CegInstEffort effort) override;
+  bool processEqualTerms(CegInstantiator* ci,
+                         SolvedForm& sf,
+                         Node pv,
+                         std::vector<Node>& eqc,
+                         CegInstEffort effort) override;
+  std::string identify() const override { return "Epr"; }
+
  private:
   std::vector<Node> d_equal_terms;
   void computeMatchScore(CegInstantiator* ci,
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
index 3443d2c4d..2bc86ef4e 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
@@ -103,16 +103,16 @@ class InstStrategyCbqi : public QuantifiersModule {
   /** whether to do CBQI for quantifier q */
   bool doCbqi( Node q );
   /** process functions */
-  bool needsCheck( Theory::Effort e );
-  QEffort needsModel(Theory::Effort e);
-  void reset_round( Theory::Effort e );
-  void check(Theory::Effort e, QEffort quant_e);
-  bool checkComplete();
-  bool checkCompleteFor( Node q );
-  void preRegisterQuantifier( Node q );
-  void registerQuantifier( Node q );
+  bool needsCheck(Theory::Effort e) override;
+  QEffort needsModel(Theory::Effort e) override;
+  void reset_round(Theory::Effort e) override;
+  void check(Theory::Effort e, QEffort quant_e) override;
+  bool checkComplete() override;
+  bool checkCompleteFor(Node q) override;
+  void preRegisterQuantifier(Node q) override;
+  void registerQuantifier(Node q) override;
   /** get next decision request */
-  Node getNextDecisionRequest( unsigned& priority );
+  Node getNextDecisionRequest(unsigned& priority) override;
 };
 
 //generalized counterexample guided quantifier instantiation
@@ -123,9 +123,9 @@ class CegqiOutputInstStrategy : public CegqiOutput {
 public:
   CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){}
   InstStrategyCegqi * d_out;
-  bool doAddInstantiation( std::vector< Node >& subs );
-  bool isEligibleForInstantiation( Node n );
-  bool addLemma( Node lem );
+  bool doAddInstantiation(std::vector<Node>& subs) override;
+  bool isEligibleForInstantiation(Node n) override;
+  bool addLemma(Node lem) override;
 };
 
 class InstStrategyCegqi : public InstStrategyCbqi {
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 85a7d3eb4..764379e76 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -237,14 +237,35 @@ private:
     ConjectureGenerator& d_sg;
   public:
     NotifyClass(ConjectureGenerator& sg): d_sg(sg) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) { }
-    void eqNotifyNewClass(TNode t) { d_sg.eqNotifyNewClass(t); }
-    void eqNotifyPreMerge(TNode t1, TNode t2) { d_sg.eqNotifyPreMerge(t1, t2); }
-    void eqNotifyPostMerge(TNode t1, TNode t2) { d_sg.eqNotifyPostMerge(t1, t2); }
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {d_sg.eqNotifyDisequal(t1, t2, reason); }
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override
+    {
+      return true;
+    }
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+    {
+      return true;
+    }
+    bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override
+    {
+      return true;
+    }
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
+    void eqNotifyNewClass(TNode t) override { d_sg.eqNotifyNewClass(t); }
+    void eqNotifyPreMerge(TNode t1, TNode t2) override
+    {
+      d_sg.eqNotifyPreMerge(t1, t2);
+    }
+    void eqNotifyPostMerge(TNode t1, TNode t2) override
+    {
+      d_sg.eqNotifyPostMerge(t1, t2);
+    }
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
+    {
+      d_sg.eqNotifyDisequal(t1, t2, reason);
+    }
   };/* class ConjectureGenerator::NotifyClass */
   /** The notify class */
   NotifyClass d_notify;
@@ -401,18 +422,18 @@ public:
   ConjectureGenerator( QuantifiersEngine * qe, context::Context* c );
 
   /* needs check */
-  bool needsCheck( Theory::Effort e );
+  bool needsCheck(Theory::Effort e) override;
   /* reset at a round */
-  void reset_round( Theory::Effort e );
+  void reset_round(Theory::Effort e) override;
   /* Call during quantifier engine's check */
-  void check(Theory::Effort e, QEffort quant_e);
+  void check(Theory::Effort e, QEffort quant_e) override;
   /* Called for new quantifiers */
-  void registerQuantifier( Node q );
-  void assertNode( Node n );
+  void registerQuantifier(Node q) override;
+  void assertNode(Node n) override;
   /** Identify this module (for debugging, dynamic configuration, etc..) */
-  std::string identify() const { return "ConjectureGenerator"; }
-//options
-private:
+  std::string identify() const override { return "ConjectureGenerator"; }
+  // options
+ private:
   bool optReqDistinctVarPatterns();
   bool optFilterUnknown();
   int optFilterScoreThreshold();
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h
index 41fec5e5f..85bb09086 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.h
+++ b/src/theory/quantifiers/ematching/ho_trigger.h
@@ -122,7 +122,7 @@ class HigherOrderTrigger : public Trigger
    * Extends Trigger::addInstantiations to also send
    * lemmas based on addHoTypeMatchPredicateLemmas.
    */
-  virtual int addInstantiations() override;
+  int addInstantiations() override;
 
  protected:
   /**
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index 8f11dfedf..eba49fa9a 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -40,9 +40,10 @@ private:
   /** counter for quantifiers */
   std::map< Node, int > d_counter;
   /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
-public:
+  void processResetInstantiationRound(Theory::Effort effort) override;
+  int process(Node f, Theory::Effort effort, int e) override;
+
+ public:
   InstStrategyUserPatterns( QuantifiersEngine* ie ) :
       InstStrategy( ie ){}
   ~InstStrategyUserPatterns(){}
@@ -54,7 +55,7 @@ public:
   /** get user pattern */
   inst::Trigger* getUserGenerator( Node q, int i ) { return d_user_gen[q][ i ]; }
   /** identify */
-  std::string identify() const { return std::string("UserPatterns"); }
+  std::string identify() const override { return std::string("UserPatterns"); }
 };/* class InstStrategyUserPatterns */
 
 class InstStrategyAutoGenTriggers : public InstStrategy {
@@ -89,16 +90,16 @@ private:
   std::map< Node, Node > d_pat_to_mpat;
 private:
   /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node q, Theory::Effort effort, int e );
-  /** generate triggers */
-  void generateTriggers( Node q );
-  void addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat );
-  void addTrigger( inst::Trigger * tr, Node f );
-  /** has user patterns */
-  bool hasUserPatterns( Node q );
-  /** has user patterns */
-  std::map< Node, bool > d_hasUserPatterns;
+ void processResetInstantiationRound(Theory::Effort effort) override;
+ int process(Node q, Theory::Effort effort, int e) override;
+ /** generate triggers */
+ void generateTriggers(Node q);
+ void addPatternToPool(Node q, Node pat, unsigned num_fv, Node mpat);
+ void addTrigger(inst::Trigger* tr, Node f);
+ /** has user patterns */
+ bool hasUserPatterns(Node q);
+ /** has user patterns */
+ std::map<Node, bool> d_hasUserPatterns;
 public:
   InstStrategyAutoGenTriggers( QuantifiersEngine* qe );
   ~InstStrategyAutoGenTriggers(){}
@@ -106,7 +107,10 @@ public:
   /** get auto-generated trigger */
   inst::Trigger* getAutoGenTrigger( Node q );
   /** identify */
-  std::string identify() const { return std::string("AutoGenTriggers"); }
+  std::string identify() const override
+  {
+    return std::string("AutoGenTriggers");
+  }
   /** add pattern */
   void addUserNoPattern( Node q, Node pat );
 };/* class InstStrategyAutoGenTriggers */
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index 18b5ea19c..32ddb19ed 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -76,19 +76,19 @@ class InstantiationEngine : public QuantifiersModule {
  public:
   InstantiationEngine(QuantifiersEngine* qe);
   ~InstantiationEngine();
-  void presolve();
-  bool needsCheck(Theory::Effort e);
-  void reset_round(Theory::Effort e);
-  void check(Theory::Effort e, QEffort quant_e);
-  bool checkCompleteFor(Node q);
-  void preRegisterQuantifier(Node q);
-  void registerQuantifier(Node q);
+  void presolve() override;
+  bool needsCheck(Theory::Effort e) override;
+  void reset_round(Theory::Effort e) override;
+  void check(Theory::Effort e, QEffort quant_e) override;
+  bool checkCompleteFor(Node q) override;
+  void preRegisterQuantifier(Node q) override;
+  void registerQuantifier(Node q) override;
   Node explain(TNode n) { return Node::null(); }
   /** add user pattern */
   void addUserPattern(Node q, Node pat);
   void addUserNoPattern(Node q, Node pat);
   /** Identify this module */
-  std::string identify() const { return "InstEngine"; }
+  std::string identify() const override { return "InstEngine"; }
 }; /* class InstantiationEngine */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index 0048cc14f..0b28f53c6 100644
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -50,26 +50,26 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery
   EqualityQueryQuantifiersEngine(context::Context* c, QuantifiersEngine* qe);
   virtual ~EqualityQueryQuantifiersEngine();
   /** reset */
-  virtual bool reset(Theory::Effort e);
+  bool reset(Theory::Effort e) override;
   /* Called for new quantifiers */
-  virtual void registerQuantifier(Node q) {}
+  void registerQuantifier(Node q) override {}
   /** identify */
-  virtual std::string identify() const { return "EqualityQueryQE"; }
+  std::string identify() const override { return "EqualityQueryQE"; }
   /** does the equality engine have term a */
-  bool hasTerm(Node a);
+  bool hasTerm(Node a) override;
   /** get the representative of a */
-  Node getRepresentative(Node a);
+  Node getRepresentative(Node a) override;
   /** are a and b equal? */
-  bool areEqual(Node a, Node b);
+  bool areEqual(Node a, Node b) override;
   /** are a and b disequal? */
-  bool areDisequal(Node a, Node b);
+  bool areDisequal(Node a, Node b) override;
   /** get equality engine
   * This may either be the master equality engine or the model's equality
   * engine.
   */
-  eq::EqualityEngine* getEngine();
+  eq::EqualityEngine* getEngine() override;
   /** get list of members in the equivalence class of a */
-  void getEquivalenceClass(Node a, std::vector<Node>& eqc);
+  void getEquivalenceClass(Node a, std::vector<Node>& eqc) override;
   /** get congruent term
   * If possible, returns a term n such that:
   * (1) n is a term in the equality engine from getEngine().
@@ -80,7 +80,7 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery
   * Notice that f should be a "match operator", returned by
   * TermDb::getMatchOperator.
   */
-  TNode getCongruentTerm(Node f, std::vector<TNode>& args);
+  TNode getCongruentTerm(Node f, std::vector<TNode>& args) override;
   /** gets the current best representative in the equivalence
    * class of a, based on some heuristic. Currently, the default heuristic
    * chooses terms that were previously chosen as representatives
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index f33151b4d..db2f97b16 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -67,19 +67,19 @@ class QRepBoundExt : public RepBoundExt
   QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {}
   virtual ~QRepBoundExt() {}
   /** set bound */
-  virtual RepSetIterator::RsiEnumType setBound(
-      Node owner, unsigned i, std::vector<Node>& elements) override;
+  RepSetIterator::RsiEnumType setBound(Node owner,
+                                       unsigned i,
+                                       std::vector<Node>& elements) override;
   /** reset index */
-  virtual bool resetIndex(RepSetIterator* rsi,
-                          Node owner,
-                          unsigned i,
-                          bool initial,
-                          std::vector<Node>& elements) override;
+  bool resetIndex(RepSetIterator* rsi,
+                  Node owner,
+                  unsigned i,
+                  bool initial,
+                  std::vector<Node>& elements) override;
   /** initialize representative set for type */
-  virtual bool initializeRepresentativesForType(TypeNode tn) override;
+  bool initializeRepresentativesForType(TypeNode tn) override;
   /** get variable order */
-  virtual bool getVariableOrder(Node owner,
-                                std::vector<unsigned>& varOrder) override;
+  bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder) override;
 
  private:
   /** quantifiers engine associated with this bound */
@@ -215,11 +215,11 @@ private:
 public:
   FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
 
-  FirstOrderModelIG * asFirstOrderModelIG() { return this; }
+  FirstOrderModelIG* asFirstOrderModelIG() override { return this; }
   // initialize the model
-  void processInitialize( bool ispre );
+  void processInitialize(bool ispre) override;
   //for initialize model
-  void processInitializeModelForTerm( Node n );
+  void processInitializeModelForTerm(Node n) override;
   /** reset evaluation */
   void resetEvaluate();
   /** evaluate functions */
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 99d77a8e7..3e990067a 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -102,10 +102,10 @@ private:
     context::CDO< bool > d_has_range;
     context::CDO< int > d_curr_range;
     IntBoolMap d_ranges_proxied;
-    void initialize();
-    void assertNode(Node n);
-    Node getNextDecisionRequest();
-    bool proxyCurrentRange();
+    void initialize() override;
+    void assertNode(Node n) override;
+    Node getNextDecisionRequest() override;
+    bool proxyCurrentRange() override;
   };
 private:
   //information for minimizing ranges
@@ -142,14 +142,14 @@ private:
 public:
   BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
   virtual ~BoundedIntegers();
-  
-  void presolve();
-  bool needsCheck( Theory::Effort e );
-  void check(Theory::Effort e, QEffort quant_e);
-  void registerQuantifier( Node q );
-  void preRegisterQuantifier( Node q );
-  void assertNode( Node n );
-  Node getNextDecisionRequest( unsigned& priority );
+
+  void presolve() override;
+  bool needsCheck(Theory::Effort e) override;
+  void check(Theory::Effort e, QEffort quant_e) override;
+  void registerQuantifier(Node q) override;
+  void preRegisterQuantifier(Node q) override;
+  void assertNode(Node n) override;
+  Node getNextDecisionRequest(unsigned& priority) override;
   bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); }
   unsigned getBoundVarType( Node q, Node v );
   unsigned getNumBoundVars( Node q ) { return d_set[q].size(); }
@@ -171,7 +171,7 @@ public:
   bool getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements );
 
   /** Identify this module */
-  std::string identify() const { return "BoundedIntegers"; }
+  std::string identify() const override { return "BoundedIntegers"; }
 };
 
 }
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index 732f8be07..a64c33303 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -138,13 +138,15 @@ public:
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);
 
-  int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
+  int doExhaustiveInstantiation(FirstOrderModel* fm,
+                                Node f,
+                                int effort) override;
 
   Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
 
-  /** process build model */  
-  bool preProcessBuildModel(TheoryModel* m); 
-  bool processBuildModel(TheoryModel* m);
+  /** process build model */
+  bool preProcessBuildModel(TheoryModel* m) override;
+  bool processBuildModel(TheoryModel* m) override;
 
   bool useSimpleModels();
 };/* class FullModelChecker */
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 4eb592b3e..5af1e3451 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -31,7 +31,8 @@ class QModelBuilder : public TheoryEngineModelBuilder
 protected:
   //quantifiers engine
   QuantifiersEngine* d_qe;
-  bool preProcessBuildModel(TheoryModel* m); //must call preProcessBuildModelStd
+  // must call preProcessBuildModelStd
+  bool preProcessBuildModel(TheoryModel* m) override;
   bool preProcessBuildModelStd(TheoryModel* m);
   /** number of lemmas generated while building model */
   unsigned d_addedLemmas;
@@ -49,7 +50,7 @@ public:
   /** exist instantiation ? */
   virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
   //debug model
-  virtual void debugModel( TheoryModel* m );
+  void debugModel(TheoryModel* m) override;
   //statistics 
   unsigned getNumAddedLemmas() { return d_addedLemmas; }
   unsigned getNumTriedLemmas() { return d_triedLemmas; }
@@ -87,7 +88,7 @@ class QModelBuilderIG : public QModelBuilder
   //whether inst gen was done
   bool d_didInstGen;
   /** process build model */
-  virtual bool processBuildModel( TheoryModel* m );
+  bool processBuildModel(TheoryModel* m) override;
 
  protected:
   //reset
@@ -143,7 +144,9 @@ class QModelBuilderIG : public QModelBuilder
   // is quantifier active?
   bool isQuantifierActive( Node f );
   //do exhaustive instantiation
-  int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
+  int doExhaustiveInstantiation(FirstOrderModel* fm,
+                                Node f,
+                                int effort) override;
 
   //temporary stats
   int d_numQuantSat;
diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index 090374744..6412ea81b 100644
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -49,18 +49,18 @@ public:
   ModelEngine( context::Context* c, QuantifiersEngine* qe );
   virtual ~ModelEngine();
 public:
-  bool needsCheck( Theory::Effort e );
-  QEffort needsModel(Theory::Effort e);
-  void reset_round( Theory::Effort e );
-  void check(Theory::Effort e, QEffort quant_e);
-  bool checkComplete();
-  bool checkCompleteFor( Node q );
-  void registerQuantifier( Node f );
-  void assertNode( Node f );
-  Node explain(TNode n){ return Node::null(); }
-  void debugPrint( const char* c );
-  /** Identify this module */
-  std::string identify() const { return "ModelEngine"; }
+ bool needsCheck(Theory::Effort e) override;
+ QEffort needsModel(Theory::Effort e) override;
+ void reset_round(Theory::Effort e) override;
+ void check(Theory::Effort e, QEffort quant_e) override;
+ bool checkComplete() override;
+ bool checkCompleteFor(Node q) override;
+ void registerQuantifier(Node f) override;
+ void assertNode(Node f) override;
+ Node explain(TNode n) { return Node::null(); }
+ void debugPrint(const char* c);
+ /** Identify this module */
+ std::string identify() const override { return "ModelEngine"; }
 };/* class ModelEngine */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/fun_def_engine.h b/src/theory/quantifiers/fun_def_engine.h
index 48de4f36c..157eb57fd 100644
--- a/src/theory/quantifiers/fun_def_engine.h
+++ b/src/theory/quantifiers/fun_def_engine.h
@@ -38,17 +38,17 @@ public:
   ~FunDefEngine(){}
 
   /* whether this module needs to check this round */
-  bool needsCheck( Theory::Effort e );
+  bool needsCheck(Theory::Effort e) override;
   /* reset at a round */
-  void reset_round( Theory::Effort e );
+  void reset_round(Theory::Effort e) override;
   /* Call during quantifier engine's check */
-  void check(Theory::Effort e, QEffort quant_e);
+  void check(Theory::Effort e, QEffort quant_e) override;
   /* Called for new quantifiers */
-  void registerQuantifier( Node q );
+  void registerQuantifier(Node q) override;
   /** called for everything that gets asserted */
-  void assertNode( Node n );
+  void assertNode(Node n) override;
   /** Identify this module (for debugging, dynamic configuration, etc..) */
-  std::string identify() const { return "FunDefEngine"; }
+  std::string identify() const override { return "FunDefEngine"; }
 };
 
 
diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index 7f485750a..e0c72c9fa 100644
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -39,28 +39,29 @@ public:
   EqualityQueryInstProp( QuantifiersEngine* qe );
   ~EqualityQueryInstProp(){};
   /** reset */
-  virtual bool reset(Theory::Effort e);
+  bool reset(Theory::Effort e) override;
   /* Called for new quantifiers */
-  virtual void registerQuantifier(Node q) {}
+  void registerQuantifier(Node q) override {}
   /** identify */
-  virtual std::string identify() const { return "EqualityQueryInstProp"; }
+  std::string identify() const override { return "EqualityQueryInstProp"; }
   /** extends engine */
-  bool extendsEngine() { return true; }
+  bool extendsEngine() override { return true; }
   /** contains term */
-  bool hasTerm( Node a );
+  bool hasTerm(Node a) override;
   /** get the representative of the equivalence class of a */
-  Node getRepresentative( Node a );
+  Node getRepresentative(Node a) override;
   /** returns true if a and b are equal in the current context */
-  bool areEqual( Node a, Node b );
+  bool areEqual(Node a, Node b) override;
   /** returns true is a and b are disequal in the current context */
-  bool areDisequal( Node a, Node b );
+  bool areDisequal(Node a, Node b) override;
   /** get the equality engine associated with this query */
-  eq::EqualityEngine* getEngine();
+  eq::EqualityEngine* getEngine() override;
   /** get the equivalence class of a */
-  void getEquivalenceClass( Node a, std::vector< Node >& eqc );
+  void getEquivalenceClass(Node a, std::vector<Node>& eqc) override;
   /** get congruent term */
-  TNode getCongruentTerm( Node f, std::vector< TNode >& args );
-public:
+  TNode getCongruentTerm(Node f, std::vector<TNode>& args) override;
+
+ public:
   /** get the representative of the equivalence class of a, with explanation */
   Node getRepresentativeExp( Node a, std::vector< Node >& exp );
   /** returns true if a and b are equal in the current context */
@@ -114,15 +115,15 @@ private:
     InstPropagator& d_ip;
   public:
     InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}
-    virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
-                                     Node q,
-                                     Node lem,
-                                     std::vector<Node>& terms,
-                                     Node body)
+    bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
+                             Node q,
+                             Node lem,
+                             std::vector<Node>& terms,
+                             Node body) override
     {
       return d_ip.notifyInstantiation( quant_e, q, lem, terms, body );
     }
-    virtual void filterInstantiations() { d_ip.filterInstantiations(); }
+    void filterInstantiations() override { d_ip.filterInstantiations(); }
   };
   InstantiationNotifyInstPropagator d_notify;
   /** notify instantiation method */
@@ -173,11 +174,11 @@ public:
   InstPropagator( QuantifiersEngine* qe );
   ~InstPropagator(){}
   /** reset */
-  virtual bool reset(Theory::Effort e) override;
+  bool reset(Theory::Effort e) override;
   /* Called for new quantifiers */
-  virtual void registerQuantifier(Node q) override {}
+  void registerQuantifier(Node q) override {}
   /** identify */
-  virtual std::string identify() const override { return "InstPropagator"; }
+  std::string identify() const override { return "InstPropagator"; }
   /** get the notify mechanism */
   InstantiationNotify* getInstantiationNotify() { return &d_notify; }
 };
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index d1973eadb..18a06dc3d 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -93,13 +93,13 @@ class Instantiate : public QuantifiersUtil
   ~Instantiate();
 
   /** reset */
-  virtual bool reset(Theory::Effort e) override;
+  bool reset(Theory::Effort e) override;
   /** register quantifier */
-  virtual void registerQuantifier(Node q) override;
+  void registerQuantifier(Node q) override;
   /** identify */
-  virtual std::string identify() const override { return "Instantiate"; }
+  std::string identify() const override { return "Instantiate"; }
   /** check incomplete */
-  virtual bool checkComplete() override;
+  bool checkComplete() override;
 
   //--------------------------------------notify objects
   /** add instantiation notify
diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h
index 3b19b8d55..76a781e1c 100644
--- a/src/theory/quantifiers/local_theory_ext.h
+++ b/src/theory/quantifiers/local_theory_ext.h
@@ -56,22 +56,21 @@ private:
 public:
   LtePartialInst( QuantifiersEngine * qe, context::Context* c );
   /** determine whether this quantified formula will be reduced */
-  void preRegisterQuantifier( Node q );
+  void preRegisterQuantifier(Node q) override;
   /** was invoked */
   bool wasInvoked() { return d_wasInvoked; }
   
   /* whether this module needs to check this round */
-  bool needsCheck( Theory::Effort e );
+  bool needsCheck(Theory::Effort e) override;
   /* Call during quantifier engine's check */
-  void check(Theory::Effort e, QEffort quant_e);
+  void check(Theory::Effort e, QEffort quant_e) override;
   /* Called for new quantifiers */
-  void registerQuantifier( Node q ) {}
+  void registerQuantifier(Node q) override {}
   /* check complete */
-  bool checkComplete() { return !d_wasInvoked; }
-  void assertNode( Node n ) {}
+  bool checkComplete() override { return !d_wasInvoked; }
+  void assertNode(Node n) override {}
   /** Identify this module (for debugging, dynamic configuration, etc..) */
-  std::string identify() const { return "LtePartialInst"; }
-  
+  std::string identify() const override { return "LtePartialInst"; }
 };
 
 }
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 3448e967b..77ea530ae 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -238,10 +238,11 @@ public:
   QuantConflictFind( QuantifiersEngine * qe, context::Context* c );
 
   /** register quantifier */
-  void registerQuantifier( Node q );
-public:
+  void registerQuantifier(Node q) override;
+
+ public:
   /** assert quantifier */
-  void assertNode( Node q );
+  void assertNode(Node q) override;
   /** new node */
   void newEqClass( Node n );
   /** merge */
@@ -249,11 +250,11 @@ public:
   /** assert disequal */
   void assertDisequal( Node a, Node b );
   /** needs check */
-  bool needsCheck( Theory::Effort level );
+  bool needsCheck(Theory::Effort level) override;
   /** reset round */
-  void reset_round( Theory::Effort level );
+  void reset_round(Theory::Effort level) override;
   /** check */
-  void check(Theory::Effort level, QEffort quant_e);
+  void check(Theory::Effort level, QEffort quant_e) override;
 
  private:
   bool d_needs_computeRelEqr;
@@ -277,7 +278,7 @@ public:
   };
   Statistics d_statistics;
   /** Identify this module */
-  std::string identify() const { return "QcfEngine"; }
+  std::string identify() const override { return "QcfEngine"; }
 };
 
 std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e);
diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h
index 47adddd9e..aa201bbc3 100644
--- a/src/theory/quantifiers/quant_equality_engine.h
+++ b/src/theory/quantifiers/quant_equality_engine.h
@@ -37,14 +37,38 @@ private:
     QuantEqualityEngine& d_qee;
   public:
     NotifyClass(QuantEqualityEngine& qee): d_qee(qee) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) { d_qee.conflict(t1, t2); }
-    void eqNotifyNewClass(TNode t) { d_qee.eqNotifyNewClass(t); }
-    void eqNotifyPreMerge(TNode t1, TNode t2) { d_qee.eqNotifyPreMerge(t1, t2); }
-    void eqNotifyPostMerge(TNode t1, TNode t2) { d_qee.eqNotifyPostMerge(t1, t2); }
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {d_qee.eqNotifyDisequal(t1, t2, reason); }
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override
+    {
+      return true;
+    }
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+    {
+      return true;
+    }
+    bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override
+    {
+      return true;
+    }
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
+    {
+      d_qee.conflict(t1, t2);
+    }
+    void eqNotifyNewClass(TNode t) override { d_qee.eqNotifyNewClass(t); }
+    void eqNotifyPreMerge(TNode t1, TNode t2) override
+    {
+      d_qee.eqNotifyPreMerge(t1, t2);
+    }
+    void eqNotifyPostMerge(TNode t1, TNode t2) override
+    {
+      d_qee.eqNotifyPostMerge(t1, t2);
+    }
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
+    {
+      d_qee.eqNotifyDisequal(t1, t2, reason);
+    }
   };/* class ConjectureGenerator::NotifyClass */
   /** The notify class */
   NotifyClass d_notify;
@@ -75,17 +99,17 @@ public:
   QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c );
 
   /* whether this module needs to check this round */
-  bool needsCheck( Theory::Effort e );
+  bool needsCheck(Theory::Effort e) override;
   /* reset at a round */
-  void reset_round( Theory::Effort e );
+  void reset_round(Theory::Effort e) override;
   /* Call during quantifier engine's check */
-  void check(Theory::Effort e, QEffort quant_e);
+  void check(Theory::Effort e, QEffort quant_e) override;
   /* Called for new quantifiers */
-  void registerQuantifier( Node q );
+  void registerQuantifier(Node q) override;
   /** called for everything that gets asserted */
-  void assertNode( Node n );
+  void assertNode(Node n) override;
   /** Identify this module (for debugging, dynamic configuration, etc..) */
-  std::string identify() const { return "QuantEqualityEngine"; }
+  std::string identify() const override { return "QuantEqualityEngine"; }
   /** queries */
   bool areUnivDisequal( TNode n1, TNode n2 );
   bool areUnivEqual( TNode n1, TNode n2 );
diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h
index 3182df34b..0650b1c42 100644
--- a/src/theory/quantifiers/quant_relevance.h
+++ b/src/theory/quantifiers/quant_relevance.h
@@ -42,11 +42,11 @@ class QuantRelevance : public QuantifiersUtil
   QuantRelevance(bool cr) : d_computeRel(cr) {}
   ~QuantRelevance() {}
   /** reset */
-  virtual bool reset(Theory::Effort e) override { return true; }
+  bool reset(Theory::Effort e) override { return true; }
   /** register quantifier */
-  virtual void registerQuantifier(Node q) override;
+  void registerQuantifier(Node q) override;
   /** identify */
-  virtual std::string identify() const override { return "QuantRelevance"; }
+  std::string identify() const override { return "QuantRelevance"; }
   /** set relevance of symbol s to r */
   void setRelevance(Node s, int r);
   /** get relevance of symbol s */
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index 644583f04..1ea57433a 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -34,18 +34,18 @@ private:
 public:
   QuantDSplit( QuantifiersEngine * qe, context::Context* c );
   /** determine whether this quantified formula will be reduced */
-  void preRegisterQuantifier( Node q );
-  
+  void preRegisterQuantifier(Node q) override;
+
   /* whether this module needs to check this round */
-  bool needsCheck( Theory::Effort e );
+  bool needsCheck(Theory::Effort e) override;
   /* Call during quantifier engine's check */
-  void check(Theory::Effort e, QEffort quant_e);
+  void check(Theory::Effort e, QEffort quant_e) override;
   /* Called for new quantifiers */
-  void registerQuantifier( Node q ) {}
-  void assertNode( Node n ) {}
-  bool checkCompleteFor( Node q );
+  void registerQuantifier(Node q) override {}
+  void assertNode(Node n) override {}
+  bool checkCompleteFor(Node q) override;
   /** Identify this module (for debugging, dynamic configuration, etc..) */
-  std::string identify() const { return "QuantDSplit"; }
+  std::string identify() const override { return "QuantDSplit"; }
 };
 
 }
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 112530788..a138e4e21 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -43,11 +43,11 @@ class RelevantDomain : public QuantifiersUtil
   RelevantDomain(QuantifiersEngine* qe);
   virtual ~RelevantDomain();
   /** Reset. */
-  virtual bool reset(Theory::Effort e) override;
+  bool reset(Theory::Effort e) override;
   /** Register the quantified formula q */
-  virtual void registerQuantifier(Node q) override;
+  void registerQuantifier(Node q) override;
   /** identify */
-  virtual std::string identify() const override { return "RelevantDomain"; }
+  std::string identify() const override { return "RelevantDomain"; }
   /** Compute the relevant domain */
   void compute();
   /** Relevant domain representation.
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 2253ac1da..03cf0c996 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -50,13 +50,13 @@ private:
 public:
   RewriteEngine( context::Context* c, QuantifiersEngine* qe );
 
-  bool needsCheck( Theory::Effort e );
-  void check(Theory::Effort e, QEffort quant_e);
-  void registerQuantifier( Node f );
-  void assertNode( Node n );
-  bool checkCompleteFor( Node q );
+  bool needsCheck(Theory::Effort e) override;
+  void check(Theory::Effort e, QEffort quant_e) override;
+  void registerQuantifier(Node f) override;
+  void assertNode(Node n) override;
+  bool checkCompleteFor(Node q) override;
   /** Identify this module */
-  std::string identify() const { return "RewriteEngine"; }
+  std::string identify() const override { return "RewriteEngine"; }
 };
 
 }
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/ce_guided_instantiation.h
index 1b1d5e44b..e461a08d5 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.h
@@ -40,31 +40,31 @@ public:
   CegInstantiation( QuantifiersEngine * qe, context::Context* c );
   ~CegInstantiation();
 public:
-  bool needsCheck( Theory::Effort e );
-  QEffort needsModel(Theory::Effort e);
-  /* Call during quantifier engine's check */
-  void check(Theory::Effort e, QEffort quant_e);
-  /* Called for new quantifiers */
-  void registerQuantifier( Node q );
-  /** get the next decision request */
-  Node getNextDecisionRequest( unsigned& priority );
-  /** Identify this module (for debugging, dynamic configuration, etc..) */
-  std::string identify() const { return "CegInstantiation"; }
-  /** print solution for synthesis conjectures */
-  void printSynthSolution( std::ostream& out );
-  /** get synth solutions
-   *
-   * This function adds entries to sol_map that map functions-to-synthesize
-   * with their solutions, for all active conjectures (currently just the one
-   * assigned to d_conj). This should be called immediately after the solver
-   * answers unsat for sygus input.
-   *
-   * For details on what is added to sol_map, see
-   * CegConjecture::getSynthSolutions.
-   */
-  void getSynthSolutions(std::map<Node, Node>& sol_map);
-  /** preregister assertion (before rewrite) */
-  void preregisterAssertion( Node n );
+ bool needsCheck(Theory::Effort e) override;
+ QEffort needsModel(Theory::Effort e) override;
+ /* Call during quantifier engine's check */
+ void check(Theory::Effort e, QEffort quant_e) override;
+ /* Called for new quantifiers */
+ void registerQuantifier(Node q) override;
+ /** get the next decision request */
+ Node getNextDecisionRequest(unsigned& priority) override;
+ /** Identify this module (for debugging, dynamic configuration, etc..) */
+ std::string identify() const override { return "CegInstantiation"; }
+ /** print solution for synthesis conjectures */
+ void printSynthSolution(std::ostream& out);
+ /** get synth solutions
+  *
+  * This function adds entries to sol_map that map functions-to-synthesize
+  * with their solutions, for all active conjectures (currently just the one
+  * assigned to d_conj). This should be called immediately after the solver
+  * answers unsat for sygus input.
+  *
+  * For details on what is added to sol_map, see
+  * CegConjecture::getSynthSolutions.
+  */
+ void getSynthSolutions(std::map<Node, Node>& sol_map);
+ /** preregister assertion (before rewrite) */
+ void preregisterAssertion(Node n);
 public:
   class Statistics {
   public:
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index abdbef708..70ba2c283 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -37,9 +37,9 @@ public:
   CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){}
   virtual ~CegqiOutputSingleInv() {}
   CegConjectureSingleInv * d_out;
-  bool doAddInstantiation( std::vector< Node >& subs );
-  bool isEligibleForInstantiation( Node n );
-  bool addLemma( Node lem );
+  bool doAddInstantiation(std::vector<Node>& subs) override;
+  bool isEligibleForInstantiation(Node n) override;
+  bool addLemma(Node lem) override;
 };
 
 class DetTrace {
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h
index a43e38719..9e357f928 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.h
+++ b/src/theory/quantifiers/sygus/sygus_invariance.h
@@ -112,7 +112,7 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest
 
  protected:
   /** does d_conj{ d_var -> nvn } still rewrite to d_result? */
-  bool invariant(TermDbSygus* tds, Node nvn, Node x);
+  bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
 
  private:
   /** the formula we are evaluating */
@@ -170,7 +170,7 @@ class EquivSygusInvarianceTest : public SygusInvarianceTest
 
  protected:
   /** checks whether the analog of nvn still rewrites to d_bvr */
-  bool invariant(TermDbSygus* tds, Node nvn, Node x);
+  bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
 
  private:
   /** the conjecture associated with the enumerator d_enum */
@@ -202,7 +202,7 @@ class DivByZeroSygusInvarianceTest : public SygusInvarianceTest
 
  protected:
   /** checks whether nvn involves division by zero. */
-  bool invariant(TermDbSygus* tds, Node nvn, Node x);
+  bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
 };
 
 /** NegContainsSygusInvarianceTest
@@ -254,7 +254,7 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest
 
  protected:
   /** checks if contains( out_i, nvn[in_i] ) --> false for some I/O pair i. */
-  bool invariant(TermDbSygus* tds, Node nvn, Node x);
+  bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
 
  private:
   /** The enumerator whose value we are considering in this invariance test */
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 06576d6ce..eba1a87b1 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -176,7 +176,7 @@ class SygusSampler : public LazyTrieEvaluator
                       std::vector<Node>& vars,
                       std::vector<Node>& pt);
   /** evaluate n on sample point index */
-  Node evaluate(Node n, unsigned index);
+  Node evaluate(Node n, unsigned index) override;
   /**
    * Returns the index of a sample point such that the evaluation of a and b
    * diverge, or -1 if no such sample point exists.
@@ -367,7 +367,7 @@ class SygusSamplerExt : public SygusSampler
    * from the set of all previous input/output pairs based on the
    * d_drewrite utility.
    */
-  virtual Node registerTerm(Node n, bool forceKeep = false) override;
+  Node registerTerm(Node n, bool forceKeep = false) override;
 
  private:
   /** dynamic rewriter class */
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index de766cc2a..e440e68e9 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -141,11 +141,11 @@ class TermDb : public QuantifiersUtil {
   /** presolve (called once per user check-sat) */
   void presolve();
   /** reset (calculate which terms are active) */
-  virtual bool reset(Theory::Effort effort) override;
+  bool reset(Theory::Effort effort) override;
   /** register quantified formula */
-  virtual void registerQuantifier(Node q) override;
+  void registerQuantifier(Node q) override;
   /** identify */
-  virtual std::string identify() const override { return "TermDb"; }
+  std::string identify() const override { return "TermDb"; }
   /** get number of operators */
   unsigned getNumOperators();
   /** get operator at index i */
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 83d9d7940..bb02b1d6a 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -117,11 +117,11 @@ public:
   Node d_one;
 
   /** reset */
-  virtual bool reset(Theory::Effort e) override { return true; }
+  bool reset(Theory::Effort e) override { return true; }
   /** register quantifier */
-  virtual void registerQuantifier(Node q) override;
+  void registerQuantifier(Node q) override;
   /** identify */
-  virtual std::string identify() const override { return "TermUtil"; }
+  std::string identify() const override { return "TermUtil"; }
   // for inst constant
  private:
   /** map from universal quantifiers to the list of variables */
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 7468d2778..9f3134f84 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -135,7 +135,7 @@ class TheorySep : public Theory {
    public:
     NotifyClass(TheorySep& sep) : d_sep(sep) {}
 
-    bool eqNotifyTriggerEquality(TNode equality, bool value)
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override
     {
       Debug("sep::propagate")
           << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", "
@@ -151,7 +151,7 @@ class TheorySep : public Theory {
       }
     }
 
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value)
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
     {
       Unreachable();
     }
@@ -159,7 +159,7 @@ class TheorySep : public Theory {
     bool eqNotifyTriggerTermEquality(TheoryId tag,
                                      TNode t1,
                                      TNode t2,
-                                     bool value)
+                                     bool value) override
     {
       Debug("sep::propagate")
           << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2
@@ -176,23 +176,23 @@ class TheorySep : public Theory {
       return true;
     }
 
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2)
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
     {
       Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1
                               << ", " << t2 << ")" << std::endl;
       d_sep.conflict(t1, t2);
     }
 
-    void eqNotifyNewClass(TNode t) {}
-    void eqNotifyPreMerge(TNode t1, TNode t2)
+    void eqNotifyNewClass(TNode t) override {}
+    void eqNotifyPreMerge(TNode t1, TNode t2) override
     {
       d_sep.eqNotifyPreMerge(t1, t2);
     }
-    void eqNotifyPostMerge(TNode t1, TNode t2)
+    void eqNotifyPostMerge(TNode t1, TNode t2) override
     {
       d_sep.eqNotifyPostMerge(t1, t2);
     }
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {}
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
   };
 
   /** The notify class for d_equalityEngine */
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index bd63ff43d..b57f208bd 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -253,14 +253,17 @@ private:
 
   public:
     NotifyClass(TheorySetsPrivate& theory): d_theory(theory) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value);
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value);
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2);
-    void eqNotifyNewClass(TNode t);
-    void eqNotifyPreMerge(TNode t1, TNode t2);
-    void eqNotifyPostMerge(TNode t1, TNode t2);
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override;
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
+    bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override;
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
+    void eqNotifyNewClass(TNode t) override;
+    void eqNotifyPreMerge(TNode t1, TNode t2) override;
+    void eqNotifyPostMerge(TNode t1, TNode t2) override;
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
   } d_notify;
 
   /** Equality engine */
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 5ca625751..bc4db97ee 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -78,28 +78,35 @@ private:
     SharedTermsDatabase& d_sharedTerms;
   public:
     EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value) {
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override
+    {
       d_sharedTerms.propagateEquality(equality, value);
       return true;
     }
 
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+    {
       Unreachable();
       return true;
     }
 
-    bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) {
+    bool eqNotifyTriggerTermEquality(theory::TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override
+    {
       return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value);
     }
 
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
+    {
       d_sharedTerms.conflict(t1, t2, true);
     }
 
-    void eqNotifyNewClass(TNode t) { }
-    void eqNotifyPreMerge(TNode t1, TNode t2) { }
-    void eqNotifyPostMerge(TNode t1, TNode t2) { }
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+    void eqNotifyNewClass(TNode t) override {}
+    void eqNotifyPreMerge(TNode t1, TNode t2) override {}
+    void eqNotifyPostMerge(TNode t1, TNode t2) override {}
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
   };
 
   /** The notify class for d_equalityEngine */
@@ -245,9 +252,7 @@ protected:
   /**
    * This method gets called on backtracks from the context manager.
    */
-  void contextNotifyPop() {
-    backtrack();
-  }
+ void contextNotifyPop() override { backtrack(); }
 };
 
 }
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index e07cc6b5e..5dbbb93d6 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -81,7 +81,8 @@ class TheoryStrings : public Theory {
     TheoryStrings& d_str;
   public:
     NotifyClass(TheoryStrings& t_str): d_str(t_str) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value) {
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override
+    {
       Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
       if (value) {
         return d_str.propagate(equality);
@@ -90,7 +91,8 @@ class TheoryStrings : public Theory {
         return d_str.propagate(equality.notNode());
       }
     }
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+    {
       Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
       if (value) {
         return d_str.propagate(predicate);
@@ -98,7 +100,11 @@ class TheoryStrings : public Theory {
          return d_str.propagate(predicate.notNode());
       }
     }
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+    bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override
+    {
       Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
       if (value) {
       return d_str.propagate(t1.eqNode(t2));
@@ -106,23 +112,28 @@ class TheoryStrings : public Theory {
       return d_str.propagate(t1.eqNode(t2).notNode());
       }
     }
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
+    {
       Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
       d_str.conflict(t1, t2);
     }
-    void eqNotifyNewClass(TNode t) {
+    void eqNotifyNewClass(TNode t) override
+    {
       Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
       d_str.eqNotifyNewClass(t);
     }
-    void eqNotifyPreMerge(TNode t1, TNode t2) {
+    void eqNotifyPreMerge(TNode t1, TNode t2) override
+    {
       Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
       d_str.eqNotifyPreMerge(t1, t2);
     }
-    void eqNotifyPostMerge(TNode t1, TNode t2) {
+    void eqNotifyPostMerge(TNode t1, TNode t2) override
+    {
       Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
       d_str.eqNotifyPostMerge(t1, t2);
     }
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
+    {
       Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
       d_str.eqNotifyDisequal(t1, t2, reason);
     }
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index cca39a62e..2a2531887 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -76,9 +76,8 @@ private:
   class CacheInvalidator : public context::ContextNotifyObj {
     bool& d_cacheInvalidated;
   protected:
-    void contextNotifyPop() {
-      d_cacheInvalidated = true;
-    }
+   void contextNotifyPop() override { d_cacheInvalidated = true; }
+
   public:
     CacheInvalidator(context::Context* context, bool& cacheInvalidated) :
       context::ContextNotifyObj(context),
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7bc95b097..04e3c5697 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -157,14 +157,35 @@ class TheoryEngine {
     TheoryEngine& d_te;
   public:
     NotifyClass(TheoryEngine& te): d_te(te) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
-    bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {}
-    void eqNotifyNewClass(TNode t) { d_te.eqNotifyNewClass(t); }
-    void eqNotifyPreMerge(TNode t1, TNode t2) { d_te.eqNotifyPreMerge(t1, t2); }
-    void eqNotifyPostMerge(TNode t1, TNode t2) { d_te.eqNotifyPostMerge(t1, t2); }
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { d_te.eqNotifyDisequal(t1, t2, reason); }
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override
+    {
+      return true;
+    }
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+    {
+      return true;
+    }
+    bool eqNotifyTriggerTermEquality(theory::TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override
+    {
+      return true;
+    }
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
+    void eqNotifyNewClass(TNode t) override { d_te.eqNotifyNewClass(t); }
+    void eqNotifyPreMerge(TNode t1, TNode t2) override
+    {
+      d_te.eqNotifyPreMerge(t1, t2);
+    }
+    void eqNotifyPostMerge(TNode t1, TNode t2) override
+    {
+      d_te.eqNotifyPostMerge(t1, t2);
+    }
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
+    {
+      d_te.eqNotifyDisequal(t1, t2, reason);
+    }
   };/* class TheoryEngine::NotifyClass */
   NotifyClass d_masterEENotify;
 
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index bb74569b7..5b4a2d983 100644
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -67,7 +67,7 @@ class TheoryEngineModelBuilder : public ModelBuilder
    * builder in steps (2) or (5), for instance, if the model we
    * are building fails to satisfy a quantified formula.
    */
-  virtual bool buildModel(Model* m) override;
+  bool buildModel(Model* m) override;
   /** Debug check model.
    *
    * This throws an assertion failure if the model
diff --git a/src/theory/theory_registrar.h b/src/theory/theory_registrar.h
index df576a694..2514ccce0 100644
--- a/src/theory/theory_registrar.h
+++ b/src/theory/theory_registrar.h
@@ -37,9 +37,7 @@ public:
 
   TheoryRegistrar(TheoryEngine* te) : d_theoryEngine(te) { }
 
-  void preRegister(Node n) {
-    d_theoryEngine->preRegister(n);
-  }
+  void preRegister(Node n) override { d_theoryEngine->preRegister(n); }
 
 };/* class TheoryRegistrar */
 
diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h
index 7ca4a6140..736a65ade 100644
--- a/src/theory/type_enumerator.h
+++ b/src/theory/type_enumerator.h
@@ -84,7 +84,10 @@ public:
     TypeEnumeratorInterface(type) {
   }
 
-  TypeEnumeratorInterface* clone() const { return new T(static_cast<const T&>(*this)); }
+  TypeEnumeratorInterface* clone() const override
+  {
+    return new T(static_cast<const T&>(*this));
+  }
 
 };/* class TypeEnumeratorBase */
 
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index a89e55312..2d757cb28 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -131,14 +131,26 @@ public:
  */
 class EqualityEngineNotifyNone : public EqualityEngineNotify {
 public:
-  bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
-  bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
-  bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
-  void eqNotifyConstantTermMerge(TNode t1, TNode t2) { }
-  void eqNotifyNewClass(TNode t) { }
-  void eqNotifyPreMerge(TNode t1, TNode t2) { }
-  void eqNotifyPostMerge(TNode t1, TNode t2) { }
-  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override
+ {
+   return true;
+ }
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+ {
+   return true;
+ }
+ bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                  TNode t1,
+                                  TNode t2,
+                                  bool value) override
+ {
+   return true;
+ }
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
+ void eqNotifyNewClass(TNode t) override {}
+ void eqNotifyPreMerge(TNode t1, TNode t2) override {}
+ void eqNotifyPostMerge(TNode t1, TNode t2) override {}
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
 };/* class EqualityEngineNotifyNone */
 
 /**
@@ -538,9 +550,7 @@ private:
   /**
    * This method gets called on backtracks from the context manager.
    */
-  void contextNotifyPop() {
-    backtrack();
-  }
+  void contextNotifyPop() override { backtrack(); }
 
   /**
    * Constructor initialization stuff.
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 6fde4a9af..bac03c34c 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -55,7 +55,8 @@ public:
   public:
     NotifyClass(TheoryUF& uf): d_uf(uf) {}
 
-    bool eqNotifyTriggerEquality(TNode equality, bool value) {
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override
+    {
       Debug("uf") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
       if (value) {
         return d_uf.propagate(equality);
@@ -65,7 +66,8 @@ public:
       }
     }
 
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+    {
       Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
       if (value) {
         return d_uf.propagate(predicate);
@@ -74,7 +76,11 @@ public:
       }
     }
 
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+    bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override
+    {
       Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
       if (value) {
         return d_uf.propagate(t1.eqNode(t2));
@@ -83,27 +89,32 @@ public:
       }
     }
 
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
+    {
       Debug("uf-notify") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
       d_uf.conflict(t1, t2);
     }
 
-    void eqNotifyNewClass(TNode t) {
+    void eqNotifyNewClass(TNode t) override
+    {
       Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl;
       d_uf.eqNotifyNewClass(t);
     }
 
-    void eqNotifyPreMerge(TNode t1, TNode t2) {
+    void eqNotifyPreMerge(TNode t1, TNode t2) override
+    {
       Debug("uf-notify") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl;
       d_uf.eqNotifyPreMerge(t1, t2);
     }
 
-    void eqNotifyPostMerge(TNode t1, TNode t2) {
+    void eqNotifyPostMerge(TNode t1, TNode t2) override
+    {
       Debug("uf-notify") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl;
       d_uf.eqNotifyPostMerge(t1, t2);
     }
 
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
+    {
       Debug("uf-notify") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl;
       d_uf.eqNotifyDisequal(t1, t2, reason);
     }