From: Tim King <taking@cs.nyu.edu>
Date: Thu, 14 Feb 2013 21:11:42 +0000 (-0500)
Subject: Removing BVDebug and replacing with Debug.
X-Git-Tag: cvc5-1.0.0~7406^2~7
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fc4121b761dd524ad5fe37789381e5814737e6b9;p=cvc5.git

Removing BVDebug and replacing with Debug.
---

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index c25c40c22..a952b2929 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -191,13 +191,13 @@ Node inline sLessThanBB(const Bits&a, const Bits& b, bool orEqual) {
 
 
 Node UndefinedAtomBBStrategy(TNode node, Bitblaster* bb) {
-  BVDebug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
+  Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
                      << node.getKind() << "\n";
   Unreachable(); 
 }
 
 Node DefaultEqBB(TNode node, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   
   Assert(node.getKind() == kind::EQUAL);
   Bits lhs, rhs; 
@@ -219,7 +219,7 @@ Node DefaultEqBB(TNode node, Bitblaster* bb) {
 
 
 Node AdderUltBB(TNode node, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   Assert(node.getKind() == kind::BITVECTOR_ULT);
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -241,7 +241,7 @@ Node AdderUltBB(TNode node, Bitblaster* bb) {
 
 
 Node DefaultUltBB(TNode node, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   Assert(node.getKind() == kind::BITVECTOR_ULT);
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -254,7 +254,7 @@ Node DefaultUltBB(TNode node, Bitblaster* bb) {
 }
 
 Node DefaultUleBB(TNode node, Bitblaster* bb){
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   Assert(node.getKind() == kind::BITVECTOR_ULE);
   Bits a, b;
   
@@ -267,31 +267,31 @@ Node DefaultUleBB(TNode node, Bitblaster* bb){
 }
 
 Node DefaultUgtBB(TNode node, Bitblaster* bb){
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
 Node DefaultUgeBB(TNode node, Bitblaster* bb){
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
 
 // Node DefaultSltBB(TNode node, Bitblaster* bb){
-//   BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+//   Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 //   // shoudl be rewritten in terms of ult
 //   Unimplemented(); 
 // }
 
 // Node DefaultSleBB(TNode node, Bitblaster* bb){
-//   BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+//   Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 //   // shoudl be rewritten in terms of ule
 //   Unimplemented(); 
 // }
 
 
 Node DefaultSltBB(TNode node, Bitblaster* bb){
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -303,7 +303,7 @@ Node DefaultSltBB(TNode node, Bitblaster* bb){
 }
 
 Node DefaultSleBB(TNode node, Bitblaster* bb){
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -315,13 +315,13 @@ Node DefaultSleBB(TNode node, Bitblaster* bb){
 }
  
 Node DefaultSgtBB(TNode node, Bitblaster* bb){
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
 
 Node DefaultSgeBB(TNode node, Bitblaster* bb){
-  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
@@ -330,7 +330,7 @@ Node DefaultSgeBB(TNode node, Bitblaster* bb){
 /// Term bitblasting strategies 
 
 void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
+  Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
                      << node.getKind() << "\n";
   Unreachable(); 
 }
@@ -342,15 +342,15 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
   }
 
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
-    BVDebug("bitvector-bb") << "                           with bits  " << toString(bits); 
+    Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
+    Debug("bitvector-bb") << "                           with bits  " << toString(bits); 
   }
 
    bb->storeVariable(node);
 }
 
 void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::CONST_BITVECTOR);
   Assert(bits.size() == 0);
   
@@ -364,13 +364,13 @@ void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
     }
   }
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+    Debug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
   }
 }
 
 
 void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_NOT);
   Assert(bits.size() == 0);
   Bits bv; 
@@ -379,7 +379,7 @@ void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
   Assert(bits.size() == 0);
   
   Assert (node.getKind() == kind::BITVECTOR_CONCAT);
@@ -394,12 +394,12 @@ void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) {
   }
   Assert (bits.size() == utils::getSize(node)); 
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+    Debug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
   }
 }
 
 void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
   
   Assert(node.getKind() == kind::BITVECTOR_AND &&
          bits.size() == 0);
@@ -417,7 +417,7 @@ void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultOrBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
 
   Assert(node.getKind() == kind::BITVECTOR_OR &&
          bits.size() == 0);
@@ -435,7 +435,7 @@ void DefaultOrBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultXorBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
 
   Assert(node.getKind() == kind::BITVECTOR_XOR &&
          bits.size() == 0);
@@ -456,7 +456,7 @@ void DefaultXorBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
 
   Assert(node.getNumChildren() == 2 &&
          node.getKind() == kind::BITVECTOR_XNOR &&
@@ -473,17 +473,17 @@ void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) {
 
 
 void DefaultNandBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultNorBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
+  Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
 
   Assert(getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP);
   Bits a, b;
@@ -501,7 +501,7 @@ void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
+  Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
   Assert(res.size() == 0 &&
          node.getKind() == kind::BITVECTOR_MULT);
 
@@ -517,12 +517,12 @@ void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) {
     res = newres;
   }
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+    Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
   }
 }
 
 void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_PLUS &&
          res.size() == 0);
 
@@ -543,7 +543,7 @@ void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
 
 
 void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_SUB &&
          node.getNumChildren() == 2 &&
          bits.size() == 0);
@@ -561,7 +561,7 @@ void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_NEG);
   
   Bits a;
