* added propagation as lemmas to TheoryBV:

   * modified BVMinisat to work incrementally
   * added more bv regressions 

14 files changed, 1502 insertions, 522 deletions

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index c0855122e..edaf8c154 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -106,7 +106,7 @@ void inline makeZero(Bits& bits, unsigned width) {
  * @return the carry-out
  */
 Node inline rippleCarryAdder(const Bits&a, const Bits& b, Bits& res, Node carry) {
-  Assert(res.size() == 0 && a.size() == b.size());
+  Assert(a.size() == b.size() && res.size() == 0);
   
   for (unsigned i = 0 ; i < a.size(); ++i) {
     Node sum = mkXor(mkXor(a[i], b[i]), carry);
@@ -119,6 +119,24 @@ Node inline rippleCarryAdder(const Bits&a, const Bits& b, Bits& res, Node carry)
   return carry;
 }
 
+inline void shiftAddMultiplier(const Bits&a, const Bits&b, Bits& res) {
+  
+  for (unsigned i = 0; i < a.size(); ++i) {
+    res.push_back(mkNode(kind::AND, b[0], a[i])); 
+  }
+  
+  for(unsigned k = 1; k < res.size(); ++k) {
+  Node carry_in = mkFalse();
+  Node carry_out;
+    for(unsigned j = 0; j < res.size() -k; ++j) {
+      Node aj = mkAnd(a[j], b[k]);
+      carry_out = mkOr(mkAnd(res[j+k], aj),
+                       mkAnd( mkXor(res[j+k], aj), carry_in));
+      res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in);
+      carry_in = carry_out; 
+    }
+  }
+}
 
 Node inline uLessThanBB(const Bits&a, const Bits& b, bool orEqual) {
   Assert (a.size() && b.size());
@@ -175,13 +193,13 @@ Node inline sLessThanBB(const Bits&a, const Bits& b, bool orEqual) {
 
 
 Node UndefinedAtomBBStrategy(TNode node, Bitblaster* bb) {
-  Trace("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
+  BVDebug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: "
                      << node.getKind() << "\n";
   Unreachable(); 
 }
 
 Node DefaultEqBB(TNode node, Bitblaster* bb) {
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   
   Assert(node.getKind() == kind::EQUAL);
   Bits lhs, rhs; 
@@ -203,7 +221,7 @@ Node DefaultEqBB(TNode node, Bitblaster* bb) {
 
 
 Node AdderUltBB(TNode node, Bitblaster* bb) {
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   Assert(node.getKind() == kind::BITVECTOR_ULT);
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -225,7 +243,7 @@ Node AdderUltBB(TNode node, Bitblaster* bb) {
 
 
 Node DefaultUltBB(TNode node, Bitblaster* bb) {
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   Assert(node.getKind() == kind::BITVECTOR_ULT);
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -238,7 +256,7 @@ Node DefaultUltBB(TNode node, Bitblaster* bb) {
 }
 
 Node DefaultUleBB(TNode node, Bitblaster* bb){
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   Assert(node.getKind() == kind::BITVECTOR_ULE);
   Bits a, b;
   
@@ -251,31 +269,31 @@ Node DefaultUleBB(TNode node, Bitblaster* bb){
 }
 
 Node DefaultUgtBB(TNode node, Bitblaster* bb){
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
 Node DefaultUgeBB(TNode node, Bitblaster* bb){
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
 
 // Node DefaultSltBB(TNode node, Bitblaster* bb){
-//   Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+//   BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 //   // shoudl be rewritten in terms of ult
 //   Unimplemented(); 
 // }
 
 // Node DefaultSleBB(TNode node, Bitblaster* bb){
-//   Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+//   BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 //   // shoudl be rewritten in terms of ule
 //   Unimplemented(); 
 // }
 
 
 Node DefaultSltBB(TNode node, Bitblaster* bb){
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -287,7 +305,7 @@ Node DefaultSltBB(TNode node, Bitblaster* bb){
 }
 
 Node DefaultSleBB(TNode node, Bitblaster* bb){
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
 
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -299,13 +317,13 @@ Node DefaultSleBB(TNode node, Bitblaster* bb){
 }
  
 Node DefaultSgtBB(TNode node, Bitblaster* bb){
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
 
 Node DefaultSgeBB(TNode node, Bitblaster* bb){
-  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  BVDebug("bitvector-bb") << "Bitblasting node " << node  << "\n";
   // should be rewritten 
   Unimplemented(); 
 }
@@ -314,7 +332,7 @@ Node DefaultSgeBB(TNode node, Bitblaster* bb){
 /// Term bitblasting strategies 
 
 void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) {
-  Trace("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
+  BVDebug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: "
                      << node.getKind() << "\n";
   Unreachable(); 
 }
@@ -327,12 +345,12 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
     bits.push_back(utils::mkBitOf(node, i));
   }
 
-  Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
-  Debug("bitvector-bb") << "                           with bits  " << toString(bits); 
+  BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
+  BVDebug("bitvector-bb") << "                           with bits  " << toString(bits); 
 }
 
 void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::CONST_BITVECTOR);
   Assert(bits.size() == 0);
   
@@ -345,12 +363,12 @@ void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
       bits.push_back(utils::mkTrue()); 
     }
   }
-  Debug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+  BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
 }
 
 
 void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_NOT);
   Assert(bits.size() == 0);
   Bits bv; 
@@ -359,7 +377,7 @@ void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n";
   Assert(bits.size() == 0);
   
   Assert (node.getKind() == kind::BITVECTOR_CONCAT);
@@ -373,64 +391,68 @@ void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) {
     }
   }
   Assert (bits.size() == utils::getSize(node)); 
-  Debug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
+  BVDebug("bitvector-bb") << "with  bits: " << toString(bits) << "\n"; 
 }
 
-
 void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
-
-  Assert(node.getNumChildren() == 2 &&
-         node.getKind() == kind::BITVECTOR_AND &&
+  BVDebug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n";
+  
+  Assert(node.getKind() == kind::BITVECTOR_AND &&
          bits.size() == 0);
   
-  Bits lhs, rhs;
-  bb->bbTerm(node[0], rhs);
-  bb->bbTerm(node[1], lhs);
-
-  Assert (lhs.size() == rhs.size()); 
-  for (unsigned i = 0; i < lhs.size(); ++i) {
-    bits.push_back(utils::mkAnd(lhs[i], rhs[i])); 
+  for(unsigned j = 0; j < utils::getSize(node); ++j) {
+    NodeBuilder<> andBuilder(kind::AND);
+    for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+      Bits current;
+      bb->bbTerm(node[i], current);
+      andBuilder << current[j];
+      Assert(utils::getSize(node) == current.size());
+    }
+    bits.push_back(andBuilder); 
   }
-
 }
 
 void DefaultOrBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n";
 
-  Assert(node.getNumChildren() == 2 &&
-         node.getKind() == kind::BITVECTOR_OR &&
+  Assert(node.getKind() == kind::BITVECTOR_OR &&
          bits.size() == 0);
   
-  Bits lhs, rhs;
-  bb->bbTerm(node[0], lhs);
-  bb->bbTerm(node[1], rhs);
-  Assert(lhs.size() == rhs.size()); 
-  
-  for (unsigned i = 0; i < lhs.size(); ++i) {
-    bits.push_back(utils::mkOr(lhs[i], rhs[i])); 
+  for(unsigned j = 0; j < utils::getSize(node); ++j) {
+    NodeBuilder<> orBuilder(kind::OR);
+    for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+      Bits current;
+      bb->bbTerm(node[i], current);
+      orBuilder << current[j];
+      Assert(utils::getSize(node) == current.size());
+    }
+    bits.push_back(orBuilder); 
   }
 }
 
 void DefaultXorBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n";
 
-  Assert(node.getNumChildren() == 2 &&
-         node.getKind() == kind::BITVECTOR_XOR &&
+  Assert(node.getKind() == kind::BITVECTOR_XOR &&
          bits.size() == 0);
   
-  Bits lhs, rhs;
-  bb->bbTerm(node[0], lhs);
-  bb->bbTerm(node[1], rhs);
-  Assert(lhs.size() == rhs.size()); 
-  
-  for (unsigned i = 0; i < lhs.size(); ++i) {
-    bits.push_back(utils::mkXor(lhs[i], rhs[i])); 
+  for(unsigned j = 0; j < utils::getSize(node); ++j) {
+    Bits first;
+    bb->bbTerm(node[0], first); 
+    Node bitj = first[j];
+    
+    for (unsigned i = 1; i < node.getNumChildren(); ++i) {
+      Bits current;
+      bb->bbTerm(node[i], current);
+      bitj = utils::mkNode(kind::XOR, bitj, current[j]);
+      Assert(utils::getSize(node) == current.size());
+    }
+    bits.push_back(bitj); 
   }
 }
 
 void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n";
 
   Assert(node.getNumChildren() == 2 &&
          node.getKind() == kind::BITVECTOR_XNOR &&
@@ -447,17 +469,17 @@ void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) {
 
 
 void DefaultNandBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultNorBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
+  BVDebug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n";
 
   Assert(getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP);
   Bits a, b;
@@ -475,51 +497,50 @@ void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
+  BVDebug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n";
   Assert(res.size() == 0 &&
          node.getKind() == kind::BITVECTOR_MULT);
-  Bits a, b;
-  bb->bbTerm(node[0], a);
-  bb->bbTerm(node[1], b);
 
-  // constructs a simple shift and add multiplier building the result in
-  // in res
-  
-  for (unsigned i = 0; i < a.size(); ++i) {
-    res.push_back(mkNode(kind::AND, b[0], a[i])); 
-  }
-  
-  for(unsigned k = 1; k < res.size(); ++k) {
-  Node carry_in = mkFalse();
-  Node carry_out;
-    for(unsigned j = 0; j < res.size() -k; ++j) {
-      Node aj = mkAnd(a[j], b[k]);
-      carry_out = mkOr(mkAnd(res[j+k], aj),
-                       mkAnd( mkXor(res[j+k], aj), carry_in));
-      res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in);
-      carry_in = carry_out; 
-    }
+  Bits newres; 
+  bb->bbTerm(node[0], res); 
+  for(unsigned i = 1; i < node.getNumChildren(); ++i) {
+    Bits current;
+    bb->bbTerm(node[i], current);
+    newres.clear(); 
+    // constructs a simple shift and add multiplier building the result
+    // in res
+    shiftAddMultiplier(res, current, newres);
+    res = newres;
   }
-  Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
 }
 
 void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaulPlusBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaulPlusBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_PLUS &&
          res.size() == 0);
 
-  Bits a, b;
-  bb->bbTerm(node[0], a);
-  bb->bbTerm(node[1], b); 
+  bb->bbTerm(node[0], res);
 
-  Assert(a.size() == b.size() && utils::getSize(node) == a.size());
-  rippleCarryAdder(a, b, res, mkFalse());
+  Bits newres;
+
+  for(unsigned i = 1; i < node.getNumChildren(); ++i) {
+    Bits current;
+    bb->bbTerm(node[i], current);
+    newres.clear(); 
+    rippleCarryAdder(res, current, newres, utils::mkFalse());
+    res = newres; 
+  }
+  
+  Assert(res.size() == utils::getSize(node));
 }
 
 
 void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefautSubBB bitblasting " << node << "\n";
-  Assert(node.getKind() == kind::BITVECTOR_SUB &&  bits.size() == 0);
+  BVDebug("bitvector-bb") << "theory::bv::DefautSubBB bitblasting " << node << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_SUB &&
+         node.getNumChildren() == 2 &&
+         bits.size() == 0);
     
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -534,7 +555,7 @@ void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefautNegBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefautNegBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_NEG);
   
   Bits a;
@@ -612,7 +633,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid
 }
 
 void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefautUdivBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefautUdivBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_UDIV &&  q.size() == 0);
 
   Bits a, b;
@@ -628,7 +649,7 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
 }
 
 void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefautUremBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefautUremBB bitblasting " << node << "\n";
   Assert(node.getKind() == kind::BITVECTOR_UREM &&  rem.size() == 0);
 
   Bits a, b;
@@ -645,23 +666,23 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
 
 
 void DefaultSdivBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultSremBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 void DefaultSmodBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
 
 void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node  << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node  << "\n";
   Assert (node.getKind() == kind::BITVECTOR_SHL &&
           res.size() == 0);
   Bits a, b;
@@ -688,11 +709,11 @@ void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) {
       }
     }
   }
-  Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
 }
 
 void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node  << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node  << "\n";
   Assert (node.getKind() == kind::BITVECTOR_LSHR &&
           res.size() == 0);
   Bits a, b;
@@ -719,12 +740,12 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) {
       }
     }
   }
-  Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
 }
 
 void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
 
-  Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node  << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node  << "\n";
   Assert (node.getKind() == kind::BITVECTOR_ASHR &&
           res.size() == 0);
   Bits a, b;
@@ -752,7 +773,7 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) {
       }
     }
   }
-  Debug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
+  BVDebug("bitvector-bb") << "with bits: " << toString(res)  << "\n";
 
 }
 
@@ -770,14 +791,14 @@ void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) {
   }
   Assert (bits.size() == high - low + 1);   
 
-  Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
-  Debug("bitvector-bb") << "                               with bits " << toString(bits); 
+  BVDebug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n";
+  BVDebug("bitvector-bb") << "                               with bits " << toString(bits); 
        
 }
 
 
 void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   // this should be rewritten 
   Unimplemented(); 
@@ -785,7 +806,7 @@ void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) {
 
 void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
 
-  Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node  << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node  << "\n";
  
   // this should be rewritten 
   Unimplemented();
@@ -793,7 +814,7 @@ void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
 }
 
 void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
-  Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node  << "\n";
+  BVDebug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node  << "\n";
 
   Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
           res_bits.size() == 0);
@@ -816,14 +837,14 @@ void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) {
 }
 
 void DefaultRotateRightBB (TNode node, Bits& res, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
 
   Unimplemented(); 
 }
 
 void DefaultRotateLeftBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Debug("bitvector") << "theory::bv:: Unimplemented kind "
+  BVDebug("bitvector") << "theory::bv:: Unimplemented kind "
                      << node.getKind() << "\n";
   Unimplemented(); 
 }
diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp
index 6f91335ce..f5c43688a 100644
--- a/src/theory/bv/bv_sat.cpp
+++ b/src/theory/bv/bv_sat.cpp
@@ -23,6 +23,7 @@
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
+#include "theory_bv_rewrite_rules_simplification.h"
 
 using namespace std;
 
