Added check for infinite lemma loop

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 53cdd3fdc083ee7f9c5e9aa4785bc9a181cac5e5..97e8a0faa8e13ea85b0e2ad51a4ffc394689fc06 100644 (file)
--- 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 39fd900121672651d8e4586c7be1e307a7828d91..2a008382302f70a178962df43d419c46ee43ae6e 100644 (file)
--- 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);