@@ -639,7 +639,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid
 }
 
 void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&  q.size() == 0);
 
   Bits a, b;
@@ -666,7 +666,7 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
 }
 
 void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL &&  rem.size() == 0);
 
   Bits a, b;
@@ -694,23 +694,23 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
 
 
 void DefaultSdivBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultSremBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultSmodBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 
 void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node  << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node  << "\n";
   Assert (node.getKind() == kind::BITVECTOR_SHL &&
           res.size() == 0);
   Bits a, b;
@@ -738,12 +738,12 @@ void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) {
     }
   }
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+    Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
   }
 }
 
 void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node  << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node  << "\n";
   Assert (node.getKind() == kind::BITVECTOR_LSHR &&
           res.size() == 0);
   Bits a, b;
@@ -771,13 +771,13 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
     }
   }
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+    Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
   }
 }
 
 void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
 
-  BVDebug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node  << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node  << "\n";
   Assert (node.getKind() == kind::BITVECTOR_ASHR &&
           res.size() == 0);
   Bits a, b;
@@ -806,7 +806,7 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
     }
   }
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+    Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
   }
 }
 
@@ -825,14 +825,14 @@ void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) {
   Assert (bits.size() == high - low + 1);   
 
   if(Debug.isOn("bitvector-bb")) {
-    BVDebug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
-    BVDebug("bitvector-bb") << "                               with bits " << toString(bits); 
+    Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
+    Debug("bitvector-bb") << "                               with bits " << toString(bits); 
   }
 }
 
 
 void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   // this should be rewritten 
   Unimplemented(); 
@@ -840,7 +840,7 @@ void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) {
 
 void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
 
-  BVDebug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node  << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node  << "\n";
  
   // this should be rewritten 
   Unimplemented();
@@ -848,7 +848,7 @@ void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
 }
 
 void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
-  BVDebug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node  << "\n";
+  Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node  << "\n";
 
   Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
           res_bits.size() == 0);
@@ -871,14 +871,14 @@ void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
 }
 
 void DefaultRotateRightBB (TNode node, Bits& res, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
 
   Unimplemented(); 
 }
 
 void DefaultRotateLeftBB (TNode node, Bits& bits, Bitblaster* bb) {
-  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
+  Debug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 91482526a..4f5325e10 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -92,7 +92,7 @@ void Bitblaster::bbAtom(TNode node) {
   // make sure it is marked as an atom
   addAtom(node); 
 
-  BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
+  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
   ++d_statistics.d_numAtoms;
   // the bitblasted definition of the atom
   Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
@@ -115,7 +115,7 @@ void Bitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
-  BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
+  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
   ++d_statistics.d_numTerms;
 
   d_termBBStrategies[node.getKind()] (node, bits,this);
@@ -195,8 +195,8 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) {
     markerLit = ~markerLit;
   }
   
-  BVDebug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n";
-  BVDebug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal:   " << markerLit << "\n";  
+  Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n";
+  Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal:   " << markerLit << "\n";  
 
   SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
 
@@ -221,7 +221,7 @@ bool Bitblaster::solve(bool quick_solve) {
       Trace("bitvector") << "     " << d_cnfStream->getNode(*it) << "\n";
     }
   }
-  BVDebug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; 
+  Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; 
   return SAT_VALUE_TRUE == d_satSolver->solve(); 
 }
 
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index e113048b8..501aafb29 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -53,7 +53,7 @@ void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
 }
 
 bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