@@ -57,7 +58,7 @@ Bitblaster::Bitblaster(context::Context* c) :
     d_assertedAtoms(c),
     d_statistics()
   {
-    d_satSolver = prop::SatSolverFactory::createMinisat();
+    d_satSolver = prop::SatSolverFactory::createMinisat(c);
     d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar());
 
     // initializing the bit-blasting strategies
@@ -83,7 +84,7 @@ void Bitblaster::bbAtom(TNode node) {
   }
 
   BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
-
+  ++d_statistics.d_numAtoms;
   // the bitblasted definition of the atom
   Node atom_bb = d_atomBBStrategies[node.getKind()](node, this);
   // asserting that the atom is true iff the definition holds
@@ -101,14 +102,78 @@ void Bitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
   BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
-  d_termBBStrategies[node.getKind()] (node, bits,this);
+  ++d_statistics.d_numTerms;
+
+  Node optimized = bbOptimize(node); 
+
+  // if we already bitblasted the optimized version 
+  if(hasBBTerm(optimized)) {
+    getBBTerm(optimized, bits);
+    // cache it as the same for this node
+    cacheTermDef(node, bits);
+    return; 
+  }
+  
+  d_termBBStrategies[optimized.getKind()] (optimized, bits,this);
   
-  Assert (bits.size() == utils::getSize(node)); 
+  Assert (bits.size() == utils::getSize(node) &&
+          bits.size() == utils::getSize(optimized));
+
+  if(optimized != node) {
+    cacheTermDef(optimized, bits);
+  }
   cacheTermDef(node, bits); 
 }
 
+Node Bitblaster::bbOptimize(TNode node) {
+  std::vector<Node> children;
+
+   if (node.getKind() == kind::BITVECTOR_PLUS) {
+    if (RewriteRule<BBPlusNeg>::applies(node)) {
+      Node res = RewriteRule<BBPlusNeg>::run<false>(node);
+      return res; 
+    }
+    //  if (RewriteRule<BBFactorOut>::applies(node)) {
+    //   Node res = RewriteRule<BBFactorOut>::run<false>(node);
+    //   return res; 
+    // } 
+
+  } else if (node.getKind() == kind::BITVECTOR_MULT) {
+    if (RewriteRule<MultPow2>::applies(node)) {
+      Node res = RewriteRule<MultPow2>::run<false>(node);
+      return res; 
+    }
+  }
+  
+  return node; 
+}
+
 /// Public methods
 
+void Bitblaster::addAtom(TNode atom) {
+  d_cnfStream->ensureLiteral(atom);
+  SatLiteral lit = d_cnfStream->getLiteral(atom);
+  d_satSolver->addMarkerLiteral(lit); 
+}
+bool Bitblaster::getPropagations(std::vector<TNode>& propagations) {
+  std::vector<SatLiteral> propagated_literals;
+  if (d_satSolver->getPropagations(propagated_literals)) {
+    for (unsigned i = 0; i < propagated_literals.size(); ++i) {
+      propagations.push_back(d_cnfStream->getNode(propagated_literals[i])); 
+    }
+    return true;
+  }
+  return false;
+}
+
+void Bitblaster::explainPropagation(TNode atom, std::vector<Node>& explanation) {
+  std::vector<SatLiteral> literal_explanation;
+  d_satSolver->explainPropagation(d_cnfStream->getLiteral(atom), literal_explanation);
+  for (unsigned i = 0; i < literal_explanation.size(); ++i) {
+    explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); 
+  }
+}
+
 /** 
  * Called from preregistration bitblasts the node
  * 
@@ -153,7 +218,7 @@ void Bitblaster::bitblast(TNode node) {
  * 
  */
  
