Resolving warnings from -Winconsistent-missing-override on clang. (#1563)

16 files changed, 421 insertions, 363 deletions

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 1c10bde0d..4f3a13b4d 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -48,41 +48,47 @@ public:
   /**
    * Does non-context dependent setup for a node connected to a theory.
    */
-  void preRegisterTerm(TNode n);
+  void preRegisterTerm(TNode n) override;
 
-  Node expandDefinition(LogicRequest &logicRequest, Node node);
+  Node expandDefinition(LogicRequest& logicRequest, Node node) override;
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
-  void check(Effort e);
-  bool needsCheckLastEffort();
-  void propagate(Effort e);
-  Node explain(TNode n);
-  bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
-  bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp );
+  void check(Effort e) override;
+  bool needsCheckLastEffort() override;
+  void propagate(Effort e) override;
+  Node explain(TNode n) override;
+  bool getCurrentSubstitution(int effort,
+                              std::vector<Node>& vars,
+                              std::vector<Node>& subs,
+                              std::map<Node, std::vector<Node> >& exp) override;
+  bool isExtfReduced(int effort,
+                     Node n,
+                     Node on,
+                     std::vector<Node>& exp) override;
 
   bool collectModelInfo(TheoryModel* m) override;
 
-  void shutdown(){ }
+  void shutdown() override {}
 
-  void presolve();
-  void notifyRestart();
-  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
-  Node ppRewrite(TNode atom);
-  void ppStaticLearn(TNode in, NodeBuilder<>& learned);
+  void presolve() override;
+  void notifyRestart() override;
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
+  Node ppRewrite(TNode atom) override;
+  void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
 
-  std::string identify() const { return std::string("TheoryArith"); }
+  std::string identify() const override { return std::string("TheoryArith"); }
 
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 
-  void addSharedTerm(TNode n);
+  void addSharedTerm(TNode n) override;
 
-  Node getModelValue(TNode var);
+  Node getModelValue(TNode var) override;
 
-
-  std::pair<bool, Node> entailmentCheck(TNode lit,
-                                        const EntailmentCheckParameters* params,
-                                        EntailmentCheckSideEffects* out);
+  std::pair<bool, Node> entailmentCheck(
+      TNode lit,
+      const EntailmentCheckParameters* params,
+      EntailmentCheckSideEffects* out) override;
 
 };/* class TheoryArith */
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 24c286e92..caf466c0c 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -143,9 +143,9 @@ class TheoryArrays : public Theory {
                std::string name = "");
   ~TheoryArrays();
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
-  std::string identify() const { return std::string("TheoryArrays"); }
+  std::string identify() const override { return std::string("TheoryArrays"); }
 
   /////////////////////////////////////////////////////////////////////////////
   // PREPROCESSING
@@ -174,17 +174,15 @@ class TheoryArrays : public Theory {
   bool ppDisequal(TNode a, TNode b);
   Node solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck);
 
-  public:
-
-  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
-  Node ppRewrite(TNode atom);
+ public:
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
+  Node ppRewrite(TNode atom) override;
 
   /////////////////////////////////////////////////////////////////////////////
   // T-PROPAGATION / REGISTRATION
   /////////////////////////////////////////////////////////////////////////////
 
-  private:
-
+ private:
   /** Literals to propagate */
   context::CDList<Node> d_literalsToPropagate;
 
