fix some confusing debug output (bogus counter)

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 59d26ff05ad51b27dbfa3743e9893f32eaa7a73b..56a5f2f76b93f9c10734dca6e9bdef788ca7b52f 100644 (file)
--- 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 94ba8cabbb1a950f9aa27a4255114585f1894b4f..d4138f80737647031de963a49876e7ad4f7940a4 100644 (file)
--- 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);