-void Bitblaster::assertToSat(TNode lit) {
+bool Bitblaster::assertToSat(TNode lit, bool propagate) {
   // strip the not
   TNode atom; 
   if (lit.getKind() == kind::NOT) {
@@ -163,17 +228,22 @@ void Bitblaster::assertToSat(TNode lit) {
   }
   
   Assert (hasBBAtom(atom));
-  Node rewr_atom = Rewriter::rewrite(atom); 
+
   SatLiteral markerLit = d_cnfStream->getLiteral(atom);
 
   if(lit.getKind() == kind::NOT) {
     markerLit = ~markerLit;
   }
   
-  Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n";
-  Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal:   " << markerLit << "\n";  
+  BVDebug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n";
+  BVDebug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal:   " << markerLit << "\n";  
+
+  SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
 
   d_assertedAtoms.push_back(markerLit);
+
+  Assert(ret != prop::SAT_VALUE_UNKNOWN);
+  return ret == prop::SAT_VALUE_TRUE;
 }
 
 /** 
@@ -183,9 +253,9 @@ void Bitblaster::assertToSat(TNode lit) {
  * @return true for sat, and false for unsat
  */
  
-bool Bitblaster::solve() {
-  Trace("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; 
-  return SAT_VALUE_TRUE == d_satSolver->solve(d_assertedAtoms); 
+bool Bitblaster::solve(bool quick_solve) {
+  BVDebug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; 
+  return SAT_VALUE_TRUE == d_satSolver->solve(); 
 }
 
 void Bitblaster::getConflict(std::vector<TNode>& conflict) {
@@ -287,11 +357,15 @@ void Bitblaster::getBBTerm(TNode node, Bits& bits) {
 
 Bitblaster::Statistics::Statistics() :
   d_numTermClauses("theory::bv::NumberOfTermSatClauses", 0),
-  d_numAtomClauses("theory::bv::NumberOfAtomSatClauses", 0), 
+  d_numAtomClauses("theory::bv::NumberOfAtomSatClauses", 0),
+  d_numTerms("theory::bv::NumberOfBitblastedTerms", 0),
+  d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0), 
   d_bitblastTimer("theory::bv::BitblastTimer")
 {
   StatisticsRegistry::registerStat(&d_numTermClauses);
   StatisticsRegistry::registerStat(&d_numAtomClauses);
+  StatisticsRegistry::registerStat(&d_numTerms);
+  StatisticsRegistry::registerStat(&d_numAtoms);
   StatisticsRegistry::registerStat(&d_bitblastTimer);
 }
 
@@ -299,6 +373,8 @@ Bitblaster::Statistics::Statistics() :
 Bitblaster::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_numTermClauses);
   StatisticsRegistry::unregisterStat(&d_numAtomClauses);
+  StatisticsRegistry::unregisterStat(&d_numTerms);
+  StatisticsRegistry::unregisterStat(&d_numAtoms);
   StatisticsRegistry::unregisterStat(&d_bitblastTimer);
 }
 
diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h
index c0f3b75ed..647e4fe9f 100644
--- a/src/theory/bv/bv_sat.h
+++ b/src/theory/bv/bv_sat.h
@@ -97,6 +97,8 @@ class Bitblaster {
   void initAtomBBStrategies();
   void initTermBBStrategies(); 
 
+  // returns a node that might be easier to bitblast
+  Node bbOptimize(TNode node); 
   
   void bbAtom(TNode node);
   // division is bitblasted in terms of constraints
@@ -110,17 +112,20 @@ public:
 public:
   Bitblaster(context::Context* c); 
   ~Bitblaster();
-  void assertToSat(TNode node);
-  bool solve();
+  bool assertToSat(TNode node, bool propagate = true);
+  bool solve(bool quick_solve = false);
   void bitblast(TNode node);
   void getConflict(std::vector<TNode>& conflict); 
-
+  void addAtom(TNode atom); 
+  bool getPropagations(std::vector<TNode>& propagations);
+  void explainPropagation(TNode atom, std::vector<Node>& explanation);
 private:
 
   
   class Statistics {
   public:
-    IntStat  d_numTermClauses, d_numAtomClauses;
+    IntStat d_numTermClauses, d_numAtomClauses;
+    IntStat d_numTerms, d_numAtoms; 
     TimerStat d_bitblastTimer;
     Statistics();
     ~Statistics(); 
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 36d25de2a..6ef2cb0a9 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -28,16 +28,16 @@ constant CONST_BITVECTOR \
     "a fixed-width bit-vector constant"
 
 operator BITVECTOR_CONCAT 2: "bit-vector concatenation"
-operator BITVECTOR_AND 2 "bitwise and"
-operator BITVECTOR_OR 2 "bitwise or"
-operator BITVECTOR_XOR 2 "bitwise xor"
+operator BITVECTOR_AND 2: "bitwise and"
+operator BITVECTOR_OR 2: "bitwise or"
+operator BITVECTOR_XOR 2: "bitwise xor"
 operator BITVECTOR_NOT 1 "bitwise not"
 operator BITVECTOR_NAND 2 "bitwise nand"
 operator BITVECTOR_NOR 2 "bitwise nor"
 operator BITVECTOR_XNOR 2 "bitwise xnor"
 operator BITVECTOR_COMP 2 "equality comparison (returns one bit)"
-operator BITVECTOR_MULT 2 "bit-vector multiplication"
-operator BITVECTOR_PLUS 2 "bit-vector addition"
+operator BITVECTOR_MULT 2: "bit-vector multiplication"
+operator BITVECTOR_PLUS 2: "bit-vector addition"
 operator BITVECTOR_SUB 2 "bit-vector subtraction"
 operator BITVECTOR_NEG 1 "bit-vector unary negation"
 operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)"
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 45d99f9c9..e8e1aead6 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -32,12 +32,13 @@ using namespace std;
 using namespace CVC4::theory::bv::utils;
 
 TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation)
-  : Theory(THEORY_BV, c, u, out, valuation), 
+  : Theory(THEORY_BV, c, u, out, valuation),
     d_context(c),
     d_assertions(c),
     d_bitblaster(new Bitblaster(c) ),
-    d_statistics()
-  {
+    d_statistics(),
+    d_alreadyPropagatedSet(c)
+   {
     d_true = utils::mkTrue();
   }
 TheoryBV::~TheoryBV() {
@@ -61,35 +62,54 @@ TheoryBV::Statistics::~Statistics() {
 
 void TheoryBV::preRegisterTerm(TNode node) {
   BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
-  //marker literal: bitblast all terms before we start
-  //d_bitblaster->bitblast(node); 
+  if (node.getKind() == kind::EQUAL ||
+      node.getKind() == kind::BITVECTOR_ULT ||
+      node.getKind() == kind::BITVECTOR_ULE ||
+      node.getKind() == kind::BITVECTOR_SLT ||
+      node.getKind() == kind::BITVECTOR_SLE) {
+    d_bitblaster->bitblast(node);
+    d_bitblaster->addAtom(node); 
+  }
 }
 
 void TheoryBV::check(Effort e) {
-  if (fullEffort(e) && !done()) {
-    Trace("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl;
-    std::vector<TNode> assertions;
-      
+  if (e == EFFORT_STANDARD) {
+    BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; 
+    BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl;
     while (!done()) {
       TNode assertion = get();
-      Trace("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n"; 
-      d_bitblaster->bitblast(assertion); 
-      d_bitblaster->assertToSat(assertion); 
+      // make sure we do not assert things we propagated 
+      if (!hasBeenPropagated(assertion)) {
+        BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n"; 
+        bool ok = d_bitblaster->assertToSat(assertion, true);
+        if (!ok) {
+          std::vector<TNode> conflictAtoms;
+          d_bitblaster->getConflict(conflictAtoms);
+          d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size());
+          Node conflict = mkConjunction(conflictAtoms);
+          d_out->conflict(conflict);
+          BVDebug("bitvector") << "TheoryBV::check returns conflict: " <<conflict <<" \n ";
+          return;
+        }
+      }
     }
+  }
 
-    TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer); 
-    bool res = d_bitblaster->solve();
-    if (res == false) {
+  if (e == EFFORT_FULL) {
+    BVDebug("bitvector") << "TheoryBV::check " << e << "\n";
+    // in standard effort we only do boolean constraint propagation 
+    bool ok = d_bitblaster->solve(false);
+    if (!ok) {
       std::vector<TNode> conflictAtoms;
       d_bitblaster->getConflict(conflictAtoms);
       d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size());
-      
       Node conflict = mkConjunction(conflictAtoms);
       d_out->conflict(conflict);
-      Trace("bitvector") << "TheoryBV::check returns conflict. \n ";
+      BVDebug("bitvector") << "TheoryBV::check returns conflict: " <<conflict <<" \n ";
       return; 
     }
   }
+
 }
 
 
@@ -109,19 +129,56 @@ Node TheoryBV::getValue(TNode n) {
   }
 }
 
-Node TheoryBV::explain(TNode node) {
-  BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl;
+bool TheoryBV::hasBeenPropagated(TNode node) {
+  return d_alreadyPropagatedSet.count(node); 
+}
 
-  TNode equality = node.getKind() == kind::NOT ? node[0] : node;
-  Assert(equality.getKind() == kind::EQUAL);
-  Assert(0); 
-  return node; 
+void TheoryBV::propagate(Effort e) {
+  BVDebug("bitvector") << "TheoryBV::propagate() \n";
+
+  // get new propagations from the sat solver
+  std::vector<TNode> propagations; 
+  d_bitblaster->getPropagations(propagations);
+
+  // propagate the facts on the propagation queue
+  for (unsigned i = 0; i < propagations.size(); ++ i) {
+    TNode node = propagations[i];
+    BVDebug("bitvector") << "TheoryBV::propagate    " << node <<" \n";
+    if (d_valuation.getSatValue(node) == Node::null()) {
+      vector<Node> explanation;
+      d_bitblaster->explainPropagation(node, explanation);
+      if (explanation.size() == 0) {
+        d_out->lemma(node);
+      } else {
+        NodeBuilder<> nb(kind::OR);
+        nb << node;
+        for (unsigned i = 0; i < explanation.size(); ++ i) {
+          nb << explanation[i].notNode();
+        }
+        Node lemma = nb;
+        d_out->lemma(lemma);
+      }
+      d_alreadyPropagatedSet.insert(node);
+    }
+  }
 
 }
 
-// Node TheoryBV::preprocessTerm(TNode term) {
-//   return term; //d_staticEqManager.find(term);
-// }
+Node TheoryBV::explain(TNode n) {
+  BVDebug("bitvector") << "TheoryBV::explain node " <<  n <<"\n";
+  std::vector<Node> explanation;
+  d_bitblaster->explainPropagation(n, explanation);
+  Node exp;
+
+  if (explanation.size() == 0) {
+    return utils::mkTrue(); 
+  }
+  
+  exp = utils::mkAnd(explanation);
+  
+  BVDebug("bitvector") << "TheoryBV::explain with " <<  exp <<"\n";
+  return exp;
+}
 
 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   switch(in.getKind()) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 36ba17b52..d147c8bb5 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -24,6 +24,7 @@
 #include "theory/theory.h"
 #include "context/context.h"
 #include "context/cdlist.h"
+#include "context/cdhashset.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "util/stats.h"
 
@@ -41,7 +42,6 @@ class Bitblaster;
 
 class TheoryBV : public Theory {
 
-public:
 
 private:
 
@@ -54,7 +54,11 @@ private:
   /** Bitblaster */
   Bitblaster* d_bitblaster; 
   Node d_true;
-    
+
+  /** Context dependent set of atoms we already propagated */
+  context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;
+
+  bool hasBeenPropagated(TNode node); 
 public:
 
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
@@ -66,7 +70,7 @@ public:
 
   void check(Effort e);
 
-  void propagate(Effort e) { }
+  void propagate(Effort e);
 
   Node explain(TNode n);
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index b01a0646c..30437a76e 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -87,7 +87,9 @@ enum RewriteRuleId {
   EvalRotateLeft,
   EvalRotateRight,
   EvalNeg,
-  
+  EvalSlt,
+  EvalSle,
+
   /// simplification rules
   /// all of these rules decrease formula size
   ShlByConst,
@@ -136,12 +138,26 @@ enum RewriteRuleId {
   ExtractArith,
   ExtractArith2,
   DoubleNeg,
+  NegMult,
+  NegSub,
+  NegPlus,
   NotConcat,
   NotAnd, // not sure why this would help (not done)
   NotOr,  // not sure why this would help (not done)
-  NotXor // not sure why this would help (not done)
+  NotXor, // not sure why this would help (not done)
+  FlattenAssocCommut,
+  PlusCombineLikeTerms,
+  MultSimplify,
+  MultDistribConst,
+  AndSimplify,
+  OrSimplify,
+  XorSimplify,
+
+  // rules to simplify bitblasting
+  BBPlusNeg
  };
 
+
 inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   switch (ruleId) {
   case EmptyRule:           out << "EmptyRule";           return out;
@@ -183,6 +199,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case EvalAshr :           out << "EvalAshr";            return out;
   case EvalUlt :            out << "EvalUlt";             return out;
   case EvalUle :            out << "EvalUle";             return out;
+  case EvalSlt :            out << "EvalSlt";             return out;
+  case EvalSle :            out << "EvalSle";             return out; 
   case EvalExtract :        out << "EvalExtract";         return out;
   case EvalSignExtend :     out << "EvalSignExtend";      return out;
   case EvalRotateLeft :     out << "EvalRotateLeft";      return out;
@@ -241,6 +259,17 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case SignExtendEliminate :            out << "SignExtendEliminate";             return out;
   case NotIdemp :                  out << "NotIdemp"; return out;
   case UleSelf:                    out << "UleSelf"; return out; 
+  case FlattenAssocCommut:     out << "FlattenAssocCommut"; return out; 
+  case PlusCombineLikeTerms: out << "PlusCombineLikeTerms"; return out;
+  case MultSimplify: out << "MultSimplify"; return out;
+  case MultDistribConst: out << "MultDistribConst"; return out;
+  case NegMult : out << "NegMult"; return out;
+  case NegSub : out << "NegSub"; return out;
+  case AndSimplify : out << "AndSimplify"; return out;
+  case OrSimplify : out << "OrSimplify"; return out;
+  case XorSimplify : out << "XorSimplify"; return out;
+  case NegPlus : out << "NegPlus"; return out;
+  case BBPlusNeg : out << "BBPlusNeg"; return out; 
   default:
     Unreachable();
   }
@@ -346,6 +375,8 @@ struct AllRewriteRules {
   RewriteRule<SgtEliminate>             rule12;
   RewriteRule<UgeEliminate>             rule13;
   RewriteRule<SgeEliminate>             rule14;
+  RewriteRule<NegMult>              rule15;
+  RewriteRule<NegSub>               rule16;
   RewriteRule<RepeatEliminate>      rule17;
   RewriteRule<RotateLeftEliminate>  rule18;
   RewriteRule<RotateRightEliminate> rule19;
@@ -359,8 +390,10 @@ struct AllRewriteRules {
   RewriteRule<EvalOr>               rule27;
   RewriteRule<EvalXor>              rule28;
   RewriteRule<EvalNot>              rule29;
+  RewriteRule<EvalSlt>              rule30;
   RewriteRule<EvalMult>             rule31;
   RewriteRule<EvalPlus>             rule32;
+  RewriteRule<XorSimplify>          rule33;
   RewriteRule<EvalUdiv>             rule34;
   RewriteRule<EvalUrem>             rule35;
   RewriteRule<EvalShl>              rule36;
@@ -368,6 +401,7 @@ struct AllRewriteRules {
   RewriteRule<EvalAshr>             rule38;
   RewriteRule<EvalUlt>              rule39;
   RewriteRule<EvalUle>              rule40;
+  RewriteRule<EvalSle>              rule41;
   RewriteRule<EvalExtract>          rule43;
   RewriteRule<EvalSignExtend>       rule44;
   RewriteRule<EvalRotateLeft>       rule45;
@@ -428,14 +462,22 @@ struct AllRewriteRules {
   RewriteRule<SignExtendEliminate> rule101;
   RewriteRule<NotIdemp> rule102;
   RewriteRule<UleSelf> rule103;
+  RewriteRule<FlattenAssocCommut> rule104;
+  RewriteRule<PlusCombineLikeTerms> rule105;
+  RewriteRule<MultSimplify> rule106;
+  RewriteRule<MultDistribConst> rule107;
+  RewriteRule<AndSimplify> rule108;
+  RewriteRule<OrSimplify> rule109;
+  RewriteRule<NegPlus> rule110;
+  RewriteRule<BBPlusNeg> rule111;
 };
 
-template<>
+template<> inline
 bool RewriteRule<EmptyRule>::applies(Node node) {
   return false;
 }
 
-template<>
+template<> inline
 Node RewriteRule<EmptyRule>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EmptyRule> for " << node.getKind() <<"\n"; 
   Unreachable();
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 1dc053b5d..da3ef4485 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -28,13 +28,13 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-template<>
+template<> inline
 bool RewriteRule<EvalAnd>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_AND &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalAnd>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalAnd>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -44,13 +44,13 @@ Node RewriteRule<EvalAnd>::apply(Node node) {
   return utils::mkConst(res);
 }
 
-template<>
+template<> inline
 bool RewriteRule<EvalOr>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_OR &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalOr>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalOr>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -60,13 +60,13 @@ Node RewriteRule<EvalOr>::apply(Node node) {
   return utils::mkConst(res);
 }
 
-template<>
+template<> inline
 bool RewriteRule<EvalXor>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_XOR &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalXor>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalXor>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -76,13 +76,13 @@ Node RewriteRule<EvalXor>::apply(Node node) {
   return utils::mkConst(res);
 }
 
-// template<>
+// template<> inline
 // bool RewriteRule<EvalXnor>::applies(Node node) {
 //   return (node.getKind() == kind::BITVECTOR_XNOR &&
 //           utils::isBVGroundTerm(node));
 // }
 
-// template<>
+// template<> inline
 // Node RewriteRule<EvalXnor>::apply(Node node) {
 //   BVDebug("bv-rewrite") << "RewriteRule<EvalXnor>(" << node << ")" << std::endl;
 //   BitVector a = node[0].getConst<BitVector>();
@@ -91,13 +91,13 @@ Node RewriteRule<EvalXor>::apply(Node node) {
   
 //   return utils::mkConst(res);
 // }
-template<>
+template<> inline
 bool RewriteRule<EvalNot>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_NOT &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalNot>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalNot>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -105,13 +105,13 @@ Node RewriteRule<EvalNot>::apply(Node node) {
   return utils::mkConst(res);
 }
 
-// template<>
+// template<> inline
 // bool RewriteRule<EvalComp>::applies(Node node) {
 //   return (node.getKind() == kind::BITVECTOR_COMP &&
 //           utils::isBVGroundTerm(node));
 // }
 
-// template<>
+// template<> inline
 // Node RewriteRule<EvalComp>::apply(Node node) {
 //   BVDebug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl;
 //   BitVector a = node[0].getConst<BitVector>();
@@ -126,13 +126,13 @@ Node RewriteRule<EvalNot>::apply(Node node) {
 //   return utils::mkConst(res);
 // }
 
-template<>
+template<> inline
 bool RewriteRule<EvalMult>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_MULT &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalMult>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalMult>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -142,13 +142,13 @@ Node RewriteRule<EvalMult>::apply(Node node) {
   return utils::mkConst(res);
 }
 
-template<>
+template<> inline
 bool RewriteRule<EvalPlus>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_PLUS &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalPlus>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalPlus>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -158,13 +158,13 @@ Node RewriteRule<EvalPlus>::apply(Node node) {
   return utils::mkConst(res);
 }
 
-// template<>
+// template<> inline
 // bool RewriteRule<EvalSub>::applies(Node node) {
 //   return (node.getKind() == kind::BITVECTOR_SUB &&
 //           utils::isBVGroundTerm(node));
 // }
 
-// template<>
+// template<> inline
 // Node RewriteRule<EvalSub>::apply(Node node) {
 //   BVDebug("bv-rewrite") << "RewriteRule<EvalSub>(" << node << ")" << std::endl;
 //   BitVector a = node[0].getConst<BitVector>();
@@ -173,13 +173,13 @@ Node RewriteRule<EvalPlus>::apply(Node node) {
   
 //   return utils::mkConst(res);
 // }
-template<>
+template<> inline
 bool RewriteRule<EvalNeg>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_NEG &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalNeg>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalNeg>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -187,13 +187,13 @@ Node RewriteRule<EvalNeg>::apply(Node node) {
   
   return utils::mkConst(res);
 }
-template<>
+template<> inline
 bool RewriteRule<EvalUdiv>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_UDIV &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalUdiv>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -202,13 +202,13 @@ Node RewriteRule<EvalUdiv>::apply(Node node) {
   
   return utils::mkConst(res);
 }
-template<>
+template<> inline
 bool RewriteRule<EvalUrem>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_UREM &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalUrem>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -217,13 +217,13 @@ Node RewriteRule<EvalUrem>::apply(Node node) {
   return utils::mkConst(res);
 }
 
-template<>
+template<> inline
 bool RewriteRule<EvalShl>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_SHL &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalShl>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalShl>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -233,13 +233,13 @@ Node RewriteRule<EvalShl>::apply(Node node) {
   return utils::mkConst(res);
 }
 
-template<>
+template<> inline
 bool RewriteRule<EvalLshr>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_LSHR &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalLshr>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalLshr>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -249,13 +249,13 @@ Node RewriteRule<EvalLshr>::apply(Node node) {
   return utils::mkConst(res);
 }
 
-template<>
+template<> inline
 bool RewriteRule<EvalAshr>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_ASHR &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalAshr>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalAshr>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -265,13 +265,13 @@ Node RewriteRule<EvalAshr>::apply(Node node) {
   return utils::mkConst(res);
 }
 
-template<>
+template<> inline
 bool RewriteRule<EvalUlt>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_ULT &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalUlt>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUlt>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -283,32 +283,32 @@ Node RewriteRule<EvalUlt>::apply(Node node) {
   return utils::mkFalse();
 }
 
-// template<>
-// bool RewriteRule<EvalSlt>::applies(Node node) {
-//   return (node.getKind() == kind::BITVECTOR_SLT &&
-//           utils::isBVGroundTerm(node));
-// }
+template<> inline
+bool RewriteRule<EvalSlt>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_SLT &&
+          utils::isBVGroundTerm(node));
+}
 
-// template<>
-// Node RewriteRule<EvalSlt>::apply(Node node) {
-//   BVDebug("bv-rewrite") << "RewriteRule<EvalSlt>(" << node << ")" << std::endl;
-//   BitVector a = node[0].getConst<BitVector>();
-//   BitVector b = node[1].getConst<BitVector>();
+template<> inline
+Node RewriteRule<EvalSlt>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<EvalSlt>(" << node << ")" << std::endl;
+  BitVector a = node[0].getConst<BitVector>();
+  BitVector b = node[1].getConst<BitVector>();
 
-//   if (a.signedLessThan(b)) {
-//     return utils::mkTrue();
-//   }
-//   return utils::mkFalse();
+  if (a.signedLessThan(b)) {
+    return utils::mkTrue();
+  }
+  return utils::mkFalse();
 
-// }
+}
 
-template<>
+template<> inline
 bool RewriteRule<EvalUle>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_ULE &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalUle>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUle>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -320,31 +320,31 @@ Node RewriteRule<EvalUle>::apply(Node node) {
   return utils::mkFalse();
 }
 
-// template<>
-// bool RewriteRule<EvalSle>::applies(Node node) {
-//   return (node.getKind() == kind::BITVECTOR_SLE &&
-//           utils::isBVGroundTerm(node));
-// }
+template<> inline
+bool RewriteRule<EvalSle>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_SLE &&
+          utils::isBVGroundTerm(node));
+}
 
-// template<>
-// Node RewriteRule<EvalSle>::apply(Node node) {
-//   BVDebug("bv-rewrite") << "RewriteRule<EvalSle>(" << node << ")" << std::endl;
-//   BitVector a = node[0].getConst<BitVector>();
-//   BitVector b = node[1].getConst<BitVector>();
+template<> inline
+Node RewriteRule<EvalSle>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<EvalSle>(" << node << ")" << std::endl;
+  BitVector a = node[0].getConst<BitVector>();
+  BitVector b = node[1].getConst<BitVector>();
 
-//   if (a.signedLessThanEq(b)) {
-//     return utils::mkTrue(); 
-//   }
-//   return utils::mkFalse();
-// }
+  if (a.signedLessThanEq(b)) {
+    return utils::mkTrue(); 
+  }
+  return utils::mkFalse();
+}
 
-template<>
+template<> inline
 bool RewriteRule<EvalExtract>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalExtract>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalExtract>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -356,13 +356,13 @@ Node RewriteRule<EvalExtract>::apply(Node node) {
 }
 
 
-template<>
+template<> inline
 bool RewriteRule<EvalConcat>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_CONCAT &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalConcat>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalConcat>(" << node << ")" << std::endl;
   unsigned num = node.getNumChildren();
@@ -374,13 +374,13 @@ Node RewriteRule<EvalConcat>::apply(Node node) {
   return utils::mkConst(res);
 }
 
-template<>
+template<> inline
 bool RewriteRule<EvalSignExtend>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalSignExtend>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalSignExtend>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
@@ -390,13 +390,13 @@ Node RewriteRule<EvalSignExtend>::apply(Node node) {
   return utils::mkConst(res);
 }
 
-template<>
+template<> inline
 bool RewriteRule<EvalEquals>::applies(Node node) {
   return (node.getKind() == kind::EQUAL &&
           utils::isBVGroundTerm(node));
 }
 
-template<>
+template<> inline
 Node RewriteRule<EvalEquals>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalEquals>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index 3240ef5f3..f3d28072e 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -28,12 +28,12 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-template<>
+template<> inline
 bool RewriteRule<ConcatFlatten>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_CONCAT);
 }
 
-template<>
+template<> inline
 Node RewriteRule<ConcatFlatten>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl;
   NodeBuilder<> result(kind::BITVECTOR_CONCAT);
@@ -54,12 +54,12 @@ Node RewriteRule<ConcatFlatten>::apply(Node node) {
   return resultNode;
 }
 
-template<>
+template<> inline
 bool RewriteRule<ConcatExtractMerge>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_CONCAT);
 }
 
-template<>
+template<> inline
 Node RewriteRule<ConcatExtractMerge>::apply(Node node) {
 
   BVDebug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl;
@@ -115,12 +115,12 @@ Node RewriteRule<ConcatExtractMerge>::apply(Node node) {
   return utils::mkConcat(mergedExtracts);
 }
 
-template<>
+template<> inline
 bool RewriteRule<ConcatConstantMerge>::applies(Node node) {
   return node.getKind() == kind::BITVECTOR_CONCAT;
 }
 
-template<>
+template<> inline
 Node RewriteRule<ConcatConstantMerge>::apply(Node node) {
 
   BVDebug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl;
@@ -157,7 +157,7 @@ Node RewriteRule<ConcatConstantMerge>::apply(Node node) {
   return utils::mkConcat(mergedConstants);
 }
 
-template<>
+template<> inline
 bool RewriteRule<ExtractWhole>::applies(Node node) {
   if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
   unsigned length = utils::getSize(node[0]);
@@ -168,20 +168,20 @@ bool RewriteRule<ExtractWhole>::applies(Node node) {
   return true;
 }
 
-template<>
+template<> inline
 Node RewriteRule<ExtractWhole>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl;
   return node[0];
 }
 
-template<>
+template<> inline
 bool RewriteRule<ExtractConstant>::applies(Node node) {
   if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
   if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
   return true;
 }
 
-template<>
+template<> inline
 Node RewriteRule<ExtractConstant>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl;
   Node child = node[0];
@@ -189,7 +189,7 @@ Node RewriteRule<ExtractConstant>::apply(Node node) {
   return utils::mkConst(childValue.extract(utils::getExtractHigh(node), utils::getExtractLow(node)));
 }
 
-template<>
+template<> inline
 bool RewriteRule<ExtractConcat>::applies(Node node) {
   //BVDebug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
   if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
@@ -197,7 +197,7 @@ bool RewriteRule<ExtractConcat>::applies(Node node) {
   return true;
 }
 
-template<>
+template<> inline
 Node RewriteRule<ExtractConcat>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
   int extract_high = utils::getExtractHigh(node);
@@ -223,14 +223,14 @@ Node RewriteRule<ExtractConcat>::apply(Node node) {
   return utils::mkConcat(resultChildren);
 }
 
-template<>
+template<> inline
 bool RewriteRule<ExtractExtract>::applies(Node node) {
   if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
   if (node[0].getKind() != kind::BITVECTOR_EXTRACT) return false;
   return true;
 }
 
-template<>
+template<> inline
 Node RewriteRule<ExtractExtract>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl;
 
@@ -244,7 +244,7 @@ Node RewriteRule<ExtractExtract>::apply(Node node) {
   return result;
 }
 
-template<>
+template<> inline
 bool RewriteRule<FailEq>::applies(Node node) {
   //BVDebug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
   if (node.getKind() != kind::EQUAL) return false;
@@ -253,29 +253,29 @@ bool RewriteRule<FailEq>::applies(Node node) {
   return node[0] != node[1];
 }
 
-template<>
+template<> inline
 Node RewriteRule<FailEq>::apply(Node node) {
   return utils::mkFalse();
 }
 
-template<>
+template<> inline
 bool RewriteRule<SimplifyEq>::applies(Node node) {
   if (node.getKind() != kind::EQUAL) return false;
   return node[0] == node[1];
 }
 
-template<>
+template<> inline
 Node RewriteRule<SimplifyEq>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl;
   return utils::mkTrue();
 }
 
-template<>
+template<> inline
 bool RewriteRule<ReflexivityEq>::applies(Node node) {
   return (node.getKind() == kind::EQUAL && node[0] < node[1]);
 }
 
-template<>
+template<> inline
 Node RewriteRule<ReflexivityEq>::apply(Node node) {
   BVDebug("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 4e974881c..5587e25eb 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -33,7 +33,7 @@ namespace bv {
  *   (x bvop y) [i:j] ==> x[i:j] bvop y[i:j]
  *  where bvop is bvand,bvor, bvxor
  */
-template<>
+template<> inline
 bool RewriteRule<ExtractBitwise>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
           (node[0].getKind() == kind::BITVECTOR_AND ||
@@ -41,7 +41,7 @@ bool RewriteRule<ExtractBitwise>::applies(Node node) {
            node[0].getKind() == kind::BITVECTOR_XOR ));
 }
 
-template<>
+template<> inline
 Node RewriteRule<ExtractBitwise>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractBitwise>(" << node << ")" << std::endl;
   unsigned high = utils::getExtractHigh(node);
@@ -57,13 +57,13 @@ Node RewriteRule<ExtractBitwise>::apply(Node node) {
  *
  *  (~ a) [i:j] ==> ~ (a[i:j])
  */
-template<>
+template<> inline
 bool RewriteRule<ExtractNot>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
           node[0].getKind() == kind::BITVECTOR_NOT);
 }
 
-template<>
+template<> inline
 Node RewriteRule<ExtractNot>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractNot>(" << node << ")" << std::endl;
   unsigned low = utils::getExtractLow(node);
@@ -78,7 +78,7 @@ Node RewriteRule<ExtractNot>::apply(Node node) {
  * (a bvop b) [k:0] ==> (a[k:0] bvop b[k:0])
  */
 
-template<>
+template<> inline
 bool RewriteRule<ExtractArith>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
           utils::getExtractLow(node) == 0 &&
@@ -86,7 +86,7 @@ bool RewriteRule<ExtractArith>::applies(Node node) {
            node[0].getKind() == kind::BITVECTOR_MULT));
 }
 
-template<>
+template<> inline
 Node RewriteRule<ExtractArith>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractArith>(" << node << ")" << std::endl;
   unsigned low = utils::getExtractLow(node);
@@ -107,14 +107,14 @@ Node RewriteRule<ExtractArith>::apply(Node node) {
  */
 
 // careful not to apply in a loop 
-template<>
+template<> inline
 bool RewriteRule<ExtractArith2>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
           (node[0].getKind() == kind::BITVECTOR_PLUS ||
            node[0].getKind() == kind::BITVECTOR_MULT));
 }
 
-template<>
+template<> inline
 Node RewriteRule<ExtractArith2>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractArith2>(" << node << ")" << std::endl;
   unsigned low = utils::getExtractLow(node);
@@ -128,13 +128,570 @@ Node RewriteRule<ExtractArith2>::apply(Node node) {
   return utils::mkExtract(a_op_b, high, low); 
 }
 
+template<> inline
+bool RewriteRule<FlattenAssocCommut>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_PLUS ||
+          node.getKind() == kind::BITVECTOR_MULT ||
+          node.getKind() == kind::BITVECTOR_OR ||
+          node.getKind() == kind::BITVECTOR_XOR ||
+          node.getKind() == kind::BITVECTOR_AND);
+}
+
+
+template<> inline
+Node RewriteRule<FlattenAssocCommut>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl;
+  std::vector<Node> processingStack;
+  processingStack.push_back(node);
+  std::vector<Node> children;
+  Kind kind = node.getKind(); 
+  
+  while (! processingStack.empty()) {
+    TNode current = processingStack.back();
+    processingStack.pop_back();
+
+    // flatten expression
+    if (current.getKind() == kind) {
+      for (unsigned i = 0; i < current.getNumChildren(); ++i) {
+        processingStack.push_back(current[i]);
+      }
+    } else {
+      children.push_back(current); 
+    }
+  }
+  return utils::mkSortedNode(kind, children); 
+}
+
+static inline void addToCoefMap(std::map<Node, BitVector>& map,
+                                TNode term, const BitVector& coef) {
+  if (map.find(term) != map.end()) {
+    map[term] = map[term] + coef; 
+  } else {
+    map[term] = coef;
+  }
+}
+
+
+template<> inline
+bool RewriteRule<PlusCombineLikeTerms>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_PLUS);
+}
+
+template<> inline
+Node RewriteRule<PlusCombineLikeTerms>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<PlusCombineLikeTerms>(" << node << ")" << std::endl;
+  unsigned size = utils::getSize(node); 
+  BitVector constSum(size, (unsigned)0); 
+  std::map<Node, BitVector> factorToCoefficient;
+
+  // combine like-terms
+  for(unsigned i= 0; i < node.getNumChildren(); ++i) {
+    TNode current = node[i];
+    
+    // look for c * x, where c is a constant
+    if (current.getKind() == kind::BITVECTOR_MULT &&
+        (current[0].getKind() == kind::CONST_BITVECTOR ||
+         current[1].getKind() == kind::CONST_BITVECTOR)) {
+      // if we are multiplying by a constant
+      BitVector coeff;
+      TNode term;
+      // figure out which part is the constant
+      if (current[0].getKind() == kind::CONST_BITVECTOR) {
+        coeff = current[0].getConst<BitVector>();
+        term = current[1];
+      } else {
+        coeff = current[1].getConst<BitVector>();
+        term = current[0];
+      }
+      if(term.getKind() == kind::BITVECTOR_SUB) {
+        TNode a = term[0];
+        TNode b = term[1];
+        addToCoefMap(factorToCoefficient, a, coeff);
+        addToCoefMap(factorToCoefficient, b, -coeff); 
+      }
+      else if(term.getKind() == kind::BITVECTOR_NEG) {
+        addToCoefMap(factorToCoefficient, term[0], -BitVector(size, coeff));
+      }
+      else {
+        addToCoefMap(factorToCoefficient, term, coeff);
+      }
+    }
+    else if (current.getKind() == kind::BITVECTOR_SUB) {
+      // turn into a + (-1)*b 
+      addToCoefMap(factorToCoefficient, current[0], BitVector(size, (unsigned)1)); 
+      addToCoefMap(factorToCoefficient, current[1], -BitVector(size, (unsigned)1)); 
+    }
+    else if (current.getKind() == kind::BITVECTOR_NEG) {
+      addToCoefMap(factorToCoefficient, current[0], -BitVector(size, (unsigned)1)); 
+    }
+    else if (current.getKind() == kind::CONST_BITVECTOR) {
+      BitVector constValue = current.getConst<BitVector>(); 
+      constSum = constSum + constValue;
+    }
+    else {
+      // store as 1 * current
+      addToCoefMap(factorToCoefficient, current, BitVector(size, (unsigned)1)); 
+    }
+  }
+    
+  std::vector<Node> children; 
+  if ( constSum!= BitVector(size, (unsigned)0)) {
+    children.push_back(utils::mkConst(constSum)); 
+  }
+
+  // construct result 
+  std::map<Node, BitVector>::const_iterator it = factorToCoefficient.begin();
+  
+  for (; it != factorToCoefficient.end(); ++it) {
+    BitVector bv_coeff = it->second;
+    TNode term = it->first;
+    if(bv_coeff == BitVector(size, (unsigned)0)) {
+      continue;
+    }
+    else if (bv_coeff == BitVector(size, (unsigned)1)) {
+      children.push_back(term); 
+    }
+    else if (bv_coeff == -BitVector(size, (unsigned)1)) {
+      // avoid introducing an extra multiplication
+      children.push_back(utils::mkNode(kind::BITVECTOR_NEG, term)); 
+    }
+    else {
+      Node coeff = utils::mkConst(bv_coeff);
+      Node product = utils::mkSortedNode(kind::BITVECTOR_MULT, coeff, term); 
+      children.push_back(product); 
+    }
+  }
+
+  if(children.size() == 0) {
+    return utils::mkConst(size, (unsigned)0); 
+  }
+  
+  return utils::mkSortedNode(kind::BITVECTOR_PLUS, children);
+}
+
+
+template<> inline
+bool RewriteRule<MultSimplify>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_MULT);
+}
+
+template<> inline
+Node RewriteRule<MultSimplify>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<MultSimplify>(" << node << ")" << std::endl;
+  unsigned size = utils::getSize(node); 
+  BitVector constant(size, Integer(1));
+
+  std::vector<Node> children; 
+  for(unsigned i = 0; i < node.getNumChildren(); ++i) {
+    TNode current = node[i];
+    if (current.getKind() == kind::CONST_BITVECTOR) {
+      BitVector value = current.getConst<BitVector>();
+      if(value == BitVector(size, (unsigned) 0)) {
+        return utils::mkConst(size, 0); 
+      }
+      constant = constant * current.getConst<BitVector>();
+    } else {
+      children.push_back(current); 
+    }
+  }
+
+
+  if(constant != BitVector(size, (unsigned)1)) {
+    children.push_back(utils::mkConst(constant)); 
+  }
+
+  
+  if(children.size() == 0) {
+    return utils::mkConst(size, (unsigned)1); 
+  }
+
+  return utils::mkSortedNode(kind::BITVECTOR_MULT, children); 
+}
+
+template<> inline
+bool RewriteRule<MultDistribConst>::applies(Node node) {
+  if (node.getKind() != kind::BITVECTOR_MULT)
+    return false;
+
+  TNode factor;
+  if (node[0].getKind() == kind::CONST_BITVECTOR) {
+    factor = node[1];
+  } else if (node[1].getKind() == kind::CONST_BITVECTOR) {
+    factor = node[0];
+  } else {
+    return false; 
+  }
+  
+  return (factor.getKind() == kind::BITVECTOR_PLUS ||
+          factor.getKind() == kind::BITVECTOR_SUB ||
+          factor.getKind() == kind::BITVECTOR_NEG); 
+}
+
+template<> inline
+Node RewriteRule<MultDistribConst>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<MultDistribConst>(" << node << ")" << std::endl;
+
+  TNode constant;
+  TNode factor;
+  if (node[0].getKind() == kind::CONST_BITVECTOR) {
+    constant = node[0];
+    factor = node[1]; 
+  } else {
+  Assert(node[1].getKind() == kind::CONST_BITVECTOR);
+  constant = node[1];
+  factor = node[0];
+  }
+
+  if (factor.getKind() == kind::BITVECTOR_NEG) {
+    // push negation on the constant part
+    BitVector const_bv = constant.getConst<BitVector>();
+    return utils::mkSortedNode(kind::BITVECTOR_MULT,
+                               utils::mkConst(-const_bv),
+                               factor[0]); 
+  }
+
+  std::vector<Node> children;
+  for(unsigned i = 0; i < factor.getNumChildren(); ++i) {
+    children.push_back(utils::mkSortedNode(kind::BITVECTOR_MULT, constant, factor[i])); 
+  }
+  
+  return utils::mkSortedNode(factor.getKind(), children); 
+                              
+}
+
+
+/**
+ * -(c * expr) ==> (-c * expr)
+ * where c is a constant
+ */
+template<> inline
+bool RewriteRule<NegMult>::applies(Node node) {
+  if(node.getKind()!= kind::BITVECTOR_NEG ||
+     node[0].getKind() != kind::BITVECTOR_MULT) {
+    return false; 
+  }
+  TNode mult = node[0]; 
+  for (unsigned i = 0; i < mult.getNumChildren(); ++i) {
+    if (mult[i].getKind() == kind::CONST_BITVECTOR) {
+      return true; 
+    }
+  } 
+  return false; 
+}
+
+template<> inline
+Node RewriteRule<NegMult>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl;
+  TNode mult = node[0];
+  std::vector<Node> children;
+  bool has_const = false; 
+  for(unsigned i = 0; i < mult.getNumChildren(); ++i) {
+    if(mult[i].getKind() == kind::CONST_BITVECTOR) {
+      Assert(has_const == false);
+      has_const = true; 
+      BitVector bv = mult[i].getConst<BitVector>();
+      children.push_back(utils::mkConst(-bv)); 
+    } else {
+      children.push_back(mult[i]); 
+    }
+  }
+  Assert (has_const); 
+  return utils::mkSortedNode(kind::BITVECTOR_MULT, children);
+}
+
+template<> inline
+bool RewriteRule<NegSub>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_NEG &&
+          node[0].getKind() == kind::BITVECTOR_SUB);
+}
+
+template<> inline
+Node RewriteRule<NegSub>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<NegSub>(" << node << ")" << std::endl;
+  return utils::mkNode(kind::BITVECTOR_SUB, node[0][1], node[0][0]);
+}
+
+template<> inline
+bool RewriteRule<NegPlus>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_NEG &&
+          node[0].getKind() == kind::BITVECTOR_PLUS);
+}
+
+template<> inline
+Node RewriteRule<NegPlus>::apply(Node node) {
+  BVDebug("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])); 
+  }
+  return utils::mkSortedNode(kind::BITVECTOR_PLUS, children);
+}
+
+
+
+
+struct Count {
+  unsigned pos;
+  unsigned neg;
+  Count() : pos(0), neg(0) {}
+  Count(unsigned p, unsigned n):
+    pos(p),
+    neg(n)
+  {}
+};
+
+inline static void insert(std::hash_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) {
+  if(map.find(node) == map.end()) {
+    Count c = neg? Count(0,1) : Count(1, 0);
+    map[node] = c; 
+  } else {
+    if (neg) {
+      ++(map[node].neg);
+    } else {
+      ++(map[node].pos);
+    }
+  }
+}
+
+template<> inline
+bool RewriteRule<AndSimplify>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_AND);
+}
+
+template<> inline
+Node RewriteRule<AndSimplify>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
+
+  // this will remove duplicates
+  std::hash_map<TNode, Count, TNodeHashFunction> subterms;
+  unsigned size = utils::getSize(node);
+  BitVector constant = utils::mkBitVectorOnes(size); 
+  
+  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+    TNode current = node[i];
+    // simplify constants
+    if (current.getKind() == kind::CONST_BITVECTOR) {
+      BitVector bv = current.getConst<BitVector>();
+      constant = constant & bv;
+    } else {
+      if (current.getKind() == kind::BITVECTOR_NOT) {
+        insert(subterms, current[0], true);
+      } else {
+        insert(subterms, current, false);
+      }
+    }
+  }
+
+  std::vector<Node> children;
+  
+  if (constant == BitVector(size, (unsigned)0)) {
+    return utils::mkConst(BitVector(size, (unsigned)0)); 
+  }
+
+  if (constant != utils::mkBitVectorOnes(size)) {
+    children.push_back(utils::mkConst(constant)); 
+  }
+  
+  std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
+
+  for (; it != subterms.end(); ++it) {
+    if (it->second.pos > 0 && it->second.neg > 0) {
+      // if we have a and ~a 
+      return utils::mkConst(BitVector(size, (unsigned)0)); 
+    } else {
+      // idempotence 
+      if (it->second.neg > 0) {
+        // if it only occured negated
+        children.push_back(utils::mkNode(kind::BITVECTOR_NOT, it->first));
+      } else {
+        // if it only occured positive
+        children.push_back(it->first); 
+      }
+    }
+  }
+  if (children.size() == 0) {
+    return utils::mkOnes(size); 
+  }
+  
+  return utils::mkSortedNode(kind::BITVECTOR_AND, children); 
+}
+
+template<> inline
+bool RewriteRule<OrSimplify>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_OR);
+}
+
+template<> inline
+Node RewriteRule<OrSimplify>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl;
+
+  // this will remove duplicates
+  std::hash_map<TNode, Count, TNodeHashFunction> subterms;
+  unsigned size = utils::getSize(node);
+  BitVector constant(size, (unsigned)0); 
+  
+  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+    TNode current = node[i];
+    // simplify constants
+    if (current.getKind() == kind::CONST_BITVECTOR) {
+      BitVector bv = current.getConst<BitVector>();
+      constant = constant | bv;
+    } else {
+      if (current.getKind() == kind::BITVECTOR_NOT) {
+        insert(subterms, current[0], true);
+      } else {
+        insert(subterms, current, false);
+      }
+    }
+  }
+
+  std::vector<Node> children;
+  
+  if (constant == utils::mkBitVectorOnes(size)) {
+    return utils::mkOnes(size); 
+  }
+
+  if (constant != BitVector(size, (unsigned)0)) {
+    children.push_back(utils::mkConst(constant)); 
+  }
+  
+  std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
+
+  for (; it != subterms.end(); ++it) {
+    if (it->second.pos > 0 && it->second.neg > 0) {
+      // if we have a or ~a 
+      return utils::mkOnes(size); 
+    } else {
+      // idempotence 
+      if (it->second.neg > 0) {
+        // if it only occured negated
+        children.push_back(utils::mkNode(kind::BITVECTOR_NOT, it->first));
+      } else {
+        // if it only occured positive
+        children.push_back(it->first); 
+      }
+    }
+  }
+
+  if (children.size() == 0) {
+    return utils::mkConst(BitVector(size, (unsigned)0)); 
+  }
+  return utils::mkSortedNode(kind::BITVECTOR_OR, children); 
+}
+
+template<> inline
+bool RewriteRule<XorSimplify>::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_XOR);
+}
+
+template<> inline
+Node RewriteRule<XorSimplify>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl;
+
+
+  std::hash_map<TNode, Count, TNodeHashFunction> subterms;
+  unsigned size = utils::getSize(node);
+  BitVector constant; 
+  bool const_set = false; 
+
+  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+    TNode current = node[i];
+    // simplify constants
+    if (current.getKind() == kind::CONST_BITVECTOR) {
+      BitVector bv = current.getConst<BitVector>();
+      if (const_set) {
+        constant = constant ^ bv;
+      } else {
+        const_set = true; 
+        constant = bv;
+      }
+    } else {
+      // collect number of occurances of each term and its negation
+      if (current.getKind() == kind::BITVECTOR_NOT) {
+        insert(subterms, current[0], true);
+      } else {
+        insert(subterms, current, false);
+      }
+    }
+  }
+
+  std::vector<Node> children;
+
+  std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
+  unsigned true_count = 0;
+  bool seen_false = false; 
+  for (; it != subterms.end(); ++it) {
+    unsigned pos = it->second.pos; // number of positive occurances
+    unsigned neg = it->second.neg; // number of negated occurances 
+
+    // remove duplicates using the following rules
+    // a xor a ==> false
+    // false xor false ==> false
+    seen_false = seen_false? seen_false : (pos > 1 || neg > 1);
+    // check what did not reduce
+    if (pos % 2 && neg % 2) {
+      // we have a xor ~a ==> true
+      ++true_count;
+    } else if (pos % 2) {
+      // we had a positive occurence left
+      children.push_back(it->first); 
+    } else if (neg % 2) {
+      // we had a negative occurence left
+      children.push_back(utils::mkNode(kind::BITVECTOR_NOT, it->first)); 
+    }
+    // otherwise both reduced to false
+  }
+
+  std::vector<BitVector> xorConst;
+  BitVector true_bv = utils::mkBitVectorOnes(size);
+  BitVector false_bv(size, (unsigned)0);
+  
+  if (true_count) {
+    // true xor ... xor true ==> true (odd)
+    //                       ==> false (even) 
+    xorConst.push_back(true_count % 2? true_bv : false_bv); 
+  }
+  if (seen_false) {
+    xorConst.push_back(false_bv); 
+  }
+  if(const_set) {
+    xorConst.push_back(constant); 
+  }
+
+  if (xorConst.size() > 0) {
+    BitVector result = xorConst[0];
+    for (unsigned i = 1; i < xorConst.size(); ++i) {
+      result = result ^ xorConst[i]; 
+    }
+    children.push_back(utils::mkConst(result)); 
+  }
+
+  Assert(children.size());
+  
+  return utils::mkSortedNode(kind::BITVECTOR_XOR, children); 
+}
+
+
+
+
+// template<> inline
+// bool RewriteRule<AndSimplify>::applies(Node node) {
+//   return (node.getKind() == kind::BITVECTOR_AND);
+// }
+
+// template<> inline
+// Node RewriteRule<AndSimplify>::apply(Node node) {
+//   BVDebug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
+//   return resultNode;
+// }
+
 
