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

1 files changed, 8 insertions, 3 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 395d51d3e..239385bfc 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -25,9 +25,9 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe)
-  : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe)
-  , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, qe))
+TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
+  : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
+  , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo))
 {}
 
 TheoryArith::~TheoryArith(){
@@ -42,6 +42,11 @@ void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_internal->setMasterEqualityEngine(eq);
 }
 
+void TheoryArith::setQuantifiersEngine(QuantifiersEngine* qe) {
+  this->Theory::setQuantifiersEngine(qe);
+  d_internal->setQuantifiersEngine(qe);
+}
+
 void TheoryArith::addSharedTerm(TNode n){
   d_internal->addSharedTerm(n);
 }