From 7515ee9cda0925721c4fa7e1ba9ef3b25dc5e0d0 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 11 Jul 2011 19:34:01 +0000
Subject: [PATCH] fix some confusing debug output (bogus counter)

---
 src/theory/theory.h        | 2 +-
 src/theory/theory_engine.h | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 59d26ff05..56a5f2f76 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -141,7 +141,7 @@ protected:
     d_wasSharedTermFact = false;
     d_factsHead = d_factsHead + 1;
     Debug("theory") << "Theory::get() => " << fact
-                    << " (" << d_facts.size() << " left)" << std::endl;
+                    << " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
     d_out->newFact(fact);
     return fact;
   }
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 94ba8cabb..d4138f807 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -355,7 +355,7 @@ public:
    * @param node the assertion
    */
   inline void assertFact(TNode node) {
-    Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl<<d_logic<<std::endl;
+    Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
 
     // Mark it as asserted in this context
     //
@@ -369,7 +369,7 @@ public:
     // Again, equality is a special case
     if (atom.getKind() == kind::EQUAL) {
       if(d_logic == "QF_AX") {
-        //Debug("theory")<< "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays \n";
+        Debug("theory") << "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays" << std::endl;
         d_theoryTable[theory::THEORY_ARRAY]->assertFact(node);
       } else {
         theory::Theory* theory = theoryOf(atom);
@@ -443,7 +443,7 @@ public:
     TNode atom = node.getKind() == kind::NOT ? node[0] : node;
     if (atom.getKind() == kind::EQUAL) {
       if(d_logic == "QF_AX") {
-        //Debug("theory")<< "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays \n";
+        Debug("theory") << "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays" << std::endl;
         d_theoryTable[theory::THEORY_ARRAY]->explain(node);
       } else {
         theoryOf(atom[0])->explain(node);
-- 
2.30.2