-// template<>
+// template<> inline
 // bool RewriteRule<>::applies(Node node) {
 //   return (node.getKind() == kind::BITVECTOR_CONCAT);
 // }
 
-// template<>
+// template<> inline
 // Node RewriteRule<>::apply(Node node) {
 //   BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
 //   return resultNode;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 507f98c91..cf8310e5a 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -36,14 +36,14 @@ namespace bv {
  *
  * Left Shift by constant amount 
  */
-template<>
+template<> inline
 bool RewriteRule<ShlByConst>::applies(Node node) {
   // if the shift amount is constant
   return (node.getKind() == kind::BITVECTOR_SHL &&
           node[1].getKind() == kind::CONST_BITVECTOR);
 }
 
-template<>
+template<> inline
 Node RewriteRule<ShlByConst>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl;
   Integer amount = node[1].getConst<BitVector>().toInteger();
@@ -72,14 +72,14 @@ Node RewriteRule<ShlByConst>::apply(Node node) {
  * Right Logical Shift by constant amount 
  */
 
-template<>
+template<> inline
 bool RewriteRule<LshrByConst>::applies(Node node) {
   // if the shift amount is constant
   return (node.getKind() == kind::BITVECTOR_LSHR &&
           node[1].getKind() == kind::CONST_BITVECTOR);
 }
 
-template<>
+template<> inline
 Node RewriteRule<LshrByConst>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl;
   Integer amount = node[1].getConst<BitVector>().toInteger();
@@ -108,14 +108,14 @@ Node RewriteRule<LshrByConst>::apply(Node node) {
  * Right Arithmetic Shift by constant amount 
  */
 
-template<>
+template<> inline
 bool RewriteRule<AshrByConst>::applies(Node node) {
   // if the shift amount is constant
   return (node.getKind() == kind::BITVECTOR_ASHR &&
           node[1].getKind() == kind::CONST_BITVECTOR);
 }
 
-template<>
+template<> inline
 Node RewriteRule<AshrByConst>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl;
   Integer amount = node[1].getConst<BitVector>().toInteger();
@@ -150,14 +150,14 @@ Node RewriteRule<AshrByConst>::apply(Node node) {
  * (a bvor a)  ==> a
  */
 
-template<>
+template<> inline
 bool RewriteRule<BitwiseIdemp>::applies(Node node) {
   return ((node.getKind() == kind::BITVECTOR_AND ||
            node.getKind() == kind::BITVECTOR_OR) &&
           node[0] == node[1]);
 }
 
-template<>
+template<> inline
 Node RewriteRule<BitwiseIdemp>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl;
   return node[0]; 
@@ -169,7 +169,7 @@ Node RewriteRule<BitwiseIdemp>::apply(Node node) {
  * (a bvand 0) ==> 0
  */
 
-template<>
+template<> inline
 bool RewriteRule<AndZero>::applies(Node node) {
   unsigned size = utils::getSize(node); 
   return (node.getKind() == kind::BITVECTOR_AND  &&
@@ -177,7 +177,7 @@ bool RewriteRule<AndZero>::applies(Node node) {
            node[1] == utils::mkConst(size, 0)));
 }
 
-template<>
+template<> inline
 Node RewriteRule<AndZero>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 0); 
@@ -189,7 +189,7 @@ Node RewriteRule<AndZero>::apply(Node node) {
  * (a bvand 1) ==> a
  */
 
-template<>
+template<> inline
 bool RewriteRule<AndOne>::applies(Node node) {
   unsigned size = utils::getSize(node);
   Node ones = utils::mkOnes(size); 
@@ -198,7 +198,7 @@ bool RewriteRule<AndOne>::applies(Node node) {
            node[1] == ones));
 }
 
-template<>
+template<> inline
 Node RewriteRule<AndOne>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl;
   unsigned size = utils::getSize(node);
@@ -217,7 +217,7 @@ Node RewriteRule<AndOne>::apply(Node node) {
  * (a bvor 0) ==> a
  */
 
-template<>
+template<> inline
 bool RewriteRule<OrZero>::applies(Node node) {
   unsigned size = utils::getSize(node); 
   return (node.getKind() == kind::BITVECTOR_OR  &&
@@ -225,7 +225,7 @@ bool RewriteRule<OrZero>::applies(Node node) {
            node[1] == utils::mkConst(size, 0)));
 }
 
-template<>
+template<> inline
 Node RewriteRule<OrZero>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl;
   
@@ -244,7 +244,7 @@ Node RewriteRule<OrZero>::apply(Node node) {
  * (a bvor 1) ==> 1
  */
 
-template<>
+template<> inline
 bool RewriteRule<OrOne>::applies(Node node) {
   unsigned size = utils::getSize(node);
   Node ones = utils::mkOnes(size); 
@@ -253,7 +253,7 @@ bool RewriteRule<OrOne>::applies(Node node) {
            node[1] == ones));
 }
 
-template<>
+template<> inline
 Node RewriteRule<OrOne>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl;
   return utils::mkOnes(utils::getSize(node)); 
@@ -266,13 +266,13 @@ Node RewriteRule<OrOne>::apply(Node node) {
  * (a bvxor a) ==> 0
  */
 
-template<>
+template<> inline
 bool RewriteRule<XorDuplicate>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_XOR &&
           node[0] == node[1]);
 }
 
-template<>
+template<> inline
 Node RewriteRule<XorDuplicate>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl;
   return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); 
@@ -284,27 +284,39 @@ Node RewriteRule<XorDuplicate>::apply(Node node) {
  * (a bvxor 1) ==> ~a
  */
 
-template<>
+template<> inline
 bool RewriteRule<XorOne>::applies(Node node) {
-  Node ones = utils::mkOnes(utils::getSize(node)); 
-  return (node.getKind() == kind::BITVECTOR_XOR &&
-          (node[0] == ones ||
-           node[1] == ones));
+  if (node.getKind() != kind::BITVECTOR_XOR) {
+    return false; 
+  }
+  Node ones = utils::mkOnes(utils::getSize(node));
+  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+    if (node[i] == ones) {
+      return true; 
+    }
+  }
+  return false; 
 }
 
-template<>
+template<> inline
 Node RewriteRule<XorOne>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl;
   Node ones = utils::mkOnes(utils::getSize(node)); 
-  Node a;
-  if (node[0] == ones) {
-    a = node[1];
-  } else {
-    Assert(node[1] == ones);
-    a = node[0];
+  std::vector<Node> children;
+  bool found_ones = false;
+  // XorSimplify should have been called before
+  for(unsigned i = 0; i < node.getNumChildren(); ++i) {
+    if (node[i] == ones) {
+      // make sure only ones occurs only once
+      Assert(!found_ones);
+      found_ones = true;
+    } else {
+      children.push_back(node[i]); 
+    }
   }
 
-  return utils::mkNode(kind::BITVECTOR_NOT, a);  
+  children[0] = utils::mkNode(kind::BITVECTOR_NOT, children[0]);
+  return utils::mkSortedNode(kind::BITVECTOR_XOR, children); 
 }
 
 
@@ -314,24 +326,39 @@ Node RewriteRule<XorOne>::apply(Node node) {
  * (a bvxor 0) ==> a
  */
 
-template<>
+template<> inline
 bool RewriteRule<XorZero>::applies(Node node) {
-  Node zero = utils::mkConst(utils::getSize(node), 0); 
-  return (node.getKind() == kind::BITVECTOR_XOR &&
-          (node[0] == zero ||
-           node[1] == zero));
+  if (node.getKind() != kind::BITVECTOR_XOR) {
+    return false; 
+  }
+  Node zero = utils::mkConst(utils::getSize(node), 0);
+  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+    if (node[i] == zero) {
+      return true; 
+    }
+  }
+  return false; 
 }
 
-template<>
+template<> inline
 Node RewriteRule<XorZero>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl;
-  Node zero = utils::mkConst(utils::getSize(node), 0); 
-  if (node[0] == zero) {
-    return node[1];
+  std::vector<Node> children;
+  bool found_zero = false;
+  Node zero = utils::mkConst(utils::getSize(node), 0);
+    
+  // XorSimplify should have been called before
+  for(unsigned i = 0; i < node.getNumChildren(); ++i) {
+    if (node[i] == zero) {
+      // make sure zero occurs only once
+      Assert(!found_zero);
+      found_zero = true;
+    } else {
+      children.push_back(node[i]); 
+    }
   }
-  
-  Assert(node[1] == zero);
-  return node[0];
+
+  return utils::mkNode(kind::BITVECTOR_XOR, children); 
 }
 
 
@@ -341,14 +368,14 @@ Node RewriteRule<XorZero>::apply(Node node) {
  * (a bvand (~ a)) ==> 0
  */
 
-template<>
+template<> inline
 bool RewriteRule<BitwiseNotAnd>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_AND &&
           ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) ||
            (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0]))); 
 }
 
