Delay QuantifiersEngine and UF strong solver initialization until after final options/logic are set.

1 files changed, 10 insertions, 3 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ff84e63b7..47ba50aad 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -60,6 +60,9 @@ using namespace CVC4;
 using namespace CVC4::theory;
 
 void TheoryEngine::finishInit() {
+  // initialize the quantifiers engine
+  d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
+
   if (d_logicInfo.isQuantified()) {
     d_quantEngine->finishInit();
     Assert(d_masterEqualityEngine == 0);
@@ -67,10 +70,17 @@ void TheoryEngine::finishInit() {
 
     for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
       if (d_theoryTable[theoryId]) {
+        d_theoryTable[theoryId]->setQuantifiersEngine(d_quantEngine);
         d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine);
       }
     }
   }
+
+  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
+    if (d_theoryTable[theoryId]) {
+      d_theoryTable[theoryId]->finishInit();
+    }
+  }
 }
 
 void TheoryEngine::eqNotifyNewClass(TNode t){
@@ -146,9 +156,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
     d_theoryOut[theoryId] = NULL;
   }
 
-  // initialize the quantifiers engine
-  d_quantEngine = new QuantifiersEngine(context, userContext, this);
-
   // build model information if applicable
   d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true);
   d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);