4 files changed, 38 insertions, 33 deletions
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 */