-template<>
+template<> inline
 Node RewriteRule<BitwiseNotAnd>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl;
   return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); 
@@ -360,14 +387,14 @@ Node RewriteRule<BitwiseNotAnd>::apply(Node node) {
  * (a bvor (~ a)) ==> 1
  */
 
-template<>
+template<> inline
 bool RewriteRule<BitwiseNotOr>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_OR &&
           ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) ||
            (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0]))); 
 }
 
-template<>
+template<> inline
 Node RewriteRule<BitwiseNotOr>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl;
   uint32_t size = utils::getSize(node);
@@ -381,14 +408,14 @@ Node RewriteRule<BitwiseNotOr>::apply(Node node) {
  * ((~ a) bvxor (~ b)) ==> (a bvxor b)
  */
 
-template<>
+template<> inline
 bool RewriteRule<XorNot>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_XOR &&
           node[0].getKind() == kind::BITVECTOR_NOT &&
           node[1].getKind() == kind::BITVECTOR_NOT); 
 }
 
-template<>
+template<> inline
 Node RewriteRule<XorNot>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
   Node a = node[0][0];
@@ -402,19 +429,19 @@ Node RewriteRule<XorNot>::apply(Node node) {
  * ~(a bvxor b) ==> (~ a bvxor b)
  */
 
-template<>
+template<> inline
 bool RewriteRule<NotXor>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_NOT &&
           node[0].getKind() == kind::BITVECTOR_XOR); 
 }
 
