1 files changed, 3 insertions, 16 deletions
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 704a65bfb..f6b8f30f4 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -28,7 +28,6 @@ QuantifiersModules::QuantifiersModules()
       d_alpha_equiv(nullptr),
       d_inst_engine(nullptr),
       d_model_engine(nullptr),
-      d_builder(nullptr),
       d_bint(nullptr),
       d_qcf(nullptr),
       d_sg_gen(nullptr),
@@ -45,6 +44,7 @@ void QuantifiersModules::initialize(QuantifiersState& qs,
                                     QuantifiersInferenceManager& qim,
                                     QuantifiersRegistry& qr,
                                     TermRegistry& tr,
+                                    QModelBuilder* builder,
                                     std::vector<QuantifiersModule*>& modules)
 {
   // add quantifiers modules
@@ -80,23 +80,10 @@ void QuantifiersModules::initialize(QuantifiersState& qs,
     d_bint.reset(new BoundedIntegers(qs, qim, qr, tr));
     modules.push_back(d_bint.get());
   }
+
   if (options::finiteModelFind() || options::fmfBound())
   {
-    Trace("quant-init-debug")
-        << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
-        << options::fmfBound() << std::endl;
-    if (tr.useFmcModel())
-    {
-      Trace("quant-init-debug") << "...make fmc builder." << std::endl;
-      d_builder.reset(new fmcheck::FullModelChecker(qs, qr, qim));
-    }
-    else
-    {
-      Trace("quant-init-debug")
-          << "...make default model builder." << std::endl;
-      d_builder.reset(new QModelBuilder(qs, qr, qim));
-    }
-    d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, d_builder.get()));
+    d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, builder));
     modules.push_back(d_model_engine.get());
   }
   if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)