diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 53cdd3fdc..97e8a0faa 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -87,6 +87,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_decisionRequests(c), d_permRef(c), d_modelConstraints(c), + d_lemmasSaved(c), d_inCheckModel(false) { StatisticsRegistry::registerStat(&d_numRow); @@ -1294,6 +1295,13 @@ void TheoryArrays::checkModel(Effort e) while (!d_lemmas.empty()) { Debug("arrays-model-based") << "Sending lemma: " << d_lemmas.back() << endl; d_out->lemma(d_lemmas.back()); +#ifdef CVC4_ASSERTIONS + context::CDList<Node>::const_iterator it = d_lemmasSaved.begin(), it_end = d_lemmasSaved.end(); + for (; it != it_end; ++it) { + Assert((*it) != d_lemmas.back()); + } + d_lemmasSaved.push_back(d_lemmas.back()); +#endif d_lemmas.pop_back(); } Assert(getSatContext()->getLevel() == d_topLevel); |