-template<>
+template<> inline
 Node RewriteRule<NotXor>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
   Node a = node[0][0];
   Node b = node[0][1];
   Node nota = utils::mkNode(kind::BITVECTOR_NOT, a); 
-  return utils::mkNode(kind::BITVECTOR_XOR, nota, b); 
+  return utils::mkSortedNode(kind::BITVECTOR_XOR, nota, b); 
 }
 
 /**
@@ -423,13 +450,13 @@ Node RewriteRule<NotXor>::apply(Node node) {
  * ~ (~ a) ==> a
  */
 
-template<>
+template<> inline
 bool RewriteRule<NotIdemp>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_NOT &&
           node[0].getKind() == kind::BITVECTOR_NOT); 
 }
 
-template<>
+template<> inline
 Node RewriteRule<NotIdemp>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<XorIdemp>(" << node << ")" << std::endl;
   return node[0][0];
@@ -443,14 +470,14 @@ Node RewriteRule<NotIdemp>::apply(Node node) {
  * a < a ==> false
  */
 
-template<>
+template<> inline
 bool RewriteRule<LtSelf>::applies(Node node) {
   return ((node.getKind() == kind::BITVECTOR_ULT ||
            node.getKind() == kind::BITVECTOR_SLT) &&
           node[0] == node[1]);
 }
 
-template<>
+template<> inline
 Node RewriteRule<LtSelf>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<LtSelf>(" << node << ")" << std::endl;
   return utils::mkFalse(); 
@@ -462,14 +489,14 @@ Node RewriteRule<LtSelf>::apply(Node node) {
  * a <= a ==> true
  */
 
-template<>
+template<> inline
 bool RewriteRule<LteSelf>::applies(Node node) {
   return ((node.getKind() == kind::BITVECTOR_ULE ||
            node.getKind() == kind::BITVECTOR_SLE) &&
           node[0] == node[1]);
 }
 
-template<>
+template<> inline
 Node RewriteRule<LteSelf>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<LteSelf>(" << node << ")" << std::endl;
   return utils::mkTrue(); 
@@ -481,13 +508,13 @@ Node RewriteRule<LteSelf>::apply(Node node) {
  * a < 0 ==> false
  */
 
-template<>
+template<> inline
 bool RewriteRule<UltZero>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_ULT &&
           node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
 }
 
-template<>
+template<> inline
 Node RewriteRule<UltZero>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
   return utils::mkFalse(); 
@@ -499,13 +526,13 @@ Node RewriteRule<UltZero>::apply(Node node) {
  * a < a ==> false
  */
 
-template<>
+template<> inline
 bool RewriteRule<UltSelf>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_ULT &&
           node[1] == node[0]); 
 }
 
-template<>
+template<> inline
 Node RewriteRule<UltSelf>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<UltSelf>(" << node << ")" << std::endl;
   return utils::mkFalse(); 
@@ -518,13 +545,13 @@ Node RewriteRule<UltSelf>::apply(Node node) {
  * a <= 0 ==> a = 0
  */
 
-template<>
+template<> inline
 bool RewriteRule<UleZero>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_ULE &&
           node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
 }
 
-template<>
+template<> inline
 Node RewriteRule<UleZero>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl;
   return utils::mkNode(kind::EQUAL, node[0], node[1]); 
@@ -536,13 +563,13 @@ Node RewriteRule<UleZero>::apply(Node node) {
  * a <= a ==> true
  */
 
-template<>
+template<> inline
 bool RewriteRule<UleSelf>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_ULE &&
           node[1] == node[0]); 
 }
 
-template<>
+template<> inline
 Node RewriteRule<UleSelf>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<UleSelf>(" << node << ")" << std::endl;
   return utils::mkTrue(); 
@@ -555,13 +582,13 @@ Node RewriteRule<UleSelf>::apply(Node node) {
  * 0 <= a ==> true
  */
 
-template<>
+template<> inline
 bool RewriteRule<ZeroUle>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_ULE &&
           node[0] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
 }
 
-template<>
+template<> inline
 Node RewriteRule<ZeroUle>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node << ")" << std::endl;
   return utils::mkTrue(); 
