Added check for infinite lemma loop

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);