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

Adds missing override keywords.

31 files changed, 377 insertions, 319 deletions

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 */