@@ -573,7 +600,7 @@ Node RewriteRule<ZeroUle>::apply(Node node) {
  * a <= 11..1 ==> true
  */
 
-template<>
+template<> inline
 bool RewriteRule<UleMax>::applies(Node node) {
   if (node.getKind()!= kind::BITVECTOR_ULE) {
     return false; 
@@ -584,7 +611,7 @@ bool RewriteRule<UleMax>::applies(Node node) {
           node[1] == utils::mkConst(BitVector(size, ones)));
 }
 
-template<>
+template<> inline
 Node RewriteRule<UleMax>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<UleMax>(" << node << ")" << std::endl;
   return utils::mkTrue(); 
@@ -596,13 +623,13 @@ Node RewriteRule<UleMax>::apply(Node node) {
  * ~ ( a < b) ==> b <= a
  */
 
-template<>
+template<> inline
 bool RewriteRule<NotUlt>::applies(Node node) {
   return (node.getKind() == kind::NOT &&
           node[0].getKind() == kind::BITVECTOR_ULT);
 }
 
-template<>
+template<> inline
 Node RewriteRule<NotUlt>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl;
   Node ult = node[0];
@@ -617,13 +644,13 @@ Node RewriteRule<NotUlt>::apply(Node node) {
  * ~ ( a <= b) ==> b < a
  */
 
-template<>
+template<> inline
 bool RewriteRule<NotUle>::applies(Node node) {
   return (node.getKind() == kind::NOT &&
           node[0].getKind() == kind::BITVECTOR_ULE);
 }
 
-template<>
+template<> inline
 Node RewriteRule<NotUle>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl;
   Node ult = node[0];
@@ -638,7 +665,7 @@ Node RewriteRule<NotUle>::apply(Node node) {
  * (a * 1) ==> a
  */
 
-template<>
+template<> inline
 bool RewriteRule<MultOne>::applies(Node node) {
   unsigned size = utils::getSize(node); 
   return (node.getKind() == kind::BITVECTOR_MULT &&
@@ -646,7 +673,7 @@ bool RewriteRule<MultOne>::applies(Node node) {
            node[1] == utils::mkConst(size, 1)));
 }
 
-template<>
+template<> inline
 Node RewriteRule<MultOne>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<MultOne>(" << node << ")" << std::endl;
   unsigned size = utils::getSize(node); 
@@ -663,7 +690,7 @@ Node RewriteRule<MultOne>::apply(Node node) {
  * (a * 0) ==> 0
  */
 
-template<>
+template<> inline
 bool RewriteRule<MultZero>::applies(Node node) {
   unsigned size = utils::getSize(node); 
   return (node.getKind() == kind::BITVECTOR_MULT &&
@@ -671,7 +698,7 @@ bool RewriteRule<MultZero>::applies(Node node) {
            node[1] == utils::mkConst(size, 0)));
 }
 
-template<>
+template<> inline
 Node RewriteRule<MultZero>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<MultZero>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 0); 
@@ -683,33 +710,39 @@ Node RewriteRule<MultZero>::apply(Node node) {
  * (a * 2^k) ==> a[n-k-1:0] 0_k
  */
 
-template<>
+template<> inline
 bool RewriteRule<MultPow2>::applies(Node node) {
-  return (node.getKind() == kind::BITVECTOR_MULT &&
-          (utils::isPow2Const(node[0]) ||
-           utils::isPow2Const(node[1])));
+  if (node.getKind() != kind::BITVECTOR_MULT)
+    return false;
+
+  for(unsigned i = 0; i < node.getNumChildren(); ++i) {
+    if (utils::isPow2Const(node[i])) {
+      return true; 
+    }
+  }
+  return false; 
 }
 
-template<>
+template<> inline
 Node RewriteRule<MultPow2>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl;
-  Node a;
-  unsigned power;
-  power = utils::isPow2Const(node[0]);
-
-  if (power != 0) {
-    a = node[1];
-    // isPow2Const returns the power + 1
-    --power;
-  } else {
-    power = utils::isPow2Const(node[1]);
-    Assert(power != 0); 
-    a = node[0];
-    power--; 
+
+  std::vector<Node>  children;
+  unsigned exponent = 0; 
+  for(unsigned i = 0; i < node.getNumChildren(); ++i) {
+    unsigned exp = utils::isPow2Const(node[i]);
+    if (exp) {
+      exponent += exp - 1;
+    }
+    else {
+      children.push_back(node[i]); 
+    }
   }
 
-  Node extract = utils::mkExtract(a, utils::getSize(node) - power - 1, 0);
-  Node zeros = utils::mkConst(power, 0);
+  Node a = utils::mkSortedNode(kind::BITVECTOR_MULT, children); 
+
+  Node extract = utils::mkExtract(a, utils::getSize(node) - exponent - 1, 0);
+  Node zeros = utils::mkConst(exponent, 0);
   return utils::mkConcat(extract, zeros); 
 }
 
@@ -719,7 +752,7 @@ Node RewriteRule<MultPow2>::apply(Node node) {
  * (a + 0) ==> a
  */
 
-template<>
+template<> inline
 bool RewriteRule<PlusZero>::applies(Node node) {
   Node zero = utils::mkConst(utils::getSize(node), 0); 
   return (node.getKind() == kind::BITVECTOR_PLUS &&
@@ -727,7 +760,7 @@ bool RewriteRule<PlusZero>::applies(Node node) {
            node[1] == zero));
 }
 
-template<>
+template<> inline
 Node RewriteRule<PlusZero>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<PlusZero>(" << node << ")" << std::endl;
   Node zero = utils::mkConst(utils::getSize(node), 0);
@@ -744,13 +777,13 @@ Node RewriteRule<PlusZero>::apply(Node node) {
  * -(-a) ==> a 
  */
 
-template<>
+template<> inline
 bool RewriteRule<NegIdemp>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_NEG &&
           node[0].getKind() == kind::BITVECTOR_NEG);
 }
 
-template<>
+template<> inline
 Node RewriteRule<NegIdemp>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node << ")" << std::endl;
   return node[0][0]; 
@@ -762,13 +795,13 @@ Node RewriteRule<NegIdemp>::apply(Node node) {
  * (a udiv 2^k) ==> 0_k a[n-1: k]
  */
 
-template<>
+template<> inline
 bool RewriteRule<UdivPow2>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_UDIV &&
           utils::isPow2Const(node[1]));
 }
 
-template<>
+template<> inline
 Node RewriteRule<UdivPow2>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl;
   Node a = node[0];
@@ -786,13 +819,13 @@ Node RewriteRule<UdivPow2>::apply(Node node) {
  * (a udiv 1) ==> a
  */
 
-template<>
+template<> inline
 bool RewriteRule<UdivOne>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_UDIV &&
           node[1] == utils::mkConst(utils::getSize(node), 1));
 }
 
-template<>
+template<> inline
 Node RewriteRule<UdivOne>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl;
   return node[0]; 
@@ -804,13 +837,13 @@ Node RewriteRule<UdivOne>::apply(Node node) {
  * (a udiv a) ==> 1
  */
 
-template<>
+template<> inline
 bool RewriteRule<UdivSelf>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_UDIV &&
           node[0] == node[1]);
 }
 
-template<>
+template<> inline
 Node RewriteRule<UdivSelf>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<UdivSelf>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 1); 
@@ -822,13 +855,13 @@ Node RewriteRule<UdivSelf>::apply(Node node) {
  * (a urem 2^k) ==> 0_(n-k) a[k-1:0]
  */
 
-template<>
+template<> inline
 bool RewriteRule<UremPow2>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_UREM &&
           utils::isPow2Const(node[1]));
 }
 
-template<>
+template<> inline
 Node RewriteRule<UremPow2>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
   TNode a = node[0];
@@ -844,13 +877,13 @@ Node RewriteRule<UremPow2>::apply(Node node) {
  * (a urem 1) ==> 0
  */
 
-template<>
+template<> inline
 bool RewriteRule<UremOne>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_UREM &&
           node[1] == utils::mkConst(utils::getSize(node), 1));
 }
 
-template<>
+template<> inline
 Node RewriteRule<UremOne>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<UremOne>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 0); 
@@ -862,13 +895,13 @@ Node RewriteRule<UremOne>::apply(Node node) {
  * (a urem a) ==> 0
  */
 
-template<>
+template<> inline
 bool RewriteRule<UremSelf>::applies(Node node) {
   return (node.getKind() == kind::BITVECTOR_UREM &&
           node[0] == node[1]);
 }
 
-template<>
+template<> inline
 Node RewriteRule<UremSelf>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<UremSelf>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 0); 
