diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2013-04-11 00:31:22 -0400 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-04-11 00:31:49 -0400 |
commit | 3dc1ba4ef7630e8bed64a5d2fc8843611ad4dd1f (patch) | |
tree | 71b4a18442c15f1525b7815e02058d36c12dbc19 /src | |
parent | 5684cdec81cee9a29958388e1980b369a48b05bb (diff) |
Added check for infinite lemma loop
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 8 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 1 |
2 files changed, 9 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); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 39fd90012..2a0083823 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -358,6 +358,7 @@ class TheoryArrays : public Theory { // List of nodes that need permanent references in this context context::CDList<Node> d_permRef; context::CDList<Node> d_modelConstraints; + context::CDList<Node> d_lemmasSaved; std::vector<Node> d_lemmas; Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true); |