Removed debugging code

2 files changed, 1 insertions, 11 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index ff51e37c5..6b25ca2b9 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -31,8 +31,6 @@ using namespace std;
 
 namespace CVC4 {
 
-bool next_lemma_is_ext;
-
 namespace theory {
 namespace arrays {
 
@@ -98,7 +96,6 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_arrayMerges(c),
   d_inCheckModel(false)
 {
-  next_lemma_is_ext = false;
   StatisticsRegistry::registerStat(&d_numRow);
   StatisticsRegistry::registerStat(&d_numExt);
   StatisticsRegistry::registerStat(&d_numProp);
@@ -1298,7 +1295,6 @@ void TheoryArrays::check(Effort e) {
             Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
             Node eq = d_valuation.ensureLiteral(ak.eqNode(bk));
             Assert(eq.getKind() == kind::EQUAL);
-            next_lemma_is_ext = true;
             Node lemma = fact[0].orNode(eq.notNode());
             Trace("arrays-lem")<<"Arrays::addExtLemma " << lemma <<"\n";
             d_out->lemma(lemma);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a45810d26..18aad4022 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1379,9 +1379,6 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
   }
 }
 
-namespace CVC4 {
-extern bool next_lemma_is_ext;
-}
 
 theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo) {
   // For resource-limiting (also does a time check).
@@ -1395,10 +1392,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable
     ensureLemmaAtoms(collectAtoms.getAtoms(), atomsTo);
   }
 
-  if (CVC4::next_lemma_is_ext) {
-    CVC4::next_lemma_is_ext = false;
-  }
-  else if(Dump.isOn("t-lemmas")) {
+  if(Dump.isOn("t-lemmas")) {
     Node n = node;
     if (negated) {
       n = node.negate();