@@ -880,7 +913,7 @@ Node RewriteRule<UremSelf>::apply(Node node) {
  * (0_k >> a) ==> 0_k 
  */
 
-template<>
+template<> inline
 bool RewriteRule<ShiftZero>::applies(Node node) {
   return ((node.getKind() == kind::BITVECTOR_SHL ||
            node.getKind() == kind::BITVECTOR_LSHR ||
@@ -888,24 +921,110 @@ bool RewriteRule<ShiftZero>::applies(Node node) {
           node[0] == utils::mkConst(utils::getSize(node), 0));
 }
 
-template<>
+template<> inline
 Node RewriteRule<ShiftZero>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node << ")" << std::endl;
   return node[0]; 
 }
 
+/**
+ * BBPlusNeg
+ * 
+ * -a1 - a2 - ... - an + ak + ..  ==> - (a1 + a2 + ... + an) + ak
+ *
+ */
+
+template<> inline
+bool RewriteRule<BBPlusNeg>::applies(Node node) {
+  if (node.getKind() != kind::BITVECTOR_PLUS) {
+    return false; 
+  }
+
+  unsigned neg_count = 0; 
+  for(unsigned i = 0; i < node.getNumChildren(); ++i) {
+    if (node[i].getKind()== kind::BITVECTOR_NEG) {
+      ++neg_count; 
+    }
+  }
+  return neg_count > 1;
+}
+
+template<> inline
+Node RewriteRule<BBPlusNeg>::apply(Node node) {
+  BVDebug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node << ")" << std::endl;
+
+  std::vector<Node> children;
+  unsigned neg_count = 0; 
+  for(unsigned i = 0; i < node.getNumChildren(); ++i) {
+    if (node[i].getKind() == kind::BITVECTOR_NEG) {
+      ++neg_count; 
+      children.push_back(utils::mkNode(kind::BITVECTOR_NOT, node[i][0]));
+    } else {
+      children.push_back(node[i]); 
+    }
+  }
+  Assert(neg_count!= 0); 
+  children.push_back(utils::mkConst(utils::getSize(node), neg_count)); 
+
+  return utils::mkSortedNode(kind::BITVECTOR_PLUS, children); 
+}
+
+// /**
+//  * 
+//  *
+//  * 
+//  */
+
+// template<> inline
+// bool RewriteRule<BBFactorOut>::applies(Node node) {
+//   if (node.getKind() != kind::BITVECTOR_PLUS) {
+//     return false; 
+//   }
+
+//   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+//     if (node[i].getKind() != kind::BITVECTOR_MULT) {
+//       return false; 
+//     }
+//   }
+// }
+
+// template<> inline
+// Node RewriteRule<BBFactorOut>::apply(Node node) {
+//   BVDebug("bv-rewrite") << "RewriteRule<BBFactorOut>(" << node << ")" << std::endl;
+//   std::hash_set<TNode, TNodeHashFunction> factors;
+
+//   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+//     Assert (node[i].getKind() == kind::BITVECTOR_MULT);
+//     for (unsigned j = 0; j < node[i].getNumChildren(); ++j) {
+//       factors.insert(node[i][j]); 
+//     }
+//   }
+
+//   std::vector<TNode> gcd; 
+//   std::hash_set<TNode, TNodeHashFunction>::const_iterator it;
+//   for (it = factors.begin(); it != factors.end(); ++it) {
+//     // for each factor check if it occurs in all children
+//     TNode f = *it; 
+//     for (unsigned i = 0; i < node.getNumChildren
+    
+//     }
+//   }
+//   return ; 
+// }
+
+
 // /**
 //  * 
 //  *
 //  * 
 //  */
 
-// template<>
+// template<> inline
 // bool RewriteRule<>::applies(Node node) {
 //   return (node.getKind() == );
 // }
 
-// template<>
+// template<> inline
 // Node RewriteRule<>::apply(Node node) {
 //   BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
 //   return ; 
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 2b48977b6..c2649e881 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -49,19 +49,31 @@ void TheoryBVRewriter::shutdown() {
 }
 
 RewriteResponse TheoryBVRewriter::preRewrite(TNode node) {
-  Debug("bitvector-rewrite") << "TheoryBV::preRewrite(" << node << ")" << std::endl;
-  //return d_rewriteTable[node.getKind()](node);
-  return RewriteResponse(REWRITE_DONE, node); 
+  RewriteResponse res = d_rewriteTable[node.getKind()](node, true);
+  if(res.node != node) {
+    Debug("bitvector-rewrite") << "TheoryBV::preRewrite    " << node << std::endl;
+    Debug("bitvector-rewrite") << "TheoryBV::preRewrite to " << res.node << std::endl;
+  }
+  return res; 
 }
 
 RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
-  //TimerStat::CodeTimer codeTimer(*d_rewriteTimer); 
-  Debug("bitvector-rewrite") << "TheoryBV::postRewrite(" << node << ")" << std::endl;
-  RewriteResponse res = d_rewriteTable[node.getKind()](node);
+  RewriteResponse res = d_rewriteTable[node.getKind()](node, false);
+  if(res.node!= node) {
+    Debug("bitvector-rewrite") << "TheoryBV::postRewrite    " << node << std::endl;
+    Debug("bitvector-rewrite") << "TheoryBV::postRewrite to " << res.node << std::endl;
+  }
+  // if (res.status == REWRITE_DONE) {
+  //   Node rewr = res.node;
+  //   Node rerewr = d_rewriteTable[rewr.getKind()](rewr, false).node;
+  //   Assert(rewr == rerewr);
+  // }
+  
   return res; 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) {
+  // reduce common subexpressions on both sides
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<EvalUlt>,
       // if both arguments are constants evaluates
@@ -72,8 +84,13 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node) {
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node){
-  return RewriteResponse(REWRITE_DONE, node); 
+RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){
+  Node resultNode = LinearRewriteStrategy
+    < RewriteRule < EvalSlt >
+      >::apply(node);
+
+  return RewriteResponse(REWRITE_DONE, resultNode); 
+
   // Node resultNode = LinearRewriteStrategy
   //   < RewriteRule < SltEliminate >
   //     // a <_s b ==> a + 2^{n-1} <_u b + 2^{n-1}
@@ -82,7 +99,7 @@ RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node){
   // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUle(TNode node){
+RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<EvalUle>,
       RewriteRule<UleMax>,
@@ -93,16 +110,15 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node){
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSle(TNode node){
-  return RewriteResponse(REWRITE_DONE, node); 
-  // Node resultNode = LinearRewriteStrategy
-  //   < RewriteRule<SleEliminate>
-  //     >::apply(node);
+RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){
+  Node resultNode = LinearRewriteStrategy
+    < RewriteRule < EvalSle >
+      >::apply(node);
 
-  // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node){
+RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<UgtEliminate>
     >::apply(node);
@@ -110,16 +126,16 @@ RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node){
   return RewriteResponse(REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node){
+RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool preregister){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SgtEliminate>
       //RewriteRule<SltEliminate>
       >::apply(node);
   
-  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  return RewriteResponse(REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUge(TNode node){
+RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool preregister){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<UgeEliminate>
     >::apply(node);
@@ -127,7 +143,7 @@ RewriteResponse TheoryBVRewriter::RewriteUge(TNode node){
   return RewriteResponse(REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSge(TNode node){
+RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool preregister){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SgeEliminate>
       //      RewriteRule<SleEliminate>
@@ -136,8 +152,9 @@ RewriteResponse TheoryBVRewriter::RewriteSge(TNode node){
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteNot(TNode node){
-  Node resultNode = node; 
+RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool preregister){
+  Node resultNode = node;
+  
   if(RewriteRule<NotXor>::applies(node)) {
     resultNode = RewriteRule<NotXor>::run<false>(node);
     return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
@@ -150,8 +167,9 @@ RewriteResponse TheoryBVRewriter::RewriteNot(TNode node){
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) {
   Node resultNode = node;
+
   if (RewriteRule<ExtractConcat>::applies(node)) {
     resultNode = RewriteRule<ExtractConcat>::run<false>(node);
     return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
@@ -184,7 +202,8 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node) {
 }
 
 
-RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool preregister) {
+  
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<ConcatFlatten>,
       // Flatten the top level concatenations
@@ -197,45 +216,53 @@ RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node) {
    return RewriteResponse(REWRITE_DONE, resultNode);  
 }
 
-RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node){
-  Node resultNode = LinearRewriteStrategy
-    < RewriteRule<EvalAnd>,
-      RewriteRule<BitwiseIdemp>,
-      RewriteRule<AndZero>,
-      RewriteRule<AndOne> 
+RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){
+  Node resultNode = node;
+  
+  resultNode = LinearRewriteStrategy
+    < RewriteRule<FlattenAssocCommut>,
+      RewriteRule<AndSimplify>
+      // RewriteRule<EvalAnd>,
+      // RewriteRule<BitwiseIdemp>,
+      // //RewriteRule<BitwiseSlice>, -> might need rw again
+      // RewriteRule<AndZero>,
+      // RewriteRule<AndOne> 
       >::apply(node);
 
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteOr(TNode node){
-  Node resultNode = LinearRewriteStrategy
-    < RewriteRule<EvalOr>,
-      RewriteRule<BitwiseIdemp>,
-      RewriteRule<OrZero>,
-      RewriteRule<OrOne>
+RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){
+  Node resultNode = node;
+
+  resultNode = LinearRewriteStrategy
+    < RewriteRule<FlattenAssocCommut>,
+      RewriteRule<OrSimplify>
     >::apply(node);
   
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteXor(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) {
   Node resultNode = node;
-  if (RewriteRule<XorOne>::applies(node)) {
-    resultNode = RewriteRule<XorOne>::run<false> (node);
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
-  }
+
   resultNode = LinearRewriteStrategy
-    < RewriteRule<XorNot>, 
-      RewriteRule<EvalXor>,
-      RewriteRule<XorDuplicate>,
-      RewriteRule<XorZero>
+    < RewriteRule<FlattenAssocCommut>, // flatten the expression 
+      RewriteRule<XorSimplify>,        // simplify duplicates and constants
+      RewriteRule<XorZero>             // checks if the constant part is zero and eliminates it
     >::apply(node);
- 
+
+  // this simplification introduces new terms and might require further
+  // rewriting
+  if (RewriteRule<XorOne>::applies(resultNode)) {
+    resultNode = RewriteRule<XorOne>::run<false> (resultNode);
+    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  }
+
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool preregister) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<XnorEliminate>
     >::apply(node);
@@ -243,7 +270,7 @@ RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteNand(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool preregister) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<NandEliminate>
       >::apply(node);
@@ -251,7 +278,7 @@ RewriteResponse TheoryBVRewriter::RewriteNand(TNode node) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteNor(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool preregister) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<NorEliminate>
     >::apply(node);
@@ -259,7 +286,7 @@ RewriteResponse TheoryBVRewriter::RewriteNor(TNode node) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteComp(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool preregister) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<CompEliminate>
       >::apply(node);
@@ -267,54 +294,81 @@ RewriteResponse TheoryBVRewriter::RewriteComp(TNode node) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteMult(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) {
   Node resultNode = node; 
-  if(RewriteRule<MultPow2>::applies(node)) {
-    resultNode = RewriteRule<MultPow2>::run <false> (node);
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
-  }
 
   resultNode = LinearRewriteStrategy
-    < RewriteRule<EvalMult>,
-      RewriteRule<MultOne>,
-      RewriteRule<MultZero>
+    < RewriteRule<FlattenAssocCommut>, // flattens and sorts
+      RewriteRule<MultSimplify>        // multiplies constant part and checks for 0
     >::apply(node);
 
+  // only apply if every subterm was already rewritten 
+  if (!preregister) {
+    // distributes multiplication by constant over +, - and unary -
+    if(RewriteRule<MultDistribConst>::applies(resultNode)) {
+      resultNode = RewriteRule<MultDistribConst>::run<false>(resultNode);
+      // creating new terms that might simplify further
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
+  }
+
+  if(resultNode == node) {
+    return RewriteResponse(REWRITE_DONE, resultNode); 
+  }
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewritePlus(TNode node) {
-  Node resultNode = LinearRewriteStrategy
-    < RewriteRule<EvalPlus>,
-      RewriteRule<PlusZero>
-      // RewriteRule<PlusSelf>,
-      // RewriteRule<PlusNegSelf>
-      // RewriteRule<PlusLiftConcat> 
-    >::apply(node);
+RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool preregister) {
+  Node resultNode = node;
 
-  return RewriteResponse(REWRITE_DONE, resultNode); 
+  resultNode = LinearRewriteStrategy
+    < RewriteRule<FlattenAssocCommut>, 
+      RewriteRule<PlusCombineLikeTerms>
+      // RewriteRule<PlusLiftConcat> 
+      >::apply(resultNode);
+  if (resultNode == node) {
+    return RewriteResponse(REWRITE_DONE, resultNode);
+  } else {
+    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  }
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSub(TNode node){
-  return RewriteResponse(REWRITE_DONE, node); 
-  // Node resultNode = LinearRewriteStrategy
-  //   < RewriteRule<SubEliminate>
-  //   >::apply(node);
+RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool preregister){
+  // return RewriteResponse(REWRITE_DONE, node); 
+  Node resultNode = LinearRewriteStrategy
+    < RewriteRule<SubEliminate>
+    >::apply(node);
   
-  // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node) {
-  Node resultNode = LinearRewriteStrategy
+RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) {
+  Node resultNode = node; 
+  
+  resultNode = LinearRewriteStrategy
     < RewriteRule<EvalNeg>,
-      RewriteRule<NegIdemp>
-    >::apply(node);
+      RewriteRule<NegIdemp>,
+      RewriteRule<NegSub>
+      >::apply(node);
+  
+  if (RewriteRule<NegPlus>::applies(node)) {
+    resultNode = RewriteRule<NegPlus>::run<false>(node);
+    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  }
   
+  if(!preregister) {
+    if (RewriteRule<NegMult>::applies(node)) {
+      resultNode = RewriteRule<NegMult>::run<false>(node);
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
+  }
+
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node){
-  Node resultNode = node; 
+RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool preregister){
+  Node resultNode = node;
+
   if(RewriteRule<UdivPow2>::applies(node)) {
     resultNode = RewriteRule<UdivPow2>::run <false> (node);
     return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
@@ -329,8 +383,10 @@ RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node){
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node) {
-  Node resultNode = node; 
+RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool preregister) {
+  Node resultNode = node;
+  return RewriteResponse(REWRITE_DONE, resultNode); 
+
   if(RewriteRule<UremPow2>::applies(node)) {
     resultNode = RewriteRule<UremPow2>::run <false> (node);
     return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
@@ -344,7 +400,7 @@ RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node) {
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool preregister) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SmodEliminate>
       >::apply(node);
@@ -352,7 +408,7 @@ RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool preregister) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SdivEliminate>
       >::apply(node);
@@ -360,14 +416,14 @@ RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSrem(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteSrem(TNode node, bool preregister) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SremEliminate>
        >::apply(node);
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteShl(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool preregister) {
   Node resultNode = node; 
   if(RewriteRule<ShlByConst>::applies(node)) {
     resultNode = RewriteRule<ShlByConst>::run <false> (node);
@@ -382,7 +438,7 @@ RewriteResponse TheoryBVRewriter::RewriteShl(TNode node) {
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool preregister) {
   Node resultNode = node; 
   if(RewriteRule<LshrByConst>::applies(node)) {
     resultNode = RewriteRule<LshrByConst>::run <false> (node);
@@ -397,7 +453,7 @@ RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node) {
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool preregister) {
   Node resultNode = node; 
   if(RewriteRule<AshrByConst>::applies(node)) {
     resultNode = RewriteRule<AshrByConst>::run <false> (node);
@@ -413,7 +469,7 @@ RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node) {
 }
 
 
-RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool preregister) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<RepeatEliminate >
     >::apply(node);
@@ -421,7 +477,7 @@ RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node){
+RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool preregister){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<ZeroExtendEliminate >
     >::apply(node);
@@ -429,17 +485,17 @@ RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node){
   return RewriteResponse(REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node) {
-  // Node resultNode = LinearRewriteStrategy
-  //   < RewriteRule<SignExtendEliminate >
-  //   >::apply(node);
+RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool preregister) {
+  Node resultNode = LinearRewriteStrategy
+    < RewriteRule<EvalSignExtend>
+    >::apply(node);
   
   // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
-  return RewriteResponse(REWRITE_DONE, node); 
+  return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
 
-RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool preregister) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<RotateRightEliminate >
     >::apply(node);
@@ -447,7 +503,7 @@ RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node){
+RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool preregister){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<RotateLeftEliminate >
       >::apply(node);
@@ -455,7 +511,7 @@ RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node){
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node) {
+RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<FailEq>,
       RewriteRule<SimplifyEq>,
@@ -466,11 +522,11 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node) {
 }
 
 
-RewriteResponse TheoryBVRewriter::IdentityRewrite(TNode node) {
+RewriteResponse TheoryBVRewriter::IdentityRewrite(TNode node, bool prerewrite) {
   return RewriteResponse(REWRITE_DONE, node); 
 }
 
-RewriteResponse TheoryBVRewriter::UndefinedRewrite(TNode node) {
+RewriteResponse TheoryBVRewriter::UndefinedRewrite(TNode node, bool prerewrite) {
   Debug("bv-rewrite") << "TheoryBV::UndefinedRewrite for" << node;
   Unimplemented(); 
 } 
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 7ce914477..0ce3fa303 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -30,7 +30,7 @@ namespace theory {
 namespace bv {
 
 struct AllRewriteRules;
-typedef RewriteResponse (*RewriteFunction) (TNode);
+typedef RewriteResponse (*RewriteFunction) (TNode, bool);
 
 class TheoryBVRewriter {
   // static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules;
@@ -39,47 +39,47 @@ class TheoryBVRewriter {
 #warning "TODO: Double check thread safety and make sure the fix compiles on mac."
   static RewriteFunction d_rewriteTable[kind::LAST_KIND];
 
-  static RewriteResponse IdentityRewrite(TNode node);
-  static RewriteResponse UndefinedRewrite(TNode node); 
+  static RewriteResponse IdentityRewrite(TNode node, bool prerewrite = false);
+  static RewriteResponse UndefinedRewrite(TNode node, bool prerewrite = false); 
 
   static void initializeRewrites();
   
-  static RewriteResponse RewriteEqual(TNode node);
-  static RewriteResponse RewriteUlt(TNode node);
-  static RewriteResponse RewriteSlt(TNode node);
-  static RewriteResponse RewriteUle(TNode node);
-  static RewriteResponse RewriteSle(TNode node);
-  static RewriteResponse RewriteUgt(TNode node);
-  static RewriteResponse RewriteSgt(TNode node);
-  static RewriteResponse RewriteUge(TNode node);
-  static RewriteResponse RewriteSge(TNode node);
-  static RewriteResponse RewriteNot(TNode node);
-  static RewriteResponse RewriteConcat(TNode node);
-  static RewriteResponse RewriteAnd(TNode node);
-  static RewriteResponse RewriteOr(TNode node);
-  static RewriteResponse RewriteXnor(TNode node);
-  static RewriteResponse RewriteXor(TNode node);
-  static RewriteResponse RewriteNand(TNode node);
-  static RewriteResponse RewriteNor(TNode node);
-  static RewriteResponse RewriteComp(TNode node);
-  static RewriteResponse RewriteMult(TNode node);
-  static RewriteResponse RewritePlus(TNode node);
-  static RewriteResponse RewriteSub(TNode node);
-  static RewriteResponse RewriteNeg(TNode node);
-  static RewriteResponse RewriteUdiv(TNode node);
-  static RewriteResponse RewriteUrem(TNode node);
-  static RewriteResponse RewriteSmod(TNode node);
-  static RewriteResponse RewriteSdiv(TNode node);
-  static RewriteResponse RewriteSrem(TNode node);
-  static RewriteResponse RewriteShl(TNode node);
-  static RewriteResponse RewriteLshr(TNode node);
-  static RewriteResponse RewriteAshr(TNode node);
-  static RewriteResponse RewriteExtract(TNode node);
-  static RewriteResponse RewriteRepeat(TNode node);
-  static RewriteResponse RewriteZeroExtend(TNode node);
-  static RewriteResponse RewriteSignExtend(TNode node);
-  static RewriteResponse RewriteRotateRight(TNode node);
-  static RewriteResponse RewriteRotateLeft(TNode node);
+ static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteUlt(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteSlt(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteUle(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteSle(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteUgt(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteSgt(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteUge(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteSge(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteNot(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteConcat(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteAnd(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteOr(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteXnor(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteXor(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteNand(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteNor(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteComp(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteMult(TNode node, bool prerewrite = false);
+  static RewriteResponse RewritePlus(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteSub(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteNeg(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteUdiv(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteUrem(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteSmod(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteSdiv(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteSrem(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteShl(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteLshr(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteAshr(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteExtract(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteRepeat(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteZeroExtend(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteSignExtend(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false);
 
 public:
 
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 60e459958..8b5dd0499 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -79,6 +79,27 @@ inline Node mkAnd(std::vector<TNode>& children) {
   }
 }
 
+inline Node mkSortedNode(Kind kind, std::vector<Node>& children) {
+  Assert (kind == kind::BITVECTOR_PLUS ||
+          kind == kind::BITVECTOR_MULT ||
+          kind == kind::BITVECTOR_AND ||
+          kind == kind::BITVECTOR_OR ||
+          kind == kind::BITVECTOR_XOR);
+
+  if (children.size() == 1) {
+    return children[0]; 
+  }
+  std::sort(children.begin(), children.end());
+  return NodeManager::currentNM()->mkNode(kind, children);
+}
+
+
+inline Node mkNode(Kind kind, std::vector<Node>& children) {
+  if (children.size() == 1) {
+    return children[0]; 
+  }
+  return NodeManager::currentNM()->mkNode(kind, children);
+}
 
 inline Node mkNode(Kind kind, TNode child) {
   return NodeManager::currentNM()->mkNode(kind, child);
@@ -88,6 +109,21 @@ inline Node mkNode(Kind kind, TNode child1, TNode child2) {
   return NodeManager::currentNM()->mkNode(kind, child1, child2);
 }
 
+
+inline Node mkSortedNode(Kind kind, TNode child1, TNode child2) {
+  Assert (kind == kind::BITVECTOR_PLUS ||
+          kind == kind::BITVECTOR_MULT ||
+          kind == kind::BITVECTOR_AND ||
+          kind == kind::BITVECTOR_OR ||
+          kind == kind::BITVECTOR_XOR);
+  
+  if (child1 < child2) {
+    return NodeManager::currentNM()->mkNode(kind, child1, child2);
+  } else {
+    return NodeManager::currentNM()->mkNode(kind, child2, child1);
+  }
+}
+
 inline Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3) {
   return NodeManager::currentNM()->mkNode(kind, child1, child2, child3);
 }
@@ -156,8 +192,14 @@ inline Node mkConcat(TNode t1, TNode t2) {
     return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, t1, t2);
 }
 
+
+inline BitVector mkBitVectorOnes(unsigned size) {
+  Assert(size > 0); 
+  return BitVector(1, Integer(1)).signExtend(size - 1); 
+}
+
 inline Node mkOnes(unsigned size) {
-  BitVector val = BitVector(1, Integer(1)).signExtend(size-1);
+  BitVector val = mkBitVectorOnes(size); 
   return NodeManager::currentNM()->mkConst<BitVector>(val); 
 }
 
@@ -276,6 +318,7 @@ inline Node mkConjunction(const std::vector<TNode>& nodes) {
   std::vector<TNode>::const_iterator it_end = nodes.end();
   while (it != it_end) {
     TNode current = *it;
+
     if (current != mkTrue()) {
       Assert(isBVPredicate(current));
       expandedNodes.push_back(current);