From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 16 Jul 2012 15:52:36 +0000 (+0000)
Subject: found a bug in the initialization order of UF, EqualityEngine, and the UF strong... 
X-Git-Tag: cvc5-1.0.0~7926
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25396f93b7df85c80a39ed207483e28a8c86ff26;p=cvc5.git

found a bug in the initialization order of UF, EqualityEngine, and the UF strong solver; fixed
---

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index ac194d5ed..d24878a62 100644
--- 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 e2dd55174..e5cb7e4f8 100644
--- 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 )
 {