-  BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl;
+  Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl;
 
   //// Eager bit-blasting
   if (options::bitvectorEagerBitblast()) {
@@ -106,7 +106,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
   // solving
   if (e == Theory::EFFORT_FULL || options::bitvectorEagerFullcheck()) {
     Assert(!d_bv->inConflict());
-    BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n";
+    Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n";
     bool ok = d_bitblaster->solve();
     if (!ok) {
       std::vector<TNode> conflictAtoms;
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index ca3e3e35c..f11b1252b 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -131,7 +131,7 @@ bool EqualitySolver::addAssertions(const std::vector<TNode>& assertions, Theory:
 }
 
 bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
-  BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+  Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
   if (value) {
     return d_solver.storePropagation(equality);
   } else {
@@ -140,7 +140,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool v
 }
 
 bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
-  BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
+  Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
   if (value) {
     return d_solver.storePropagation(predicate);
   } else {
diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h
index e4bcbca47..ec7f6d66d 100644
--- a/src/theory/bv/cd_set_collection.h
+++ b/src/theory/bv/cd_set_collection.h
@@ -71,7 +71,7 @@ class BacktrackableSetCollection {
       const tree_entry_type& node = d_memory.back();
 
       if(Debug.isOn("cd_set_collection")) {
-        BVDebug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue()
+        Debug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue()
                                      << " from " << internalToString(getRoot(d_memory.size()-1)) << std::endl;
       }
 
@@ -279,7 +279,7 @@ public:
     // Find the biggest node smaleer than value (it must exist)
     while (set != null) {
       if(Debug.isOn("set_collection")) {
-        BVDebug("set_collection") << "BacktrackableSetCollection::getPrev(" << toString(set) << "," << value << ")" << std::endl;
+        Debug("set_collection") << "BacktrackableSetCollection::getPrev(" << toString(set) << "," << value << ")" << std::endl;
       }
       const tree_entry_type& node = d_memory[set];
       if (node.getValue() >= value) {
@@ -308,7 +308,7 @@ public:
     // Find the smallest node bigger than value (it must exist)
     while (set != null) {
       if(Debug.isOn("set_collection")) {
-        BVDebug("set_collection") << "BacktrackableSetCollection::getNext(" << toString(set) << "," << value << ")" << std::endl;
+        Debug("set_collection") << "BacktrackableSetCollection::getNext(" << toString(set) << "," << value << ")" << std::endl;
       }
       const tree_entry_type& node = d_memory[set];
       if (node.getValue() <= value) {
@@ -377,7 +377,7 @@ public:
     Assert(isValid(set));
 
     if(Debug.isOn("set_collection")) {
-      BVDebug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl;
+      Debug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl;
     }
 
     // Empty set no elements
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 7acb93cc2..de5b70557 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -72,7 +72,7 @@ TheoryBV::Statistics::~Statistics() {
 }
 
 void TheoryBV::preRegisterTerm(TNode node) {
-  BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
+  Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
 
   if (options::bitvectorEagerBitblast()) {
     // don't use the equality engine in the eager bit-blasting
@@ -88,7 +88,7 @@ void TheoryBV::sendConflict() {
   if (d_conflictNode.isNull()) {
     return;
   } else {
-    BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
+    Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
     d_out->conflict(d_conflictNode);
     d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
     d_conflictNode = Node::null();
@@ -97,7 +97,7 @@ void TheoryBV::sendConflict() {
 
 void TheoryBV::check(Effort e)
 {
-  BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
+  Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
 
   // if we are already in conflict just return the conflict
   if (inConflict()) {
@@ -111,7 +111,7 @@ void TheoryBV::check(Effort e)
     Assertion assertion = get();
     TNode fact = assertion.assertion;
     new_assertions.push_back(fact);
-    BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n";
+    Debug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n";
   }
 
   if (!inConflict()) {
@@ -138,7 +138,7 @@ void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
 }
 
 void TheoryBV::propagate(Effort e) {
-  BVDebug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
+  Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
 
   if (inConflict()) {
     return;
@@ -152,7 +152,7 @@ void TheoryBV::propagate(Effort e) {
   }
 
   if (!ok) {
-    BVDebug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl;
+    Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl;
     setConflict();
   }
 }
@@ -197,7 +197,7 @@ Node TheoryBV::ppRewrite(TNode t)
 
 bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 {
-  Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
+  Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
 
   // If already in conflict, no more propagation
   if (d_conflict) {
@@ -240,18 +240,18 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
   // Ask the appropriate subtheory for the explanation
   if (propagatedBy(literal, SUB_EQUALITY)) {
-    BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl;
+    Debug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl;
     d_equalitySolver.explain(literal, assumptions);
   } else {
     Assert(propagatedBy(literal, SUB_BITBLAST));
-    BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;
+    Debug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;
     d_bitblastSolver.explain(literal, assumptions);
   }
 }
 
 
 Node TheoryBV::explain(TNode node) {
-  BVDebug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
+  Debug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
   std::vector<TNode> assumptions;
 
   // Ask for the explanation
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index f9650932e..bd7a8131a 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -334,7 +334,7 @@ public:
   template<bool checkApplies>
   static inline Node run(TNode node) {
     if (!checkApplies || applies(node)) {
-      BVDebug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ")" << std::endl;
+      Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ")" << std::endl;
       Assert(checkApplies || applies(node));
       //++ s_statistics->d_ruleApplications;
       Node result = apply(node);
@@ -355,7 +355,7 @@ public:
             << CheckSatCommand(condition.toExpr());
         }
       }
-      BVDebug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl;
+      Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl;
       return result;
     } else {
       return node;
@@ -486,7 +486,7 @@ bool RewriteRule<EmptyRule>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EmptyRule>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EmptyRule> for " << node.getKind() <<"\n"; 
+  Debug("bv-rewrite") << "RewriteRule<EmptyRule> for " << node.getKind() <<"\n"; 
   Unreachable();
   return node;
 }
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 498378638..178b17b43 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -37,7 +37,7 @@ bool RewriteRule<EvalAnd>::applies(TNode node) {
 template<> inline
 Node RewriteRule<EvalAnd>::apply(TNode node) {
   Unreachable();
-  BVDebug("bv-rewrite") << "RewriteRule<EvalAnd>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalAnd>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
   BitVector res = a & b;
@@ -56,7 +56,7 @@ bool RewriteRule<EvalOr>::applies(TNode node) {
 template<> inline
 Node RewriteRule<EvalOr>::apply(TNode node) {
   Unreachable();
-  BVDebug("bv-rewrite") << "RewriteRule<EvalOr>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalOr>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
   BitVector res = a | b;
@@ -75,7 +75,7 @@ bool RewriteRule<EvalXor>::applies(TNode node) {
 template<> inline
 Node RewriteRule<EvalXor>::apply(TNode node) {
   Unreachable();
-  BVDebug("bv-rewrite") << "RewriteRule<EvalXor>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalXor>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
   BitVector res = a ^ b;
@@ -91,7 +91,7 @@ Node RewriteRule<EvalXor>::apply(TNode node) {
 
 // template<> inline
 // Node RewriteRule<EvalXnor>::apply(TNode node) {
-//   BVDebug("bv-rewrite") << "RewriteRule<EvalXnor>(" << node << ")" << std::endl;
+//   Debug("bv-rewrite") << "RewriteRule<EvalXnor>(" << node << ")" << std::endl;
 //   BitVector a = node[0].getConst<BitVector>();
 //   BitVector b = node[1].getConst<BitVector>();
 //   BitVector res = ~ (a ^ b);
@@ -106,7 +106,7 @@ bool RewriteRule<EvalNot>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalNot>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalNot>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalNot>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector res = ~ a;
   return utils::mkConst(res);
@@ -120,7 +120,7 @@ Node RewriteRule<EvalNot>::apply(TNode node) {
 
 // template<> inline
 // Node RewriteRule<EvalComp>::apply(TNode node) {
-//   BVDebug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl;
+//   Debug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl;
 //   BitVector a = node[0].getConst<BitVector>();
 //   BitVector b = node[1].getConst<BitVector>();
 //   BitVector res;
@@ -141,7 +141,7 @@ bool RewriteRule<EvalMult>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalMult>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalMult>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalMult>(" << node << ")" << std::endl;
   TNode::iterator child_it = node.begin();
   BitVector res = (*child_it).getConst<BitVector>();
   for(++child_it; child_it != node.end(); ++child_it) {
@@ -158,7 +158,7 @@ bool RewriteRule<EvalPlus>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalPlus>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalPlus>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalPlus>(" << node << ")" << std::endl;
   TNode::iterator child_it = node.begin();
   BitVector res = (*child_it).getConst<BitVector>();
   for(++child_it; child_it != node.end(); ++child_it) {
@@ -175,7 +175,7 @@ Node RewriteRule<EvalPlus>::apply(TNode node) {
 
 // template<> inline
 // Node RewriteRule<EvalSub>::apply(TNode node) {
-//   BVDebug("bv-rewrite") << "RewriteRule<EvalSub>(" << node << ")" << std::endl;
+//   Debug("bv-rewrite") << "RewriteRule<EvalSub>(" << node << ")" << std::endl;
 //   BitVector a = node[0].getConst<BitVector>();
 //   BitVector b = node[1].getConst<BitVector>();
 //   BitVector res = a - b;
@@ -190,7 +190,7 @@ bool RewriteRule<EvalNeg>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalNeg>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalNeg>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalNeg>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector res = - a;
   
@@ -204,7 +204,7 @@ bool RewriteRule<EvalUdiv>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalUdiv>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
   BitVector res = a.unsignedDivTotal(b);
@@ -219,7 +219,7 @@ bool RewriteRule<EvalUrem>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalUrem>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
   BitVector res = a.unsignedRemTotal(b);
@@ -234,7 +234,7 @@ bool RewriteRule<EvalShl>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalShl>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalShl>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalShl>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
 
@@ -250,7 +250,7 @@ bool RewriteRule<EvalLshr>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalLshr>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalLshr>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalLshr>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
   
@@ -266,7 +266,7 @@ bool RewriteRule<EvalAshr>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalAshr>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalAshr>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalAshr>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
 
@@ -282,7 +282,7 @@ bool RewriteRule<EvalUlt>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalUlt>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalUlt>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalUlt>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
 
@@ -300,7 +300,7 @@ bool RewriteRule<EvalSlt>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalSlt>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalSlt>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalSlt>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
 
@@ -319,7 +319,7 @@ bool RewriteRule<EvalUle>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalUle>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalUle>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalUle>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
 
@@ -337,7 +337,7 @@ bool RewriteRule<EvalSle>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalSle>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalSle>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalSle>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
 
@@ -355,7 +355,7 @@ bool RewriteRule<EvalExtract>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalExtract>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalExtract>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalExtract>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   unsigned lo = utils::getExtractLow(node);
   unsigned hi = utils::getExtractHigh(node);
@@ -373,7 +373,7 @@ bool RewriteRule<EvalConcat>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalConcat>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalConcat>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalConcat>(" << node << ")" << std::endl;
   unsigned num = node.getNumChildren();
   BitVector res = node[0].getConst<BitVector>();
   for(unsigned i = 1; i < num; ++i ) {  
@@ -391,7 +391,7 @@ bool RewriteRule<EvalSignExtend>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalSignExtend>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalSignExtend>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalSignExtend>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount; 
   BitVector res = a.signExtend(amount);
@@ -407,7 +407,7 @@ bool RewriteRule<EvalEquals>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<EvalEquals>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<EvalEquals>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<EvalEquals>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
   if (a == b) {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index b44c72f74..ade345d1c 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -33,7 +33,7 @@ bool RewriteRule<ConcatFlatten>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<ConcatFlatten>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl;
   NodeBuilder<> result(kind::BITVECTOR_CONCAT);
   std::vector<Node> processing_stack;
   processing_stack.push_back(node);
@@ -48,7 +48,7 @@ Node RewriteRule<ConcatFlatten>::apply(TNode node) {
     }
   }
   Node resultNode = result;
-  BVDebug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << resultNode << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << resultNode << ")" << std::endl;
   return resultNode;
 }
 
@@ -60,7 +60,7 @@ bool RewriteRule<ConcatExtractMerge>::applies(TNode node) {
 template<> inline
 Node RewriteRule<ConcatExtractMerge>::apply(TNode node) {
 
-  BVDebug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl;
 
   std::vector<Node> mergedExtracts;
 
@@ -121,7 +121,7 @@ bool RewriteRule<ConcatConstantMerge>::applies(TNode node) {
 template<> inline
 Node RewriteRule<ConcatConstantMerge>::apply(TNode node) {
 
-  BVDebug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl;
 
   std::vector<Node> mergedConstants;
   for (unsigned i = 0, end = node.getNumChildren(); i < end;) {
@@ -150,7 +150,7 @@ Node RewriteRule<ConcatConstantMerge>::apply(TNode node) {
     }
   }
 
-  BVDebug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl;
 
   return utils::mkConcat(mergedConstants);
 }
@@ -168,7 +168,7 @@ bool RewriteRule<ExtractWhole>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<ExtractWhole>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl;
   return node[0];
 }
 
@@ -181,7 +181,7 @@ bool RewriteRule<ExtractConstant>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<ExtractConstant>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl;
   Node child = node[0];
   BitVector childValue = child.getConst<BitVector>();
   return utils::mkConst(childValue.extract(utils::getExtractHigh(node), utils::getExtractLow(node)));
@@ -189,7 +189,7 @@ Node RewriteRule<ExtractConstant>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<ExtractConcat>::applies(TNode node) {
-  //BVDebug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
+  //Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
   if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
   if (node[0].getKind() != kind::BITVECTOR_CONCAT) return false;
   return true;
@@ -197,7 +197,7 @@ bool RewriteRule<ExtractConcat>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<ExtractConcat>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
   int extract_high = utils::getExtractHigh(node);
   int extract_low = utils::getExtractLow(node);
 
@@ -230,7 +230,7 @@ bool RewriteRule<ExtractExtract>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<ExtractExtract>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl;
 
   // x[i:j][k:l] ~>  x[k+j:l+j]
   Node child = node[0];
@@ -244,7 +244,7 @@ Node RewriteRule<ExtractExtract>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<FailEq>::applies(TNode node) {
-  //BVDebug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
+  //Debug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
   if (node.getKind() != kind::EQUAL) return false;
   if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
   if (node[1].getKind() != kind::CONST_BITVECTOR) return false;
@@ -264,7 +264,7 @@ bool RewriteRule<SimplifyEq>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<SimplifyEq>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl;
   return utils::mkTrue();
 }
 
@@ -275,7 +275,7 @@ bool RewriteRule<ReflexivityEq>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<ReflexivityEq>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
   return node[1].eqNode(node[0]);
 }
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 6b3d0f770..39f55f26c 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -41,7 +41,7 @@ bool RewriteRule<ExtractBitwise>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<ExtractBitwise>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<ExtractBitwise>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ExtractBitwise>(" << node << ")" << std::endl;
   unsigned high = utils::getExtractHigh(node);
   unsigned low = utils::getExtractLow(node);
   std::vector<Node> children; 
@@ -65,7 +65,7 @@ bool RewriteRule<ExtractNot>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<ExtractNot>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<ExtractNot>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ExtractNot>(" << node << ")" << std::endl;
   unsigned low = utils::getExtractLow(node);
   unsigned high = utils::getExtractHigh(node);
   Node a = utils::mkExtract(node[0][0], high, low);
@@ -88,7 +88,7 @@ bool RewriteRule<ExtractArith>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<ExtractArith>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<ExtractArith>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ExtractArith>(" << node << ")" << std::endl;
   unsigned low = utils::getExtractLow(node);
   Assert (low == 0); 
   unsigned high = utils::getExtractHigh(node);
@@ -117,7 +117,7 @@ bool RewriteRule<ExtractArith2>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<ExtractArith2>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<ExtractArith2>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ExtractArith2>(" << node << ")" << std::endl;
   unsigned low = utils::getExtractLow(node);
   unsigned high = utils::getExtractHigh(node);
   std::vector<Node> children;
@@ -151,7 +151,7 @@ bool RewriteRule<FlattenAssocCommut>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<FlattenAssocCommut>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl;
   std::vector<Node> processingStack;
   processingStack.push_back(node);
   std::vector<Node> children;
@@ -291,7 +291,7 @@ bool RewriteRule<PlusCombineLikeTerms>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<PlusCombineLikeTerms>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<PlusCombineLikeTerms>(" << node << ")" << std::endl;
   unsigned size = utils::getSize(node); 
   BitVector constSum(size, (unsigned)0); 
   std::map<Node, BitVector> factorToCoefficient;
@@ -348,7 +348,7 @@ bool RewriteRule<MultSimplify>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<MultSimplify>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<MultSimplify>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<MultSimplify>(" << node << ")" << std::endl;
   unsigned size = utils::getSize(node); 
   BitVector constant(size, Integer(1));
 
@@ -397,7 +397,7 @@ bool RewriteRule<MultDistribConst>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<MultDistribConst>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<MultDistribConst>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<MultDistribConst>(" << node << ")" << std::endl;
 
   TNode constant = node[1];
   TNode factor = node[0];
@@ -434,7 +434,7 @@ bool RewriteRule<SolveEq>::applies(TNode node) {
 // Doesn't do full solving (yet), instead, if a term appears both on lhs and rhs, it subtracts from both sides so that one side's coeff is zero
 template<> inline
 Node RewriteRule<SolveEq>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<SolveEq>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<SolveEq>(" << node << ")" << std::endl;
 
   TNode left = node[0];
   TNode right = node[1];
@@ -662,7 +662,7 @@ static inline Node mkNodeKind(Kind k, TNode node, TNode c) {
 
 template<> inline
 Node RewriteRule<BitwiseEq>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<BitwiseEq>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<BitwiseEq>(" << node << ")" << std::endl;
 
   TNode term;
   BitVector c;
@@ -745,7 +745,7 @@ bool RewriteRule<NegMult>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<NegMult>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl;
   TNode mult = node[0];
   NodeBuilder<> nb(kind::BITVECTOR_MULT);
   BitVector bv(utils::getSize(node), (unsigned)1);
@@ -767,7 +767,7 @@ bool RewriteRule<NegSub>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<NegSub>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<NegSub>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<NegSub>(" << node << ")" << std::endl;
   return utils::mkNode(kind::BITVECTOR_SUB, node[0][1], node[0][0]);
 }
 
@@ -779,7 +779,7 @@ bool RewriteRule<NegPlus>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<NegPlus>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<NegPlus>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<NegPlus>(" << node << ")" << std::endl;
   std::vector<Node> children;
   for (unsigned i = 0; i < node[0].getNumChildren(); ++i) {
     children.push_back(utils::mkNode(kind::BITVECTOR_NEG, node[0][i])); 
@@ -820,7 +820,7 @@ bool RewriteRule<AndSimplify>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<AndSimplify>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
 
   // this will remove duplicates
   std::hash_map<TNode, Count, TNodeHashFunction> subterms;
@@ -883,7 +883,7 @@ bool RewriteRule<OrSimplify>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<OrSimplify>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl;
 
   // this will remove duplicates
   std::hash_map<TNode, Count, TNodeHashFunction> subterms;
@@ -946,7 +946,7 @@ bool RewriteRule<XorSimplify>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<XorSimplify>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl;
 
 
   std::hash_map<TNode, Count, TNodeHashFunction> subterms;
@@ -1041,7 +1041,7 @@ Node RewriteRule<XorSimplify>::apply(TNode node) {
 
 // template<> inline
 // Node RewriteRule<AndSimplify>::apply(TNode node) {
-//   BVDebug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
+//   Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
 //   return resultNode;
 // }
 
@@ -1053,7 +1053,7 @@ Node RewriteRule<XorSimplify>::apply(TNode node) {
 
 // template<> inline
 // Node RewriteRule<>::apply(TNode node) {
-//   BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
+//   Debug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
 //   return resultNode;
 // }
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 94983e03a..4202f8c2e 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -33,7 +33,7 @@ bool RewriteRule<UgtEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<UgtEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<UgtEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<UgtEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1];
   Node result = utils::mkNode(kind::BITVECTOR_ULT, b, a);
@@ -48,7 +48,7 @@ bool RewriteRule<UgeEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<UgeEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<UgeEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<UgeEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1];
   Node result = utils::mkNode(kind::BITVECTOR_ULE, b, a);
@@ -63,7 +63,7 @@ bool RewriteRule<SgtEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<SgtEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<SgtEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<SgtEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1];
   Node result = utils::mkNode(kind::BITVECTOR_SLT, b, a);
@@ -78,7 +78,7 @@ bool RewriteRule<SgeEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<SgeEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<SgeEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<SgeEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1];
   Node result = utils::mkNode(kind::BITVECTOR_SLE, b, a);
@@ -92,7 +92,7 @@ bool RewriteRule<SltEliminate>::applies(TNode node) {
 
 template <>
 Node RewriteRule<SltEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<SltEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<SltEliminate>(" << node << ")" << std::endl;
   
   unsigned size = utils::getSize(node[0]);
   Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1)));
@@ -110,7 +110,7 @@ bool RewriteRule<SleEliminate>::applies(TNode node) {
 
 template <>
 Node RewriteRule<SleEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")" << std::endl;
   
   unsigned size = utils::getSize(node[0]);
   Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1)));
@@ -128,7 +128,7 @@ bool RewriteRule<CompEliminate>::applies(TNode node) {
 
 template <>
 Node RewriteRule<CompEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<CompEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<CompEliminate>(" << node << ")" << std::endl;
   Node comp = utils::mkNode(kind::EQUAL, node[0], node[1]);
   Node one = utils::mkConst(1, 1);
   Node zero = utils::mkConst(1, 0); 
@@ -143,7 +143,7 @@ bool RewriteRule<SubEliminate>::applies(TNode node) {
 
 template <>
 Node RewriteRule<SubEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<SubEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<SubEliminate>(" << node << ")" << std::endl;
   Node negb = utils::mkNode(kind::BITVECTOR_NEG, node[1]);
   Node a = node[0];
 
@@ -158,7 +158,7 @@ bool RewriteRule<RepeatEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<RepeatEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<RepeatEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<RepeatEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned amount = node.getOperator().getConst<BitVectorRepeat>().repeatAmount;
   Assert(amount >= 1);
@@ -180,7 +180,7 @@ bool RewriteRule<RotateLeftEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<RotateLeftEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<RotateLeftEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<RotateLeftEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned amount = node.getOperator().getConst<BitVectorRotateLeft>().rotateLeftAmount;
   amount = amount % utils::getSize(a); 
@@ -202,7 +202,7 @@ bool RewriteRule<RotateRightEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<RotateRightEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<RotateRightEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<RotateRightEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned amount = node.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount;
   amount = amount % utils::getSize(a); 
@@ -225,7 +225,7 @@ bool RewriteRule<NandEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<NandEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<NandEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<NandEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1]; 
   Node andNode = utils::mkNode(kind::BITVECTOR_AND, a, b);
@@ -241,7 +241,7 @@ bool RewriteRule<NorEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<NorEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<NorEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<NorEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1]; 
   Node orNode = utils::mkNode(kind::BITVECTOR_OR, a, b);
@@ -257,7 +257,7 @@ bool RewriteRule<XnorEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<XnorEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<XnorEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<XnorEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1]; 
   Node xorNode = utils::mkNode(kind::BITVECTOR_XOR, a, b);
@@ -272,7 +272,7 @@ bool RewriteRule<SdivEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<SdivEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<SdivEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<SdivEliminate>(" << node << ")" << std::endl;
 
   TNode a = node[0];
   TNode b = node[1];
@@ -301,7 +301,7 @@ bool RewriteRule<SremEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<SremEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<SremEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<SremEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1];
   unsigned size = utils::getSize(a);
@@ -327,7 +327,7 @@ bool RewriteRule<SmodEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<SmodEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")" << std::endl;
   TNode s = node[0];
   TNode t = node[1];
   unsigned size = utils::getSize(s);
@@ -382,7 +382,7 @@ bool RewriteRule<ZeroExtendEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<ZeroExtendEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<ZeroExtendEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ZeroExtendEliminate>(" << node << ")" << std::endl;
 
   TNode bv = node[0];
   unsigned amount = node.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
@@ -402,7 +402,7 @@ bool RewriteRule<SignExtendEliminate>::applies(TNode node) {
 
 template<>
 Node RewriteRule<SignExtendEliminate>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<SignExtendEliminate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<SignExtendEliminate>(" << node << ")" << std::endl;
 
   unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
   if(amount == 0) {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 23cd8381d..a8aef748b 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -43,7 +43,7 @@ bool RewriteRule<ShlByConst>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<ShlByConst>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl;
   Integer amount = node[1].getConst<BitVector>().toInteger();
   
   Node a = node[0]; 
@@ -79,7 +79,7 @@ bool RewriteRule<LshrByConst>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<LshrByConst>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl;
   Integer amount = node[1].getConst<BitVector>().toInteger();
   
   Node a = node[0]; 
@@ -115,7 +115,7 @@ bool RewriteRule<AshrByConst>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<AshrByConst>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl;
   Integer amount = node[1].getConst<BitVector>().toInteger();
   
   Node a = node[0]; 
@@ -160,7 +160,7 @@ bool RewriteRule<BitwiseIdemp>::applies(TNode node) {
 template<> inline
 Node RewriteRule<BitwiseIdemp>::apply(TNode node) {
   Unreachable();
-  BVDebug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl;
   return node[0]; 
 }
 
@@ -183,7 +183,7 @@ bool RewriteRule<AndZero>::applies(TNode node) {
 template<> inline
 Node RewriteRule<AndZero>::apply(TNode node) {
   Unreachable();
-  BVDebug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 0); 
 }
 
@@ -207,7 +207,7 @@ bool RewriteRule<AndOne>::applies(TNode node) {
 template<> inline
 Node RewriteRule<AndOne>::apply(TNode node) {
   Unreachable();
-  BVDebug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl;
   unsigned size = utils::getSize(node);
   
   if (node[0] == utils::mkOnes(size)) {
@@ -237,7 +237,7 @@ bool RewriteRule<OrZero>::applies(TNode node) {
 template<> inline
 Node RewriteRule<OrZero>::apply(TNode node) {
   Unreachable();
-  BVDebug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl;
   
   unsigned size = utils::getSize(node); 
   if (node[0] == utils::mkConst(size, 0)) {
@@ -268,7 +268,7 @@ bool RewriteRule<OrOne>::applies(TNode node) {
 template<> inline
 Node RewriteRule<OrOne>::apply(TNode node) {
   Unreachable();
-  BVDebug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl;
   return utils::mkOnes(utils::getSize(node)); 
 }
 
@@ -290,7 +290,7 @@ bool RewriteRule<XorDuplicate>::applies(TNode node) {
 template<> inline
 Node RewriteRule<XorDuplicate>::apply(TNode node) {
   Unreachable();
-  BVDebug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl;
   return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); 
 }
 
@@ -316,7 +316,7 @@ bool RewriteRule<XorOne>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<XorOne>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl;
   Node ones = utils::mkOnes(utils::getSize(node)); 
   std::vector<Node> children;
   bool found_ones = false;
@@ -360,7 +360,7 @@ bool RewriteRule<XorZero>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<XorZero>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl;
   std::vector<Node> children;
   Node zero = utils::mkConst(utils::getSize(node), 0);
     
@@ -393,7 +393,7 @@ bool RewriteRule<BitwiseNotAnd>::applies(TNode node) {
 template<> inline
 Node RewriteRule<BitwiseNotAnd>::apply(TNode node) {
   Unreachable();
-  BVDebug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl;
   return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); 
 }
 
@@ -415,7 +415,7 @@ bool RewriteRule<BitwiseNotOr>::applies(TNode node) {
 template<> inline
 Node RewriteRule<BitwiseNotOr>::apply(TNode node) {
   Unreachable();
-  BVDebug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl;
   uint32_t size = utils::getSize(node);
   Integer ones = Integer(1).multiplyByPow2(size) - 1; 
   return utils::mkConst(BitVector(size, ones)); 
@@ -439,7 +439,7 @@ bool RewriteRule<XorNot>::applies(TNode node) {
 template<> inline
 Node RewriteRule<XorNot>::apply(TNode node) {
   Unreachable();
-  BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
   Node a = node[0][0];
   Node b = node[1][0]; 
   return utils::mkNode(kind::BITVECTOR_XOR, a, b); 
@@ -459,7 +459,7 @@ bool RewriteRule<NotXor>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<NotXor>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<NotXor>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<NotXor>(" << node << ")" << std::endl;
   std::vector<Node> children;
   TNode::iterator child_it = node[0].begin();
   children.push_back(utils::mkNode(kind::BITVECTOR_NOT, *child_it));
@@ -483,7 +483,7 @@ bool RewriteRule<NotIdemp>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<NotIdemp>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<XorIdemp>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<XorIdemp>(" << node << ")" << std::endl;
   return node[0][0];
 }
 
@@ -504,7 +504,7 @@ bool RewriteRule<LtSelf>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<LtSelf>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<LtSelf>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<LtSelf>(" << node << ")" << std::endl;
   return utils::mkFalse(); 
 }
 
@@ -523,7 +523,7 @@ bool RewriteRule<LteSelf>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<LteSelf>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<LteSelf>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<LteSelf>(" << node << ")" << std::endl;
   return utils::mkTrue(); 
 }
 
@@ -541,7 +541,7 @@ bool RewriteRule<UltZero>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<UltZero>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
   return utils::mkFalse(); 
 }
 
@@ -559,7 +559,7 @@ bool RewriteRule<UltSelf>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<UltSelf>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<UltSelf>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<UltSelf>(" << node << ")" << std::endl;
   return utils::mkFalse(); 
 }
 
@@ -578,7 +578,7 @@ bool RewriteRule<UleZero>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<UleZero>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl;
   return utils::mkNode(kind::EQUAL, node[0], node[1]); 
 }
 
@@ -596,7 +596,7 @@ bool RewriteRule<UleSelf>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<UleSelf>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<UleSelf>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<UleSelf>(" << node << ")" << std::endl;
   return utils::mkTrue(); 
 }
 
@@ -615,7 +615,7 @@ bool RewriteRule<ZeroUle>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<ZeroUle>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node << ")" << std::endl;
   return utils::mkTrue(); 
 }
 
@@ -638,7 +638,7 @@ bool RewriteRule<UleMax>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<UleMax>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<UleMax>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<UleMax>(" << node << ")" << std::endl;
   return utils::mkTrue(); 
 }
 
@@ -656,7 +656,7 @@ bool RewriteRule<NotUlt>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<NotUlt>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl;
   Node ult = node[0];
   Node a = ult[0];
   Node b = ult[1]; 
@@ -677,7 +677,7 @@ bool RewriteRule<NotUle>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<NotUle>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl;
   Node ult = node[0];
   Node a = ult[0];
   Node b = ult[1]; 
@@ -705,7 +705,7 @@ bool RewriteRule<MultPow2>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<MultPow2>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl;
 
   std::vector<Node>  children;
   unsigned exponent = 0; 
@@ -740,7 +740,7 @@ bool RewriteRule<NegIdemp>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<NegIdemp>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node << ")" << std::endl;
   return node[0][0]; 
 }
 
@@ -758,7 +758,7 @@ bool RewriteRule<UdivPow2>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<UdivPow2>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl;
   Node a = node[0];
   unsigned power = utils::isPow2Const(node[1]) -1;
 
@@ -782,7 +782,7 @@ bool RewriteRule<UdivOne>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<UdivOne>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl;
   return node[0]; 
 }
 
@@ -800,7 +800,7 @@ bool RewriteRule<UdivSelf>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<UdivSelf>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<UdivSelf>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<UdivSelf>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 1); 
 }
 
@@ -818,7 +818,7 @@ bool RewriteRule<UremPow2>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<UremPow2>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned power = utils::isPow2Const(node[1]) - 1;
   if (power == 0) {
@@ -843,7 +843,7 @@ bool RewriteRule<UremOne>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<UremOne>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<UremOne>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<UremOne>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 0); 
 }
 
@@ -861,7 +861,7 @@ bool RewriteRule<UremSelf>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<UremSelf>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<UremSelf>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<UremSelf>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 0); 
 }
 
@@ -881,7 +881,7 @@ bool RewriteRule<ShiftZero>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<ShiftZero>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node << ")" << std::endl;
   return node[0]; 
 }
 
@@ -909,7 +909,7 @@ bool RewriteRule<BBPlusNeg>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<BBPlusNeg>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node << ")" << std::endl;
 
   std::vector<Node> children;
   unsigned neg_count = 0; 
@@ -948,7 +948,7 @@ Node RewriteRule<BBPlusNeg>::apply(TNode node) {
 
 // template<> inline
 // Node RewriteRule<BBFactorOut>::apply(TNode node) {
-//   BVDebug("bv-rewrite") << "RewriteRule<BBFactorOut>(" << node << ")" << std::endl;
+//   Debug("bv-rewrite") << "RewriteRule<BBFactorOut>(" << node << ")" << std::endl;
 //   std::hash_set<TNode, TNodeHashFunction> factors;
 
 //   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
@@ -984,7 +984,7 @@ Node RewriteRule<BBPlusNeg>::apply(TNode node) {
 
 // template<> inline
 // Node RewriteRule<>::apply(TNode node) {
-//   BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
+//   Debug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
 //   return ; 
 // }
 
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 3f59be86d..7d851d0fb 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -24,12 +24,6 @@
 #include <sstream>
 #include "expr/node_manager.h"
 
-#ifdef CVC4_DEBUG
-#define BVDebug(x) Debug(x)
-#else
-#define BVDebug(x) if (false) Debug(x)
-#endif
-
 
 
 namespace CVC4 {