@@ -204,19 +202,17 @@ class TheoryArrays : public Theory {
   /** Helper for preRegisterTerm, also used internally */
   void preRegisterTermInternal(TNode n);
 
-  public:
-
-  void preRegisterTerm(TNode n);
-  void propagate(Effort e);
+ public:
+  void preRegisterTerm(TNode n) override;
+  void propagate(Effort e) override;
   Node explain(TNode n, eq::EqProof* proof);
-  Node explain(TNode n);
+  Node explain(TNode n) override;
 
   /////////////////////////////////////////////////////////////////////////////
   // SHARING
   /////////////////////////////////////////////////////////////////////////////
 
-  private:
-
+ private:
   class MayEqualNotifyClass {
   public:
     bool notify(TNode propagation) { return true; }
@@ -232,46 +228,40 @@ class TheoryArrays : public Theory {
   // Helper for computeCareGraph
   void checkPair(TNode r1, TNode r2);
 
-  public:
-
-  void addSharedTerm(TNode t);
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
-  void computeCareGraph();
+ public:
+  void addSharedTerm(TNode t) override;
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+  void computeCareGraph() override;
   bool isShared(TNode t)
-    { return (d_sharedArrays.find(t) != d_sharedArrays.end()); }
-
+  {
+    return (d_sharedArrays.find(t) != d_sharedArrays.end());
+  }
 
   /////////////////////////////////////////////////////////////////////////////
   // MODEL GENERATION
   /////////////////////////////////////////////////////////////////////////////
 
-  private:
-
-  public:
-   bool collectModelInfo(TheoryModel* m) override;
-
-   /////////////////////////////////////////////////////////////////////////////
-   // NOTIFICATIONS
-   /////////////////////////////////////////////////////////////////////////////
+ public:
+  bool collectModelInfo(TheoryModel* m) override;
 
-  private:
-  public:
+  /////////////////////////////////////////////////////////////////////////////
+  // NOTIFICATIONS
+  /////////////////////////////////////////////////////////////////////////////
 
-  Node getNextDecisionRequest( unsigned& priority );
+ public:
+  Node getNextDecisionRequest(unsigned& priority) override;
 
-  void presolve();
-  void shutdown() { }
+  void presolve() override;
+  void shutdown() override {}
 
   /////////////////////////////////////////////////////////////////////////////
   // MAIN SOLVER
   /////////////////////////////////////////////////////////////////////////////
 
-  public:
-
-  void check(Effort e);
-
-  private:
+ public:
+  void check(Effort e) override;
 
+ private:
   TNode weakEquivGetRep(TNode node);
   TNode weakEquivGetRepIndex(TNode node, TNode index);
   void visitAllLeaves(TNode reason, std::vector<TNode>& conjunctions);
@@ -454,11 +444,8 @@ class TheoryArrays : public Theory {
   /** An equality-engine callback for proof reconstruction */
   ArrayProofReconstruction d_proofReconstruction;
 
-  public:
-
-  eq::EqualityEngine* getEqualityEngine() {
-    return &d_equalityEngine;
-  }
+ public:
+  eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
 
 };/* class TheoryArrays */
 
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 8cefe03b2..1992c0ae3 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -64,40 +64,43 @@ public:
 
   ~TheoryBV();
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
-  Node expandDefinition(LogicRequest &logicRequest, Node node);
+  Node expandDefinition(LogicRequest& logicRequest, Node node) override;
 
   void mkAckermanizationAssertions(std::vector<Node>& assertions);
 
-  void preRegisterTerm(TNode n);
+  void preRegisterTerm(TNode n) override;
 
-  void check(Effort e);
-  
-  bool needsCheckLastEffort();
+  void check(Effort e) override;
+
+  bool needsCheckLastEffort() override;
 
-  void propagate(Effort e);
+  void propagate(Effort e) override;
 
-  Node explain(TNode n);
+  Node explain(TNode n) override;
 
   bool collectModelInfo(TheoryModel* m) override;
 
-  std::string identify() const { return std::string("TheoryBV"); }
+  std::string identify() const override { return std::string("TheoryBV"); }
 
   /** equality engine */
-  eq::EqualityEngine * getEqualityEngine();
-  bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
-  int getReduction( int effort, Node n, Node& nr );
-  
-  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+  eq::EqualityEngine* getEqualityEngine() override;
+  bool getCurrentSubstitution(int effort,
+                              std::vector<Node>& vars,
+                              std::vector<Node>& subs,
+                              std::map<Node, std::vector<Node> >& exp) override;
+  int getReduction(int effort, Node n, Node& nr) override;
+
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 
   void enableCoreTheorySlicer();
 
-  Node ppRewrite(TNode t);
+  Node ppRewrite(TNode t) override;
 
-  void ppStaticLearn(TNode in, NodeBuilder<>& learned);
+  void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
 
-  void presolve();
+  void presolve() override;
 
   bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
 
@@ -206,13 +209,13 @@ private:
    */
   void explain(TNode literal, std::vector<TNode>& assumptions);
 
-  void addSharedTerm(TNode t);
+  void addSharedTerm(TNode t) override;
 
   bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
 
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 
-  Node getModelValue(TNode var);
+  Node getModelValue(TNode var) override;
 
   inline std::string indent()
   {
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index a3001d042..8052df59a 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -220,21 +220,21 @@ private:
   /** get eqc constructor */
   TNode getEqcConstructor( TNode r );
 
-protected:
+ protected:
   void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs );
   /** compute care graph */
-  void computeCareGraph();
+  void computeCareGraph() override;
 
-public:
+ public:
   TheoryDatatypes(context::Context* c, context::UserContext* u,
                   OutputChannel& out, Valuation valuation,
                   const LogicInfo& logicInfo);
   ~TheoryDatatypes();
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
   /** propagate */
-  void propagate(Effort effort);
+  void propagate(Effort effort) override;
   /** propagate */
   bool propagate(TNode literal);
   /** explain */
@@ -242,7 +242,7 @@ public:
   void explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions );
   void explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions );
   void explain( TNode literal, std::vector<TNode>& assumptions );
-  Node explain( TNode literal );
+  Node explain(TNode literal) override;
   Node explain( std::vector< Node >& lits );
   /** Conflict when merging two constants */
   void conflict(TNode a, TNode b);
@@ -255,26 +255,36 @@ public:
   /** called when two equivalence classes are made disequal */
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 
-  void check(Effort e);
-  bool needsCheckLastEffort();
-  void preRegisterTerm(TNode n);
-  void finishInit();
-  Node expandDefinition(LogicRequest &logicRequest, Node n);
-  Node ppRewrite(TNode n);
-  void presolve();
-  void addSharedTerm(TNode t);
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
+  void check(Effort e) override;
+  bool needsCheckLastEffort() override;
+  void preRegisterTerm(TNode n) override;
+  void finishInit() override;
+  Node expandDefinition(LogicRequest& logicRequest, Node n) override;
+  Node ppRewrite(TNode n) override;
+  void presolve() override;
+  void addSharedTerm(TNode t) override;
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   bool collectModelInfo(TheoryModel* m) override;
-  void shutdown() { }
-  std::string identify() const { return std::string("TheoryDatatypes"); }
+  void shutdown() override {}
+  std::string identify() const override
+  {
+    return std::string("TheoryDatatypes");
+  }
   /** equality engine */
-  eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; }
-  bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
+  eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
+  bool getCurrentSubstitution(int effort,
+                              std::vector<Node>& vars,
+                              std::vector<Node>& subs,
+                              std::map<Node, std::vector<Node> >& exp) override;
   /** debug print */
   void printModelDebug( const char* c );
   /** entailment check */
