1 files changed, 10 insertions, 11 deletions

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index f28db4c35..71b45915f 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -37,12 +37,10 @@ typedef expr::Attribute<StringsProxyVarAttributeId, bool>
     StringsProxyVarAttribute;
 
 TermRegistry::TermRegistry(SolverState& s,
-                           eq::EqualityEngine& ee,
                            OutputChannel& out,
                            SequencesStatistics& statistics,
                            ProofNodeManager* pnm)
     : d_state(s),
-      d_ee(ee),
       d_out(out),
       d_statistics(statistics),
       d_hasStrCode(false),
@@ -129,6 +127,7 @@ void TermRegistry::preRegisterTerm(TNode n)
   {
     return;
   }
+  eq::EqualityEngine* ee = d_state.getEqualityEngine();
   d_preregisteredTerms.insert(n);
   Trace("strings-preregister")
       << "TheoryString::preregister : " << n << std::endl;
@@ -156,15 +155,15 @@ void TermRegistry::preRegisterTerm(TNode n)
       ss << "Equality between regular expressions is not supported";
       throw LogicException(ss.str());
     }
-    d_ee.addTriggerEquality(n);
+    ee->addTriggerEquality(n);
     return;
   }
   else if (k == STRING_IN_REGEXP)
   {
     d_out.requirePhase(n, true);
-    d_ee.addTriggerPredicate(n);
-    d_ee.addTerm(n[0]);
-    d_ee.addTerm(n[1]);
+    ee->addTriggerPredicate(n);
+    ee->addTerm(n[0]);
+    ee->addTerm(n[1]);
     return;
   }
   else if (k == STRING_TO_CODE)
@@ -196,17 +195,17 @@ void TermRegistry::preRegisterTerm(TNode n)
         }
       }
     }
-    d_ee.addTerm(n);
+    ee->addTerm(n);
   }
   else if (tn.isBoolean())
   {
     // Get triggered for both equal and dis-equal
-    d_ee.addTriggerPredicate(n);
+    ee->addTriggerPredicate(n);
   }
   else
   {
     // Function applications/predicates
-    d_ee.addTerm(n);
+    ee->addTerm(n);
   }
   // Set d_functionsTerms stores all function applications that are
   // relevant to theory combination. Notice that this is a subset of
@@ -216,7 +215,7 @@ void TermRegistry::preRegisterTerm(TNode n)
   // Concatenation terms do not need to be considered here because
   // their arguments have string type and do not introduce any shared
   // terms.
-  if (n.hasOperator() && d_ee.isFunctionKind(k) && k != STRING_CONCAT)
+  if (n.hasOperator() && ee->isFunctionKind(k) && k != STRING_CONCAT)
   {
     d_functionsTerms.push_back(n);
   }
@@ -313,7 +312,7 @@ void TermRegistry::registerType(TypeNode tn)
   {
     // preregister the empty word for the type
     Node emp = Word::mkEmptyWord(tn);
-    if (!d_ee.hasTerm(emp))
+    if (!d_state.hasTerm(emp))
     {
       preRegisterTerm(emp);
     }