1 files changed, 15 insertions, 6 deletions
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index df866fbe1..cfccd4d93 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -30,6 +30,7 @@ class FirstOrderModel;
 class QuantifiersState;
 class QuantifiersRegistry;
 class QuantifiersInferenceManager;
+class TermRegistry;
 
 class QModelBuilder : public TheoryEngineModelBuilder
 {
@@ -43,9 +44,11 @@ class QModelBuilder : public TheoryEngineModelBuilder
 
  public:
   QModelBuilder(QuantifiersState& qs,
+                QuantifiersInferenceManager& qim,
                 QuantifiersRegistry& qr,
-                QuantifiersInferenceManager& qim);
-
+                TermRegistry& tr);
+  /** finish init, which sets the model object */
+  virtual void finishInit();
   //do exhaustive instantiation  
   // 0 :  failed, but resorting to true exhaustive instantiation may work
   // >0 : success
@@ -60,16 +63,22 @@ class QModelBuilder : public TheoryEngineModelBuilder
   //statistics 
   unsigned getNumAddedLemmas() { return d_addedLemmas; }
   unsigned getNumTriedLemmas() { return d_triedLemmas; }
+  /** get the model we are using */
+  FirstOrderModel* getModel();
 
  protected:
-  /** Pointer to quantifiers engine */
-  QuantifiersEngine* d_qe;
   /** The quantifiers state object */
   QuantifiersState& d_qstate;
+  /** The quantifiers inference manager */
+  QuantifiersInferenceManager& d_qim;
   /** Reference to the quantifiers registry */
   QuantifiersRegistry& d_qreg;
-  /** The quantifiers inference manager */
-  quantifiers::QuantifiersInferenceManager& d_qim;
+  /** Term registry */
+  TermRegistry& d_treg;
+  /** Pointer to the model object we are using */
+  FirstOrderModel* d_model;
+  /** The model object we have allocated */
+  std::unique_ptr<FirstOrderModel> d_modelAloc;
 };
 
 }  // namespace quantifiers