1 files changed, 5 insertions, 10 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index f111b23ce..cb5c7dfec 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -36,10 +36,8 @@ namespace quantifiers {
 
 TermDb::TermDb(QuantifiersState& qs,
                QuantifiersInferenceManager& qim,
-               QuantifiersRegistry& qr,
-               QuantifiersEngine* qe)
-    : d_quantEngine(qe),
-      d_qstate(qs),
+               QuantifiersRegistry& qr)
+    : d_qstate(qs),
       d_qim(qim),
       d_qreg(qr),
       d_termsContext(),
@@ -1083,19 +1081,16 @@ bool TermDb::reset( Theory::Effort effort ){
       }
       ++eqcs_i;
     }
-    TheoryEngine* te = d_quantEngine->getTheoryEngine();
-    const LogicInfo& logicInfo = te->getLogicInfo();
+    const LogicInfo& logicInfo = d_qstate.getLogicInfo();
     for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId)
     {
       if (!logicInfo.isTheoryEnabled(theoryId))
       {
         continue;
       }
-      Theory* theory = te->theoryOf(theoryId);
-      Assert(theory != nullptr);
       for (context::CDList<Assertion>::const_iterator
-               it = theory->facts_begin(),
-               it_end = theory->facts_end();
+               it = d_qstate.factsBegin(theoryId),
+               it_end = d_qstate.factsEnd(theoryId);
            it != it_end;
            ++it)
       {