1 files changed, 7 insertions, 12 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 27ae0018e..16d68ea5c 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -169,8 +169,10 @@ void TheoryEngine::finishInit()
   // initialize the quantifiers engine
   if (d_logicInfo.isQuantified())
   {
-    // initialize the quantifiers engine
-    d_quantEngine = new QuantifiersEngine(this, *d_decManager.get(), d_pnm);
+    // get the quantifiers engine, which is initialized by the quantifiers
+    // theory
+    d_quantEngine = d_theoryTable[THEORY_QUANTIFIERS]->getQuantifiersEngine();
+    Assert(d_quantEngine != nullptr);
   }
   // initialize the theory combination manager, which decides and allocates the
   // equality engines to use for all theories.
@@ -178,10 +180,11 @@ void TheoryEngine::finishInit()
   // get pointer to the shared solver
   d_sharedSolver = d_tc->getSharedSolver();
 
-  // set the core equality engine on quantifiers engine
+  // finish initializing the quantifiers engine
   if (d_logicInfo.isQuantified())
   {
-    d_quantEngine->setMasterEqualityEngine(d_tc->getCoreEqualityEngine());
+    d_quantEngine->finishInit(
+        this, d_decManager.get(), d_tc->getCoreEqualityEngine());
   }
 
   // finish initializing the theories by linking them with the appropriate
@@ -205,12 +208,6 @@ void TheoryEngine::finishInit()
     // finish initializing the theory
     t->finishInit();
   }
-
-  // finish initializing the quantifiers engine
-  if (d_logicInfo.isQuantified())
-  {
-    d_quantEngine->finishInit();
-  }
 }
 
 ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; }
@@ -283,8 +280,6 @@ TheoryEngine::~TheoryEngine() {
     }
   }
 
-  delete d_quantEngine;
-
   smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
   smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
 }