found a bug in the initialization order of UF, EqualityEngine, and the UF strong...

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index ac194d5ed929d02cbd500eed65faeca27130e91e..d24878a62f6d0c8d1e6fa249c453d89848990497 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -31,6 +31,9 @@ using namespace CVC4::theory::uf;
 TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
   Theory(THEORY_UF, c, u, out, valuation, logicInfo, qe),
   d_notify(*this),
+  /* The strong theory solver can be notified by EqualityEngine::init(),
+   * so make sure it's initialized first. */
+  d_thss(Options::current()->finiteModelFind ? new StrongSolverTheoryUf(c, u, out, this) : NULL),
   d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"),
   d_conflict(c, false),
   d_literalsToPropagate(c),
@@ -39,13 +42,7 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel&
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
-
-  if (Options::current()->finiteModelFind) {
-    d_thss = new StrongSolverTheoryUf(c, u, out, this);
-  } else {
-    d_thss = NULL;
-  }
-}/* TheoryUF::TheoryUF() */
+}
 
 static Node mkAnd(const std::vector<TNode>& conjunctions) {
   Assert(conjunctions.size() > 0);

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index e2dd551745d8247c337a49fb38ebeacc4b844208..e5cb7e4f85be47637521297a2b8bd2228a650373 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1062,6 +1062,8 @@ Node StrongSolverTheoryUf::ConflictFind::getCardinalityLemma(){
 StrongSolverTheoryUf::StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) :
 d_out( &out ),
 d_th( th ),
+d_conf_find(),
+d_conf_types(),
 d_conf_find_init( c )
 {