From: Clark Barrett <barrett@cs.nyu.edu>
Date: Thu, 11 Apr 2013 04:31:22 +0000 (-0400)
Subject: Added check for infinite lemma loop
X-Git-Tag: cvc5-1.0.0~7325
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3dc1ba4ef7630e8bed64a5d2fc8843611ad4dd1f;p=cvc5.git

Added check for infinite lemma loop
---

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