-  virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL);
-private:
+  std::pair<bool, Node> entailmentCheck(
+      TNode lit,
+      const EntailmentCheckParameters* params = NULL,
+      EntailmentCheckSideEffects* out = NULL) override;
+
+ private:
   /** add tester to equivalence class info */
   void addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg );
   /** add selector to equivalence class info */
@@ -325,7 +335,7 @@ private:
  SygusSymBreakNew* d_sygus_sym_break;
 
 public:
-  Node getNextDecisionRequest( unsigned& priority );
+ Node getNextDecisionRequest(unsigned& priority) override;
 };/* class TheoryDatatypes */
 
 }/* CVC4::theory::datatypes namespace */
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 614cbff46..ca80546b8 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -38,21 +38,21 @@ class TheoryFp : public Theory {
   TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out,
            Valuation valuation, const LogicInfo& logicInfo);
 
-  Node expandDefinition(LogicRequest& lr, Node node);
+  Node expandDefinition(LogicRequest& lr, Node node) override;
 
-  void preRegisterTerm(TNode node);
-  void addSharedTerm(TNode node);
+  void preRegisterTerm(TNode node) override;
+  void addSharedTerm(TNode node) override;
 
-  void check(Effort);
+  void check(Effort) override;
 
-  Node getModelValue(TNode var);
+  Node getModelValue(TNode var) override;
   bool collectModelInfo(TheoryModel* m) override;
 
-  std::string identify() const { return "THEORY_FP"; }
+  std::string identify() const override { return "THEORY_FP"; }
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
-  Node explain(TNode n);
+  Node explain(TNode n) override;
 
  protected:
   /** Equality engine */
diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
index a607909cc..95295d214 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -187,43 +187,44 @@ class EprInstantiator : public Instantiator {
 class BvInstantiator : public Instantiator {
  public:
   BvInstantiator(QuantifiersEngine* qe, TypeNode tn);
-  virtual ~BvInstantiator();
-  virtual void reset(CegInstantiator* ci,
-                     SolvedForm& sf,
-                     Node pv,
-                     CegInstEffort effort) override;
-  virtual bool hasProcessAssertion(CegInstantiator* ci,
-                                   SolvedForm& sf,
-                                   Node pv,
-                                   CegInstEffort effort) override
+  ~BvInstantiator() override;
+  void reset(CegInstantiator* ci,
+             SolvedForm& sf,
+             Node pv,
+             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;
+  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;
   /** use model value
    *
    * We allow model values if we have not already tried an assertion,
    * and only at levels below full if cbqiFullEffort is false.
    */
-  virtual bool useModelValue(CegInstantiator* ci,
-                             SolvedForm& sf,
-                             Node pv,
-                             CegInstEffort effort) override;
-  virtual std::string identify() const { return "Bv"; }
+  bool useModelValue(CegInstantiator* ci,
+                     SolvedForm& sf,
+                     Node pv,
+                     CegInstEffort effort) override;
+  std::string identify() const override { return "Bv"; }
+
  private:
   // point to the bv inverter class
   BvInverter * d_inverter;
@@ -281,7 +282,7 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess
 {
  public:
   BvInstantiatorPreprocess() {}
-  virtual ~BvInstantiatorPreprocess() {}
+  ~BvInstantiatorPreprocess() override {}
   /** register counterexample lemma
    *
    * This method modifies the contents of lems based on the extract terms
@@ -308,8 +309,8 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess
    * since the added equalities ensure we are able to construct the proper
    * solved forms for variables in t and for the intermediate variables above.
    */
-  virtual void registerCounterexampleLemma(std::vector<Node>& lems,
-                                           std::vector<Node>& ce_vars) override;
+  void registerCounterexampleLemma(std::vector<Node>& lems,
+                                   std::vector<Node>& ce_vars) override;
 
  private:
   /** collect extracts
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 0c4b6b7a4..f33151b4d 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -248,19 +248,21 @@ class Def;
 class FirstOrderModelFmc : public FirstOrderModel
 {
   friend class FullModelChecker;
-private:
+
+ private:
   /** models for UF */
   std::map<Node, Def * > d_models;
   std::map<TypeNode, Node > d_type_star;
   Node intervalOp;
   /** get current model value */
-  void processInitializeModelForTerm(Node n);
-public:
+  void processInitializeModelForTerm(Node n) override;
+
+ public:
   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
   ~FirstOrderModelFmc() override;
-  FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
+  FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; }
   // initialize the model
-  void processInitialize( bool ispre );
+  void processInitialize(bool ispre) override;
   Node getFunctionValue(Node op, const char* argPrefix );
 
   bool isStar(Node n);
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index fc913c7cf..1903a0f95 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -222,7 +222,7 @@ class InstMatchGenerator : public IMGenerator {
    *
    * See Trigger::getActiveScore for details.
    */
-  int getActiveScore(QuantifiersEngine* qe);
+  int getActiveScore(QuantifiersEngine* qe) override;
   /** exclude match
    *
    * Exclude matching d_match_pattern with Node n on subsequent calls to
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index c2520a973..26591c678 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -129,18 +129,19 @@ public:
 };
 
 class InstStrategyCegqi : public InstStrategyCbqi {
-protected:
+ protected:
   CegqiOutputInstStrategy * d_out;
   std::map< Node, CegInstantiator * > d_cinst;
   Node d_small_const;
   Node d_curr_quant;
   bool d_check_vts_lemma_lc;
   /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  void process( Node f, Theory::Effort effort, int e );
+  void processResetInstantiationRound(Theory::Effort effort) override;
+  void process(Node f, Theory::Effort effort, int e) override;
   /** register ce lemma */
-  void registerCounterexampleLemma( Node q, Node lem );
-public:
+  void registerCounterexampleLemma(Node q, Node lem) override;
+
+ public:
   InstStrategyCegqi( QuantifiersEngine * qe );
   ~InstStrategyCegqi() override;
 
@@ -148,14 +149,14 @@ public:
   bool isEligibleForInstantiation( Node n );
   bool addLemma( Node lem );
   /** identify */
-  std::string identify() const { return std::string("Cegqi"); }
+  std::string identify() const override { return std::string("Cegqi"); }
 
   //get instantiator for quantifier
   CegInstantiator * getInstantiator( Node q );
   //register quantifier
-  void registerQuantifier( Node q );
+  void registerQuantifier(Node q) override;
   //presolve
-  void presolve();
+  void presolve() override;
 };
 
 }
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 511aebf3b..4eb592b3e 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -178,7 +178,7 @@ class QModelBuilderDefault : public QModelBuilderIG
   //do InstGen techniques for quantifier, return number of lemmas produced
   int doInstGen(FirstOrderModel* fm, Node f) override;
   //theory-specific build models
-  void constructModelUf( FirstOrderModel* fm, Node op );
+  void constructModelUf(FirstOrderModel* fm, Node op) override;
 
  protected:
   std::map< Node, QuantPhaseReq > d_phase_reqs;
@@ -189,7 +189,10 @@ class QModelBuilderDefault : public QModelBuilderIG
   //options
   bool optReconsiderFuncConstants() { return true; }
   //has inst gen
-  bool hasInstGen( Node f ) { return !d_quant_selection_lit[f].isNull(); }
+  bool hasInstGen(Node f) override
+  {
+    return !d_quant_selection_lit[f].isNull();
+  }
 };
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 295a39464..4f87f6aae 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -33,37 +33,47 @@ namespace theory {
 namespace quantifiers {
 
 class TheoryQuantifiers : public Theory {
-private:
-  typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-  /** number of instantiations */
-  int d_numInstantiations;
-  int d_baseDecLevel;
-private:
-  void computeCareGraph();
-
-public:
+ public:
   TheoryQuantifiers(context::Context* c, context::UserContext* u,
                     OutputChannel& out, Valuation valuation,
                     const LogicInfo& logicInfo);
   ~TheoryQuantifiers();
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
-  void addSharedTerm(TNode t);
+  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+  void addSharedTerm(TNode t) override;
   void notifyEq(TNode lhs, TNode rhs);
-  void preRegisterTerm(TNode n);
-  void presolve();
-  void ppNotifyAssertions(const std::vector<Node>& assertions);
-  void check(Effort e);
-  Node getNextDecisionRequest( unsigned& priority );
+  void preRegisterTerm(TNode n) override;
+  void presolve() override;
+  void ppNotifyAssertions(const std::vector<Node>& assertions) override;
+  void check(Effort e) override;
+  Node getNextDecisionRequest(unsigned& priority) override;
   Node getValue(TNode n);
   bool collectModelInfo(TheoryModel* m) override;
-  void shutdown() { }
-  std::string identify() const { return std::string("TheoryQuantifiers"); }
-  void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value);
-  bool ppDontRewriteSubterm(TNode atom) { return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; }
-private:
+  void shutdown() override {}
+  std::string identify() const override
+  {
+    return std::string("TheoryQuantifiers");
+  }
+  void setUserAttribute(const std::string& attr,
+                        Node n,
+                        std::vector<Node> node_values,
+                        std::string str_value) override;
+  bool ppDontRewriteSubterm(TNode atom) override
+  {
+    return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS;
+  }
+
+ private:
   void assertUniversal( Node n );
   void assertExistential( Node n );
+  void computeCareGraph() override;
+
+  using BoolMap = context::CDHashMap<Node, bool, NodeHashFunction>;
+
+  /** number of instantiations */
+  int d_numInstantiations;
+  int d_baseDecLevel;
+
 };/* class TheoryQuantifiers */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 65f076631..7468d2778 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -43,7 +43,7 @@ class TheorySep : public Theory {
   // MISC
   /////////////////////////////////////////////////////////////////////////////
 
-  private:
+ private:
   /** all lemmas sent */
   NodeSet d_lemmas_produced_c;
 
@@ -62,119 +62,137 @@ class TheorySep : public Theory {
                         std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict,
                         bool pol, bool hasPol, bool underSpatial );
 
-  public:
-
+ public:
   TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
   ~TheorySep();
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
-  std::string identify() const { return std::string("TheorySep"); }
+  std::string identify() const override { return std::string("TheorySep"); }
 
   /////////////////////////////////////////////////////////////////////////////
   // PREPROCESSING
   /////////////////////////////////////////////////////////////////////////////
 
-  public:
-
-  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
-  Node ppRewrite(TNode atom);
+ public:
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
+  Node ppRewrite(TNode atom) override;
 
-  void ppNotifyAssertions(const std::vector<Node>& assertions);
+  void ppNotifyAssertions(const std::vector<Node>& assertions) override;
   /////////////////////////////////////////////////////////////////////////////
   // T-PROPAGATION / REGISTRATION
   /////////////////////////////////////////////////////////////////////////////
 
-  private:
-
+ private:
   /** Should be called to propagate the literal.  */
   bool propagate(TNode literal);
 
   /** Explain why this literal is true by adding assumptions */
   void explain(TNode literal, std::vector<TNode>& assumptions);
 
-  public:
+ public:
+  void propagate(Effort e) override;
+  Node explain(TNode n) override;
 
-  void propagate(Effort e);
-  Node explain(TNode n);
-
-  public:
-
-  void addSharedTerm(TNode t);
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
-  void computeCareGraph();
+ public:
+  void addSharedTerm(TNode t) override;
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+  void computeCareGraph() override;
 
   /////////////////////////////////////////////////////////////////////////////
   // MODEL GENERATION
   /////////////////////////////////////////////////////////////////////////////
 
-  public:
-   bool collectModelInfo(TheoryModel* m) override;
-   void postProcessModel(TheoryModel* m);
-
-   /////////////////////////////////////////////////////////////////////////////
-   // NOTIFICATIONS
-   /////////////////////////////////////////////////////////////////////////////
+ public:
+  bool collectModelInfo(TheoryModel* m) override;
+  void postProcessModel(TheoryModel* m) override;
 
-  private:
-  public:
+  /////////////////////////////////////////////////////////////////////////////
+  // NOTIFICATIONS
+  /////////////////////////////////////////////////////////////////////////////
 
-  Node getNextDecisionRequest( unsigned& priority );
+ public:
+  Node getNextDecisionRequest(unsigned& priority) override;
 
-  void presolve();
-  void shutdown() { }
+  void presolve() override;
+  void shutdown() override {}
 
   /////////////////////////////////////////////////////////////////////////////
   // MAIN SOLVER
   /////////////////////////////////////////////////////////////////////////////
-  public:
-
-  void check(Effort e);
+ public:
+  void check(Effort e) override;
 
-  bool needsCheckLastEffort();
+  bool needsCheckLastEffort() override;
 
-  private:
-
-  // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
-  class NotifyClass : public eq::EqualityEngineNotify {
+ private:
+  // NotifyClass: template helper class for d_equalityEngine - handles
+  // call-back from congruence closure module
+  class NotifyClass : public eq::EqualityEngineNotify
+  {
     TheorySep& d_sep;
-  public:
-    NotifyClass(TheorySep& sep): d_sep(sep) {}
 
-    bool eqNotifyTriggerEquality(TNode equality, bool value) {
-      Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
+   public:
+    NotifyClass(TheorySep& sep) : d_sep(sep) {}
+
+    bool eqNotifyTriggerEquality(TNode equality, bool value)
+    {
+      Debug("sep::propagate")
+          << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", "
+          << (value ? "true" : "false") << ")" << std::endl;
       // Just forward to sep
-      if (value) {
+      if (value)
+      {
         return d_sep.propagate(equality);
-      } else {
+      }
+      else
+      {
         return d_sep.propagate(equality.notNode());
       }
     }
 
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value)
+    {
       Unreachable();
     }
 
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
-      Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
-      if (value) {
+    bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value)
+    {
+      Debug("sep::propagate")
+          << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2
+          << ", " << (value ? "true" : "false") << ")" << std::endl;
+      if (value)
+      {
         // Propagate equality between shared terms
         return d_sep.propagate(t1.eqNode(t2));
-      } else {
+      }
+      else
+      {
         return d_sep.propagate(t1.eqNode(t2).notNode());
       }
       return true;
     }
 
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-      Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2)
+    {
+      Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1
+                              << ", " << t2 << ")" << std::endl;
       d_sep.conflict(t1, t2);
     }
 
-    void eqNotifyNewClass(TNode t) { }
-    void eqNotifyPreMerge(TNode t1, TNode t2) { d_sep.eqNotifyPreMerge( t1, t2 ); }
-    void eqNotifyPostMerge(TNode t1, TNode t2) { d_sep.eqNotifyPostMerge( t1, t2 ); }
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+    void eqNotifyNewClass(TNode t) {}
+    void eqNotifyPreMerge(TNode t1, TNode t2)
+    {
+      d_sep.eqNotifyPreMerge(t1, t2);
+    }
+    void eqNotifyPostMerge(TNode t1, TNode t2)
+    {
+      d_sep.eqNotifyPostMerge(t1, t2);
+    }
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {}
   };
 
   /** The notify class for d_equalityEngine */
@@ -289,7 +307,8 @@ class TheorySep : public Theory {
   void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active );
 
   Node mkUnion( TypeNode tn, std::vector< Node >& locs );
-private:
+
+ private:
   Node getRepresentative( Node t );
   bool hasTerm( Node a );
   bool areEqual( Node a, Node b );
@@ -299,10 +318,9 @@ private:
 
   void sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer = false );
   void doPendingFacts();
-public:
-  eq::EqualityEngine* getEqualityEngine() {
-    return &d_equalityEngine;
-  }
+
+ public:
+  eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
 
   void initializeBounds();
 };/* class TheorySep */
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 1f0fbdd1f..a246903a1 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -46,36 +46,36 @@ public:
 
   ~TheorySets();
 
-  void addSharedTerm(TNode);
+  void addSharedTerm(TNode) override;
 
-  void check(Effort);
-  
-  bool needsCheckLastEffort();
+  void check(Effort) override;
+
+  bool needsCheckLastEffort() override;
 
   bool collectModelInfo(TheoryModel* m) override;
 
-  void computeCareGraph();
+  void computeCareGraph() override;
+
+  Node explain(TNode) override;
 
-  Node explain(TNode);
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
+  Node getModelValue(TNode) override;
 
-  Node getModelValue(TNode);
+  std::string identify() const override { return "THEORY_SETS"; }
 
-  std::string identify() const { return "THEORY_SETS"; }
+  void preRegisterTerm(TNode node) override;
 
-  void preRegisterTerm(TNode node);
+  Node expandDefinition(LogicRequest& logicRequest, Node n) override;
 
-  Node expandDefinition(LogicRequest &logicRequest, Node n);
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 
-  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+  void presolve() override;
 
-  void presolve();
+  void propagate(Effort) override;
 
-  void propagate(Effort);
+  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
-  
   bool isEntailed( Node n, bool pol );
 
 };/* class TheorySets */
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index f07057444..e07cc6b5e 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -54,25 +54,28 @@ class TheoryStrings : public Theory {
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
-public:
+ public:
   TheoryStrings(context::Context* c, context::UserContext* u,
                 OutputChannel& out, Valuation valuation,
                 const LogicInfo& logicInfo);
   ~TheoryStrings();
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
-  std::string identify() const { return std::string("TheoryStrings"); }
+  std::string identify() const override { return std::string("TheoryStrings"); }
 
-public:
-  void propagate(Effort e);
+ public:
+  void propagate(Effort e) override;
   bool propagate(TNode literal);
   void explain( TNode literal, std::vector<TNode>& assumptions );
-  Node explain( TNode literal );
-  eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; }
-  bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
-  int getReduction( int effort, Node n, Node& nr );
- 
+  Node explain(TNode literal) override;
+  eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
+  bool getCurrentSubstitution(int effort,
+                              std::vector<Node>& vars,
+                              std::vector<Node>& subs,
+                              std::map<Node, std::vector<Node> >& exp) override;
+  int getReduction(int effort, Node n, Node& nr) override;
+
   // NotifyClass for equality engine
   class NotifyClass : public eq::EqualityEngineNotify {
     TheoryStrings& d_str;
@@ -213,24 +216,24 @@ private:
   /////////////////////////////////////////////////////////////////////////////
   // MODEL GENERATION
   /////////////////////////////////////////////////////////////////////////////
-public:
- bool collectModelInfo(TheoryModel* m) override;
+ public:
+  bool collectModelInfo(TheoryModel* m) override;
 
- /////////////////////////////////////////////////////////////////////////////
- // NOTIFICATIONS
- /////////////////////////////////////////////////////////////////////////////
-public:
-  void presolve();
-  void shutdown() { }
+  /////////////////////////////////////////////////////////////////////////////
+  // NOTIFICATIONS
+  /////////////////////////////////////////////////////////////////////////////
+ public:
+  void presolve() override;
+  void shutdown() override {}
 
   /////////////////////////////////////////////////////////////////////////////
   // MAIN SOLVER
   /////////////////////////////////////////////////////////////////////////////
-private:
-  void addSharedTerm(TNode n);
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
+ private:
+  void addSharedTerm(TNode n) override;
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 
-private:
+ private:
   class EqcInfo {
   public:
     EqcInfo( context::Context* c );
@@ -367,17 +370,18 @@ private:
   //cardinality check
   void checkCardinality();
 
-private:
+ private:
   void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
-public:
+
+ public:
   /** preregister term */
-  void preRegisterTerm(TNode n);
+  void preRegisterTerm(TNode n) override;
   /** Expand definition */
-  Node expandDefinition(LogicRequest &logicRequest, Node n);
+  Node expandDefinition(LogicRequest& logicRequest, Node n) override;
   /** Check at effort e */
-  void check(Effort e);
+  void check(Effort e) override;
   /** needs check last effort */
-  bool needsCheckLastEffort();
+  bool needsCheckLastEffort() override;
   /** Conflict when merging two constants */
   void conflict(TNode a, TNode b);
   /** called when a new equivalence class is created */
@@ -389,39 +393,48 @@ public:
   /** called when two equivalence classes are made disequal */
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
   /** get preprocess */
-  StringsPreprocess * getPreprocess() { return &d_preproc; }
-protected:
+  StringsPreprocess* getPreprocess() { return &d_preproc; }
+
+ protected:
   /** compute care graph */
-  void computeCareGraph();
+  void computeCareGraph() override;
 
-  //do pending merges
+  // do pending merges
   void assertPendingFact(Node atom, bool polarity, Node exp);
   void doPendingFacts();
   void doPendingLemmas();
   bool hasProcessed();
-  void addToExplanation( Node a, Node b, std::vector< Node >& exp );
-  void addToExplanation( Node lit, std::vector< Node >& exp );
-
-  //register term
-  void registerTerm( Node n, int effort );
-  //send lemma
-  void sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma = false );
-  void sendInference( std::vector< Node >& exp, Node eq, const char * c, bool asLemma = false );
-  void sendLemma( Node ant, Node conc, const char * c );
-  void sendInfer( Node eq_exp, Node eq, const char * c );
+  void addToExplanation(Node a, Node b, std::vector<Node>& exp);
+  void addToExplanation(Node lit, std::vector<Node>& exp);
+
+  // register term
+  void registerTerm(Node n, int effort);
+  // send lemma
+  void sendInference(std::vector<Node>& exp,
+                     std::vector<Node>& exp_n,
+                     Node eq,
+                     const char* c,
+                     bool asLemma = false);
+  void sendInference(std::vector<Node>& exp,
+                     Node eq,
+                     const char* c,
+                     bool asLemma = false);
+  void sendLemma(Node ant, Node conc, const char* c);
+  void sendInfer(Node eq_exp, Node eq, const char* c);
   bool sendSplit(Node a, Node b, const char* c, bool preq = true);
-  void sendLengthLemma( Node n );
+  void sendLengthLemma(Node n);
   /** mkConcat **/
-  inline Node mkConcat( Node n1, Node n2 );
-  inline Node mkConcat( Node n1, Node n2, Node n3 );
-  inline Node mkConcat( const std::vector< Node >& c );
-  inline Node mkLength( Node n );
-  //mkSkolem
-  enum {
+  inline Node mkConcat(Node n1, Node n2);
+  inline Node mkConcat(Node n1, Node n2, Node n3);
+  inline Node mkConcat(const std::vector<Node>& c);
+  inline Node mkLength(Node n);
+  // mkSkolem
+  enum
+  {
     sk_id_c_spt,
     sk_id_vc_spt,
     sk_id_vc_bin_spt,
-    sk_id_v_spt,    
+    sk_id_v_spt,
     sk_id_c_spt_rev,
     sk_id_vc_spt_rev,
     sk_id_vc_bin_spt_rev,
@@ -434,30 +447,36 @@ protected:
     sk_id_deq_y,
     sk_id_deq_z,
   };
-  std::map< Node, std::map< Node, std::map< int, Node > > > d_skolem_cache;
-  Node mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit = 0 );
-  inline Node mkSkolemS(const char * c, int isLenSplit = 0);
-  void registerNonEmptySkolem( Node sk );
-  //inline Node mkSkolemI(const char * c);
+  std::map<Node, std::map<Node, std::map<int, Node> > > d_skolem_cache;
+  Node mkSkolemCached(
+      Node a, Node b, int id, const char* c, int isLenSplit = 0);
+  inline Node mkSkolemS(const char* c, int isLenSplit = 0);
+  void registerNonEmptySkolem(Node sk);
+  // inline Node mkSkolemI(const char * c);
   /** mkExplain **/
-  Node mkExplain( std::vector< Node >& a );
-  Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
+  Node mkExplain(std::vector<Node>& a);
+  Node mkExplain(std::vector<Node>& a, std::vector<Node>& an);
   /** mkAnd **/
-  Node mkAnd( std::vector< Node >& a );
+  Node mkAnd(std::vector<Node>& a);
   /** get concat vector */
-  void getConcatVec( Node n, std::vector< Node >& c );
+  void getConcatVec(Node n, std::vector<Node>& c);
 
-  //get equivalence classes
-  void getEquivalenceClasses( std::vector< Node >& eqcs );
+  // get equivalence classes
+  void getEquivalenceClasses(std::vector<Node>& eqcs);
 
-  //separate into collections with equal length
-  void separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
-  void printConcat( std::vector< Node >& n, const char * c );
+  // separate into collections with equal length
+  void separateByLength(std::vector<Node>& n,
+                        std::vector<std::vector<Node> >& col,
+                        std::vector<Node>& lts);
+  void printConcat(std::vector<Node>& n, const char* c);
 
-  void inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc );
+  void inferSubstitutionProxyVars(Node n,
+                                  std::vector<Node>& vars,
+                                  std::vector<Node>& subs,
+                                  std::vector<Node>& unproc);
 
   // Symbolic Regular Expression
-private:
+ private:
   // regular expression memberships
   NodeList d_regexp_memberships;
   NodeSet d_regexp_ucached;
@@ -492,18 +511,20 @@ private:
 
 
   // Finite Model Finding
-private:
+ private:
   NodeSet d_input_vars;
   context::CDO< Node > d_input_var_lsum;
   context::CDHashMap< int, Node > d_cardinality_lits;
   context::CDO< int > d_curr_cardinality;
-public:
+
+ public:
   //for finite model finding
-  Node getNextDecisionRequest( unsigned& priority );
-  //ppRewrite
-  Node ppRewrite(TNode atom);
-public:
-/** statistics class */
+  Node getNextDecisionRequest(unsigned& priority) override;
+  // ppRewrite
+  Node ppRewrite(TNode atom) override;
+
+ public:
+  /** statistics class */
   class Statistics {
   public:
     IntStat d_splits;
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 934a09a8e..1f9fd92d4 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -162,13 +162,13 @@ public:
    */
   Node getValue(TNode n, bool useDontCares = false) const;
   /** get comments */
-  void getComments(std::ostream& out) const;
+  void getComments(std::ostream& out) const override;
 
   //---------------------------- separation logic
   /** set the heap and value sep.nil is equal to */
   void setHeapModel(Node h, Node neq);
   /** get the heap and value sep.nil is equal to */
-  bool getHeapModel(Expr& h, Expr& neq) const;
+  bool getHeapModel(Expr& h, Expr& neq) const override;
   //---------------------------- end separation logic
 
   /** get the representative set object */
@@ -176,11 +176,11 @@ public:
   /** get the representative set object (FIXME: remove this, see #1199) */
   RepSet* getRepSetPtr() { return &d_rep_set; }
   /** return whether this node is a don't-care */
-  bool isDontCare(Expr expr) const;
+  bool isDontCare(Expr expr) const override;
   /** get value function for Exprs. */
-  Expr getValue( Expr expr ) const;
+  Expr getValue(Expr expr) const override;
   /** get cardinality for sort */
-  Cardinality getCardinality( Type t ) const;
+  Cardinality getCardinality(Type t) const override;
   /** print representative debug function */
   void printRepresentativeDebug( const char* c, Node r );
   /** print representative function */
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 269aa63db..6fde4a9af 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -234,34 +234,30 @@ public:
 
   ~TheoryUF();
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
-  void finishInit();
+  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
+  void finishInit() override;
 
-  void check(Effort);  
-  Node expandDefinition(LogicRequest &logicRequest, Node node);
-  void preRegisterTerm(TNode term);
-  Node explain(TNode n);
+  void check(Effort) override;
+  Node expandDefinition(LogicRequest& logicRequest, Node node) override;
+  void preRegisterTerm(TNode term) override;
+  Node explain(TNode n) override;
 
   bool collectModelInfo(TheoryModel* m) override;
 
-  void ppStaticLearn(TNode in, NodeBuilder<>& learned);
-  void presolve();
+  void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
+  void presolve() override;
 
-  void addSharedTerm(TNode n);
-  void computeCareGraph();
+  void addSharedTerm(TNode n) override;
+  void computeCareGraph() override;
 
-  void propagate(Effort effort);
-  Node getNextDecisionRequest( unsigned& priority );
+  void propagate(Effort effort) override;
+  Node getNextDecisionRequest(unsigned& priority) override;
 
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 
-  std::string identify() const {
-    return "THEORY_UF";
-  }
+  std::string identify() const override { return "THEORY_UF"; }
 
-  eq::EqualityEngine* getEqualityEngine() {
-    return &d_equalityEngine;
-  }
+  eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
 
   StrongSolverTheoryUF* getStrongSolver() {
     return d_thss;