From 5c61887222630583b48bd26fc914d166f122c252 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Mon, 28 May 2012 16:27:50 +0000
Subject: [PATCH] Added some BV rewrites, fixed bugs in array theory, made ite
 simp work with BV

---
 src/theory/arrays/theory_arrays.cpp           |  35 +-
 src/theory/arrays/theory_arrays.h             |   1 +
 src/theory/bv/bitblast_strategies.cpp         |   2 +-
 src/theory/bv/theory_bv_rewrite_rules.h       |  26 +-
 ...ory_bv_rewrite_rules_constant_evaluation.h |  92 ++--
 src/theory/bv/theory_bv_rewrite_rules_core.h  |  40 +-
 .../theory_bv_rewrite_rules_normalization.h   | 490 ++++++++++++++----
 ...ry_bv_rewrite_rules_operator_elimination.h |  76 +--
 .../theory_bv_rewrite_rules_simplification.h  | 164 +++---
 src/theory/bv/theory_bv_rewriter.cpp          |  26 +-
 src/theory/bv/theory_bv_utils.h               |   2 +-
 src/theory/ite_simplifier.cpp                 |  19 +-
 src/theory/ite_simplifier.h                   |   3 +-
 src/theory/rewriter.cpp                       |   4 +-
 src/theory/rewriter.h                         |   2 +-
 src/theory/theory_engine.cpp                  |   2 +-
 src/theory/theory_engine.h                    |   2 +-
 17 files changed, 652 insertions(+), 334 deletions(-)

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 15636fc72..cdc736d14 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -123,6 +123,13 @@ TheoryArrays::~TheoryArrays() {
 /////////////////////////////////////////////////////////////////////////////
 
 
+bool TheoryArrays::ppDisequal(TNode a, TNode b) {
+  bool termsExist = d_ppEqualityEngine.hasTerm(a) && d_ppEqualityEngine.hasTerm(b);
+  Assert(!termsExist || !a.isConst() || !b.isConst() || a == b || d_ppEqualityEngine.areDisequal(a, b, false));
+  return ((termsExist && d_ppEqualityEngine.areDisequal(a, b, false)) ||
+          Rewriter::rewrite(a.eqNode(b)) == d_false);
+}
+
 Node TheoryArrays::ppRewrite(TNode term) {
   if (!d_preprocess) return term;
   d_ppEqualityEngine.addTerm(term);
@@ -130,9 +137,7 @@ Node TheoryArrays::ppRewrite(TNode term) {
     case kind::SELECT: {
       // select(store(a,i,v),j) = select(a,j)
       //    IF i != j
-      if (term[0].getKind() == kind::STORE &&
-          (d_ppEqualityEngine.areDisequal(term[0][1], term[1], false) ||
-           (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) {
+      if (term[0].getKind() == kind::STORE && ppDisequal(term[0][1], term[1])) {
         return NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1];
       }
       break;
@@ -140,10 +145,7 @@ Node TheoryArrays::ppRewrite(TNode term) {
     case kind::STORE: {
       // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
       //    IF i != j and j comes before i in the ordering
-      if (term[0].getKind() == kind::STORE &&
-          (term[1] < term[0][1]) &&
-          (d_ppEqualityEngine.areDisequal(term[1], term[0][1], false) ||
-           (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) {
+      if (term[0].getKind() == kind::STORE && (term[1] < term[0][1]) && ppDisequal(term[1],term[0][1])) {
         Node inner = NodeBuilder<3>(kind::STORE) << term[0][0] << term[1] << term[2];
         Node outer = NodeBuilder<3>(kind::STORE) << inner << term[0][1] << term[0][2];
         return outer;
@@ -206,13 +208,11 @@ Node TheoryArrays::ppRewrite(TNode term) {
                 NodeBuilder<> hyp(kind::AND);
                 for (j = leftWrites - 1; j > i; --j) {
                   index_j = write_j[1];
-                  if (d_ppEqualityEngine.areDisequal(index_i, index_j, false) ||
-                      (index_i.isConst() && index_j.isConst() && index_i != index_j)) {
-                    continue;
+                  if (!ppDisequal(index_i, index_j)) {
+                    Node hyp2(index_i.getType() == nm->booleanType()? 
+                              index_i.iffNode(index_j) : index_i.eqNode(index_j));
+                    hyp << hyp2.notNode();
                   }
-                  Node hyp2(index_i.getType() == nm->booleanType()? 
-                            index_i.iffNode(index_j) : index_i.eqNode(index_j));
-                  hyp << hyp2.notNode();
                   write_j = write_j[0];
                 }
 
@@ -722,7 +722,7 @@ void TheoryArrays::check(Effort e) {
           d_equalityEngine.assertEquality(fact[0], false, fact);
 
           // Apply ArrDiseq Rule if diseq is between arrays
-          if(fact[0][0].getType().isArray()) {
+          if(fact[0][0].getType().isArray() && !d_conflict) {
             NodeManager* nm = NodeManager::currentNM();
             TypeNode indexType = fact[0][0].getType()[0];
             TNode k;
@@ -766,7 +766,7 @@ void TheoryArrays::check(Effort e) {
     // Otherwise we propagate
     propagate(e);
 
-    if(!d_eagerLemmas && fullEffort(e)) {
+    if(!d_eagerLemmas && fullEffort(e) && !d_conflict) {
       // generate the lemmas on the worklist
       Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
       dischargeLemmas();
@@ -916,6 +916,7 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b)
         e1 = e1[0];
       }
       Assert(d_equalityEngine.hasTerm(e1));
+      Assert(d_equalityEngine.hasTerm(b));
       if (d_equalityEngine.areEqual(e1, b)) {
         apply = true;
       }
@@ -1283,8 +1284,8 @@ void TheoryArrays::dischargeLemmas()
 
     // Check for redundant lemma
     // TODO: more checks possible (i.e. check d_RowAlreadyAdded in context)
-    if (d_equalityEngine.areEqual(i,j) ||
-        d_equalityEngine.areEqual(a,b) ||
+    if (!d_equalityEngine.hasTerm(i) || !d_equalityEngine.hasTerm(j) || d_equalityEngine.areEqual(i,j) ||
+        !d_equalityEngine.hasTerm(a) || !d_equalityEngine.hasTerm(b) || d_equalityEngine.areEqual(a,b) ||
         (ajExists && bjExists && d_equalityEngine.areEqual(aj,bj))) {
       d_RowQueue.push(l);
       continue;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 03d7e7d8d..d17caba45 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -141,6 +141,7 @@ class TheoryArrays : public Theory {
 
   Node preprocessTerm(TNode term);
   Node recursivePreprocessTerm(TNode term);
+  bool ppDisequal(TNode a, TNode b);
 
   public:
 
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index 6871a5421..c063245a5 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -39,7 +39,7 @@ Bits* rewriteBits(const Bits& bits) {
   return newbits;
 }
 
-Node rewrite(Node node) {
+Node rewrite(TNode node) {
   return Rewriter::rewrite(node); 
 }
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 343d4d1f1..620d33aea 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -150,6 +150,8 @@ enum RewriteRuleId {
   PlusCombineLikeTerms,
   MultSimplify,
   MultDistribConst,
+  SolveEq,
+  BitwiseEq,
   AndSimplify,
   OrSimplify,
   XorSimplify,
@@ -264,6 +266,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case PlusCombineLikeTerms: out << "PlusCombineLikeTerms"; return out;
   case MultSimplify: out << "MultSimplify"; return out;
   case MultDistribConst: out << "MultDistribConst"; return out;
+  case SolveEq : out << "SolveEq"; return out;
+  case BitwiseEq : out << "BitwiseEq"; return out;
   case NegMult : out << "NegMult"; return out;
   case NegSub : out << "NegSub"; return out;
   case AndSimplify : out << "AndSimplify"; return out;
@@ -314,7 +318,7 @@ class RewriteRule {
   // static RuleStatistics* s_statistics;
 
   /** Actually apply the rewrite rule */
-  static inline Node apply(Node node) {
+  static inline Node apply(TNode node) {
     Unreachable();
   }
 
@@ -335,12 +339,12 @@ public:
     
   }
 
-  static inline bool applies(Node node) {
+  static inline bool applies(TNode node) {
     Unreachable();
   }
 
   template<bool checkApplies>
-  static inline Node run(Node node) {
+  static inline Node run(TNode node) {
     if (!checkApplies || applies(node)) {
       BVDebug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ")" << std::endl;
       Assert(checkApplies || applies(node));
@@ -488,15 +492,17 @@ struct AllRewriteRules {
   RewriteRule<OrSimplify> rule109;
   RewriteRule<NegPlus> rule110;
   RewriteRule<BBPlusNeg> rule111;
+  RewriteRule<SolveEq> rule112;
+  RewriteRule<BitwiseEq> rule113;
 };
 
 template<> inline
-bool RewriteRule<EmptyRule>::applies(Node node) {
+bool RewriteRule<EmptyRule>::applies(TNode node) {
   return false;
 }
 
 template<> inline
-Node RewriteRule<EmptyRule>::apply(Node node) {
+Node RewriteRule<EmptyRule>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EmptyRule> for " << node.getKind() <<"\n"; 
   Unreachable();
   return node;
@@ -505,7 +511,7 @@ Node RewriteRule<EmptyRule>::apply(Node node) {
 template<Kind kind, RewriteRuleId rule>
 struct ApplyRuleToChildren {
 
-  static Node apply(Node node) {
+  static Node apply(TNode node) {
     if (node.getKind() != kind) {
       return RewriteRule<rule>::template run<true>(node);
     }
@@ -516,13 +522,13 @@ struct ApplyRuleToChildren {
     return result;
   }
 
-  static bool applies(Node node) {
+  static bool applies(TNode node) {
     if (node.getKind() == kind) return true;
     return RewriteRule<rule>::applies(node);
   }
 
   template <bool checkApplies>
-  static Node run(Node node) {
+  static Node run(TNode node) {
     if (!checkApplies || applies(node)) {
       return apply(node);
     } else {
@@ -554,7 +560,7 @@ template <
   typename R20 = RewriteRule<EmptyRule>
   >
 struct LinearRewriteStrategy {
-  static Node apply(Node node) {
+  static Node apply(TNode node) {
     Node current = node;
     if (R1::applies(current)) current  = R1::template run<false>(current);
     if (R2::applies(current)) current  = R2::template run<false>(current);
@@ -603,7 +609,7 @@ template <
   typename R20 = RewriteRule<EmptyRule>
   >
 struct FixpointRewriteStrategy {
-  static Node apply(Node node) {
+  static Node apply(TNode node) {
     Node previous = node; 
     Node current = node;
     do {
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 da3ef4485..c695d20ab 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -29,13 +29,13 @@ namespace theory {
 namespace bv {
 
 template<> inline
-bool RewriteRule<EvalAnd>::applies(Node node) {
+bool RewriteRule<EvalAnd>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_AND &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalAnd>::apply(Node node) {
+Node RewriteRule<EvalAnd>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalAnd>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -45,13 +45,13 @@ Node RewriteRule<EvalAnd>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<EvalOr>::applies(Node node) {
+bool RewriteRule<EvalOr>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_OR &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalOr>::apply(Node node) {
+Node RewriteRule<EvalOr>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalOr>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -61,13 +61,13 @@ Node RewriteRule<EvalOr>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<EvalXor>::applies(Node node) {
+bool RewriteRule<EvalXor>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_XOR &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalXor>::apply(Node node) {
+Node RewriteRule<EvalXor>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalXor>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -77,13 +77,13 @@ Node RewriteRule<EvalXor>::apply(Node node) {
 }
 
 // template<> inline
-// bool RewriteRule<EvalXnor>::applies(Node node) {
+// bool RewriteRule<EvalXnor>::applies(TNode node) {
 //   return (node.getKind() == kind::BITVECTOR_XNOR &&
 //           utils::isBVGroundTerm(node));
 // }
 
 // template<> inline
-// Node RewriteRule<EvalXnor>::apply(Node node) {
+// Node RewriteRule<EvalXnor>::apply(TNode node) {
 //   BVDebug("bv-rewrite") << "RewriteRule<EvalXnor>(" << node << ")" << std::endl;
 //   BitVector a = node[0].getConst<BitVector>();
 //   BitVector b = node[1].getConst<BitVector>();
@@ -92,13 +92,13 @@ Node RewriteRule<EvalXor>::apply(Node node) {
 //   return utils::mkConst(res);
 // }
 template<> inline
-bool RewriteRule<EvalNot>::applies(Node node) {
+bool RewriteRule<EvalNot>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_NOT &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalNot>::apply(Node node) {
+Node RewriteRule<EvalNot>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalNot>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector res = ~ a;  
@@ -106,13 +106,13 @@ Node RewriteRule<EvalNot>::apply(Node node) {
 }
 
 // template<> inline
-// bool RewriteRule<EvalComp>::applies(Node node) {
+// bool RewriteRule<EvalComp>::applies(TNode node) {
 //   return (node.getKind() == kind::BITVECTOR_COMP &&
 //           utils::isBVGroundTerm(node));
 // }
 
 // template<> inline
-// Node RewriteRule<EvalComp>::apply(Node node) {
+// Node RewriteRule<EvalComp>::apply(TNode node) {
 //   BVDebug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl;
 //   BitVector a = node[0].getConst<BitVector>();
 //   BitVector b = node[1].getConst<BitVector>();
@@ -127,13 +127,13 @@ Node RewriteRule<EvalNot>::apply(Node node) {
 // }
 
 template<> inline
-bool RewriteRule<EvalMult>::applies(Node node) {
+bool RewriteRule<EvalMult>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_MULT &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalMult>::apply(Node node) {
+Node RewriteRule<EvalMult>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalMult>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -143,13 +143,13 @@ Node RewriteRule<EvalMult>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<EvalPlus>::applies(Node node) {
+bool RewriteRule<EvalPlus>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_PLUS &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalPlus>::apply(Node node) {
+Node RewriteRule<EvalPlus>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalPlus>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -159,13 +159,13 @@ Node RewriteRule<EvalPlus>::apply(Node node) {
 }
 
 // template<> inline
-// bool RewriteRule<EvalSub>::applies(Node node) {
+// bool RewriteRule<EvalSub>::applies(TNode node) {
 //   return (node.getKind() == kind::BITVECTOR_SUB &&
 //           utils::isBVGroundTerm(node));
 // }
 
 // template<> inline
-// Node RewriteRule<EvalSub>::apply(Node node) {
+// Node RewriteRule<EvalSub>::apply(TNode node) {
 //   BVDebug("bv-rewrite") << "RewriteRule<EvalSub>(" << node << ")" << std::endl;
 //   BitVector a = node[0].getConst<BitVector>();
 //   BitVector b = node[1].getConst<BitVector>();
@@ -174,13 +174,13 @@ Node RewriteRule<EvalPlus>::apply(Node node) {
 //   return utils::mkConst(res);
 // }
 template<> inline
-bool RewriteRule<EvalNeg>::applies(Node node) {
+bool RewriteRule<EvalNeg>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_NEG &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalNeg>::apply(Node node) {
+Node RewriteRule<EvalNeg>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalNeg>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector res = - a;
@@ -188,13 +188,13 @@ Node RewriteRule<EvalNeg>::apply(Node node) {
   return utils::mkConst(res);
 }
 template<> inline
-bool RewriteRule<EvalUdiv>::applies(Node node) {
+bool RewriteRule<EvalUdiv>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_UDIV &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalUdiv>::apply(Node node) {
+Node RewriteRule<EvalUdiv>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -203,13 +203,13 @@ Node RewriteRule<EvalUdiv>::apply(Node node) {
   return utils::mkConst(res);
 }
 template<> inline
-bool RewriteRule<EvalUrem>::applies(Node node) {
+bool RewriteRule<EvalUrem>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_UREM &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalUrem>::apply(Node node) {
+Node RewriteRule<EvalUrem>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -218,13 +218,13 @@ Node RewriteRule<EvalUrem>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<EvalShl>::applies(Node node) {
+bool RewriteRule<EvalShl>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SHL &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalShl>::apply(Node node) {
+Node RewriteRule<EvalShl>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalShl>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -234,13 +234,13 @@ Node RewriteRule<EvalShl>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<EvalLshr>::applies(Node node) {
+bool RewriteRule<EvalLshr>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_LSHR &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalLshr>::apply(Node node) {
+Node RewriteRule<EvalLshr>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalLshr>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -250,13 +250,13 @@ Node RewriteRule<EvalLshr>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<EvalAshr>::applies(Node node) {
+bool RewriteRule<EvalAshr>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ASHR &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalAshr>::apply(Node node) {
+Node RewriteRule<EvalAshr>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalAshr>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -266,13 +266,13 @@ Node RewriteRule<EvalAshr>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<EvalUlt>::applies(Node node) {
+bool RewriteRule<EvalUlt>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULT &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalUlt>::apply(Node node) {
+Node RewriteRule<EvalUlt>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUlt>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -284,13 +284,13 @@ Node RewriteRule<EvalUlt>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<EvalSlt>::applies(Node node) {
+bool RewriteRule<EvalSlt>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SLT &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalSlt>::apply(Node node) {
+Node RewriteRule<EvalSlt>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalSlt>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -303,13 +303,13 @@ Node RewriteRule<EvalSlt>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<EvalUle>::applies(Node node) {
+bool RewriteRule<EvalUle>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULE &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalUle>::apply(Node node) {
+Node RewriteRule<EvalUle>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUle>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -321,13 +321,13 @@ Node RewriteRule<EvalUle>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<EvalSle>::applies(Node node) {
+bool RewriteRule<EvalSle>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SLE &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalSle>::apply(Node node) {
+Node RewriteRule<EvalSle>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalSle>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
@@ -339,13 +339,13 @@ Node RewriteRule<EvalSle>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<EvalExtract>::applies(Node node) {
+bool RewriteRule<EvalExtract>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalExtract>::apply(Node node) {
+Node RewriteRule<EvalExtract>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalExtract>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   unsigned lo = utils::getExtractLow(node);
@@ -357,13 +357,13 @@ Node RewriteRule<EvalExtract>::apply(Node node) {
 
 
 template<> inline
-bool RewriteRule<EvalConcat>::applies(Node node) {
+bool RewriteRule<EvalConcat>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_CONCAT &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalConcat>::apply(Node node) {
+Node RewriteRule<EvalConcat>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalConcat>(" << node << ")" << std::endl;
   unsigned num = node.getNumChildren();
   BitVector res = node[0].getConst<BitVector>();
@@ -375,13 +375,13 @@ Node RewriteRule<EvalConcat>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<EvalSignExtend>::applies(Node node) {
+bool RewriteRule<EvalSignExtend>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalSignExtend>::apply(Node node) {
+Node RewriteRule<EvalSignExtend>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalSignExtend>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount; 
@@ -391,13 +391,13 @@ Node RewriteRule<EvalSignExtend>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<EvalEquals>::applies(Node node) {
+bool RewriteRule<EvalEquals>::applies(TNode node) {
   return (node.getKind() == kind::EQUAL &&
           utils::isBVGroundTerm(node));
 }
 
 template<> inline
-Node RewriteRule<EvalEquals>::apply(Node node) {
+Node RewriteRule<EvalEquals>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalEquals>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].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 f3d28072e..2ccd0fbda 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -29,12 +29,12 @@ namespace theory {
 namespace bv {
 
 template<> inline
-bool RewriteRule<ConcatFlatten>::applies(Node node) {
+bool RewriteRule<ConcatFlatten>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_CONCAT);
 }
 
 template<> inline
-Node RewriteRule<ConcatFlatten>::apply(Node node) {
+Node RewriteRule<ConcatFlatten>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl;
   NodeBuilder<> result(kind::BITVECTOR_CONCAT);
   std::vector<Node> processing_stack;
@@ -55,12 +55,12 @@ Node RewriteRule<ConcatFlatten>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<ConcatExtractMerge>::applies(Node node) {
+bool RewriteRule<ConcatExtractMerge>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_CONCAT);
 }
 
 template<> inline
-Node RewriteRule<ConcatExtractMerge>::apply(Node node) {
+Node RewriteRule<ConcatExtractMerge>::apply(TNode node) {
 
   BVDebug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl;
 
@@ -116,12 +116,12 @@ Node RewriteRule<ConcatExtractMerge>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<ConcatConstantMerge>::applies(Node node) {
+bool RewriteRule<ConcatConstantMerge>::applies(TNode node) {
   return node.getKind() == kind::BITVECTOR_CONCAT;
 }
 
 template<> inline
-Node RewriteRule<ConcatConstantMerge>::apply(Node node) {
+Node RewriteRule<ConcatConstantMerge>::apply(TNode node) {
 
   BVDebug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl;
 
@@ -158,7 +158,7 @@ Node RewriteRule<ConcatConstantMerge>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<ExtractWhole>::applies(Node node) {
+bool RewriteRule<ExtractWhole>::applies(TNode node) {
   if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
   unsigned length = utils::getSize(node[0]);
   unsigned extractHigh = utils::getExtractHigh(node);
@@ -169,20 +169,20 @@ bool RewriteRule<ExtractWhole>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<ExtractWhole>::apply(Node node) {
+Node RewriteRule<ExtractWhole>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl;
   return node[0];
 }
 
 template<> inline
-bool RewriteRule<ExtractConstant>::applies(Node node) {
+bool RewriteRule<ExtractConstant>::applies(TNode node) {
   if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
   if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
   return true;
 }
 
 template<> inline
-Node RewriteRule<ExtractConstant>::apply(Node node) {
+Node RewriteRule<ExtractConstant>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl;
   Node child = node[0];
   BitVector childValue = child.getConst<BitVector>();
@@ -190,7 +190,7 @@ Node RewriteRule<ExtractConstant>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<ExtractConcat>::applies(Node node) {
+bool RewriteRule<ExtractConcat>::applies(TNode node) {
   //BVDebug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
   if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
   if (node[0].getKind() != kind::BITVECTOR_CONCAT) return false;
@@ -198,7 +198,7 @@ bool RewriteRule<ExtractConcat>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<ExtractConcat>::apply(Node node) {
+Node RewriteRule<ExtractConcat>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
   int extract_high = utils::getExtractHigh(node);
   int extract_low = utils::getExtractLow(node);
@@ -224,14 +224,14 @@ Node RewriteRule<ExtractConcat>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<ExtractExtract>::applies(Node node) {
+bool RewriteRule<ExtractExtract>::applies(TNode node) {
   if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
   if (node[0].getKind() != kind::BITVECTOR_EXTRACT) return false;
   return true;
 }
 
 template<> inline
-Node RewriteRule<ExtractExtract>::apply(Node node) {
+Node RewriteRule<ExtractExtract>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl;
 
   // x[i:j][k:l] ~>  x[k+j:l+j]
@@ -245,7 +245,7 @@ Node RewriteRule<ExtractExtract>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<FailEq>::applies(Node node) {
+bool RewriteRule<FailEq>::applies(TNode node) {
   //BVDebug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
   if (node.getKind() != kind::EQUAL) return false;
   if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
@@ -254,29 +254,29 @@ bool RewriteRule<FailEq>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<FailEq>::apply(Node node) {
+Node RewriteRule<FailEq>::apply(TNode node) {
   return utils::mkFalse();
 }
 
 template<> inline
-bool RewriteRule<SimplifyEq>::applies(Node node) {
+bool RewriteRule<SimplifyEq>::applies(TNode node) {
   if (node.getKind() != kind::EQUAL) return false;
   return node[0] == node[1];
 }
 
 template<> inline
-Node RewriteRule<SimplifyEq>::apply(Node node) {
+Node RewriteRule<SimplifyEq>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl;
   return utils::mkTrue();
 }
 
 template<> inline
-bool RewriteRule<ReflexivityEq>::applies(Node node) {
+bool RewriteRule<ReflexivityEq>::applies(TNode node) {
   return (node.getKind() == kind::EQUAL && node[0] < node[1]);
 }
 
 template<> inline
-Node RewriteRule<ReflexivityEq>::apply(Node node) {
+Node RewriteRule<ReflexivityEq>::apply(TNode 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 3a5a07f1c..5be052947 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -34,7 +34,7 @@ namespace bv {
  *  where bvop is bvand,bvor, bvxor
  */
 template<> inline
-bool RewriteRule<ExtractBitwise>::applies(Node node) {
+bool RewriteRule<ExtractBitwise>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
           (node[0].getKind() == kind::BITVECTOR_AND ||
            node[0].getKind() == kind::BITVECTOR_OR ||
@@ -42,7 +42,7 @@ bool RewriteRule<ExtractBitwise>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<ExtractBitwise>::apply(Node node) {
+Node RewriteRule<ExtractBitwise>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractBitwise>(" << node << ")" << std::endl;
   unsigned high = utils::getExtractHigh(node);
   unsigned low = utils::getExtractLow(node);
@@ -60,13 +60,13 @@ Node RewriteRule<ExtractBitwise>::apply(Node node) {
  *  (~ a) [i:j] ==> ~ (a[i:j])
  */
 template<> inline
-bool RewriteRule<ExtractNot>::applies(Node node) {
+bool RewriteRule<ExtractNot>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
           node[0].getKind() == kind::BITVECTOR_NOT);
 }
 
 template<> inline
-Node RewriteRule<ExtractNot>::apply(Node node) {
+Node RewriteRule<ExtractNot>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractNot>(" << node << ")" << std::endl;
   unsigned low = utils::getExtractLow(node);
   unsigned high = utils::getExtractHigh(node);
@@ -81,7 +81,7 @@ Node RewriteRule<ExtractNot>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<ExtractArith>::applies(Node node) {
+bool RewriteRule<ExtractArith>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
           utils::getExtractLow(node) == 0 &&
           (node[0].getKind() == kind::BITVECTOR_PLUS ||
@@ -89,7 +89,7 @@ bool RewriteRule<ExtractArith>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<ExtractArith>::apply(Node node) {
+Node RewriteRule<ExtractArith>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractArith>(" << node << ")" << std::endl;
   unsigned low = utils::getExtractLow(node);
   Assert (low == 0); 
@@ -111,14 +111,14 @@ Node RewriteRule<ExtractArith>::apply(Node node) {
 
 // careful not to apply in a loop 
 template<> inline
-bool RewriteRule<ExtractArith2>::applies(Node node) {
+bool RewriteRule<ExtractArith2>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_EXTRACT &&
           (node[0].getKind() == kind::BITVECTOR_PLUS ||
            node[0].getKind() == kind::BITVECTOR_MULT));
 }
 
 template<> inline
-Node RewriteRule<ExtractArith2>::apply(Node node) {
+Node RewriteRule<ExtractArith2>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<ExtractArith2>(" << node << ")" << std::endl;
   unsigned low = utils::getExtractLow(node);
   unsigned high = utils::getExtractHigh(node);
@@ -133,7 +133,7 @@ Node RewriteRule<ExtractArith2>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<FlattenAssocCommut>::applies(Node node) {
+bool RewriteRule<FlattenAssocCommut>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_PLUS ||
           node.getKind() == kind::BITVECTOR_MULT ||
           node.getKind() == kind::BITVECTOR_OR ||
@@ -143,7 +143,7 @@ bool RewriteRule<FlattenAssocCommut>::applies(Node node) {
 
 
 template<> inline
-Node RewriteRule<FlattenAssocCommut>::apply(Node node) {
+Node RewriteRule<FlattenAssocCommut>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl;
   std::vector<Node> processingStack;
   processingStack.push_back(node);
@@ -176,13 +176,83 @@ static inline void addToCoefMap(std::map<Node, BitVector>& map,
 }
 
 
+static inline void updateCoefMap(TNode current, unsigned size,
+                                 std::map<Node, BitVector>& factorToCoefficient,
+                                 BitVector& constSum) {
+  // 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)); 
+  }
+}
+
+
+static inline void addToChildren(TNode term, unsigned size, BitVector coeff, std::vector<Node>& children) {
+  if (coeff == BitVector(size, (unsigned)0)) {
+    return;
+  }
+  else if (coeff == BitVector(size, (unsigned)1)) {
+    children.push_back(term); 
+  }
+  else if (coeff == -BitVector(size, (unsigned)1)) {
+    // avoid introducing an extra multiplication
+    children.push_back(utils::mkNode(kind::BITVECTOR_NEG, term)); 
+  }
+  else {
+    Node coeffNode = utils::mkConst(coeff);
+    Node product = utils::mkSortedNode(kind::BITVECTOR_MULT, coeffNode, term); 
+    children.push_back(product); 
+  }
+}
+
+
 template<> inline
-bool RewriteRule<PlusCombineLikeTerms>::applies(Node node) {
+bool RewriteRule<PlusCombineLikeTerms>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_PLUS);
 }
 
+
 template<> inline
-Node RewriteRule<PlusCombineLikeTerms>::apply(Node node) {
+Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<PlusCombineLikeTerms>(" << node << ")" << std::endl;
   unsigned size = utils::getSize(node); 
   BitVector constSum(size, (unsigned)0); 
@@ -191,51 +261,7 @@ Node RewriteRule<PlusCombineLikeTerms>::apply(Node node) {
   // 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)); 
-    }
+    updateCoefMap(current, size, factorToCoefficient, constSum);
   }
     
   std::vector<Node> children; 
@@ -247,23 +273,7 @@ Node RewriteRule<PlusCombineLikeTerms>::apply(Node node) {
   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); 
-    }
+    addToChildren(it->first, size, it->second, children);
   }
 
   if(children.size() == 0) {
@@ -275,12 +285,12 @@ Node RewriteRule<PlusCombineLikeTerms>::apply(Node node) {
 
 
 template<> inline
-bool RewriteRule<MultSimplify>::applies(Node node) {
+bool RewriteRule<MultSimplify>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_MULT);
 }
 
 template<> inline
-Node RewriteRule<MultSimplify>::apply(Node node) {
+Node RewriteRule<MultSimplify>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<MultSimplify>(" << node << ")" << std::endl;
   unsigned size = utils::getSize(node); 
   BitVector constant(size, Integer(1));
@@ -313,7 +323,7 @@ Node RewriteRule<MultSimplify>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<MultDistribConst>::applies(Node node) {
+bool RewriteRule<MultDistribConst>::applies(TNode node) {
   if (node.getKind() != kind::BITVECTOR_MULT)
     return false;
 
@@ -332,7 +342,7 @@ bool RewriteRule<MultDistribConst>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<MultDistribConst>::apply(Node node) {
+Node RewriteRule<MultDistribConst>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<MultDistribConst>(" << node << ")" << std::endl;
 
   TNode constant;
@@ -364,12 +374,304 @@ Node RewriteRule<MultDistribConst>::apply(Node node) {
 }
 
 
+template<> inline
+bool RewriteRule<SolveEq>::applies(TNode node) {
+  if (node.getKind() != kind::EQUAL ||
+      (node[0].getMetaKind() == kind::metakind::VARIABLE && !node[1].hasSubterm(node[0])) ||
+      (node[1].getMetaKind() == kind::metakind::VARIABLE && !node[0].hasSubterm(node[1]))) {
+    return false;
+  }
+  return true;
+}
+
+
+// Doesn't do full solving (yet), instead, if a term appears both on lhs and rhs, it subtracts from both sides so that one side's coeff is zero
+template<> inline
+Node RewriteRule<SolveEq>::apply(TNode node) {
+  BVDebug("bv-rewrite") << "RewriteRule<SolveEq>(" << node << ")" << std::endl;
+
+  TNode left = node[0];
+  TNode right = node[1];
+
+  unsigned size = utils::getSize(left);
+  BitVector zero(size, (unsigned)0);
+  BitVector leftConst(size, (unsigned)0);
+  BitVector rightConst(size, (unsigned)0);
+  std::map<Node, BitVector> leftMap, rightMap;
+
+  // Collect terms and coefficients plus constant for left
+  if (left.getKind() == kind::BITVECTOR_PLUS) {
+    for(unsigned i= 0; i < left.getNumChildren(); ++i) {
+      updateCoefMap(left[i], size, leftMap, leftConst);
+    }
+  }
+  else {
+    updateCoefMap(left, size, leftMap, leftConst);
+  }
+
+  // Collect terms and coefficients plus constant for right
+  if (right.getKind() == kind::BITVECTOR_PLUS) {
+    for(unsigned i= 0; i < right.getNumChildren(); ++i) {
+      updateCoefMap(right[i], size, rightMap, rightConst);
+    }
+  }
+  else {
+    updateCoefMap(right, size, rightMap, rightConst);
+  }
+
+  std::vector<Node> childrenLeft, childrenRight;
+
+  // If both constants are nonzero, combine on right, otherwise leave them where they are
+  if (rightConst != zero) {
+    rightConst = rightConst - leftConst;
+    childrenRight.push_back(utils::mkConst(rightConst));
+  }
+  else if (leftConst != zero) {
+    childrenLeft.push_back(utils::mkConst(leftConst));
+  }
+
+  std::map<Node, BitVector>::const_iterator iLeft = leftMap.begin(), iLeftEnd = leftMap.end();
+  std::map<Node, BitVector>::const_iterator iRight = rightMap.begin(), iRightEnd = rightMap.end();
+
+  BitVector coeffLeft;
+  TNode termLeft;
+  if (iLeft != iLeftEnd) {
+    coeffLeft = iLeft->second;
+    termLeft = iLeft->first;
+  }
+
+  BitVector coeffRight;
+  TNode termRight;
+  if (iRight != iRightEnd) {
+    coeffRight = iRight->second;
+    termRight = iRight->first;
+  }
+
+  bool incLeft, incRight;
+
+  while (iLeft != iLeftEnd || iRight != iRightEnd) {
+    incLeft = incRight = false;
+    if (iLeft != iLeftEnd && (iRight == iRightEnd || termLeft < termRight)) {
+      addToChildren(termLeft, size, coeffLeft, childrenLeft);
+      incLeft = true;
+    }      
+    else if (iLeft == iLeftEnd || termRight < termLeft) {
+      Assert(iRight != iRightEnd);
+      addToChildren(termRight, size, coeffRight, childrenRight);
+      incRight = true;
+    }
+    else {
+      if (coeffLeft > coeffRight) {
+        addToChildren(termLeft, size, coeffLeft - coeffRight, childrenLeft);
+      }
+      else if (coeffRight > coeffLeft) {
+        addToChildren(termRight, size, coeffRight - coeffLeft, childrenRight);
+      }
+      incLeft = incRight = true;
+    }
+    if (incLeft) {
+      ++iLeft;
+      if (iLeft != iLeftEnd) {
+        coeffLeft = iLeft->second;
+        termLeft = iLeft->first;
+      }
+    }
+    if (incRight) {
+      ++iRight;
+      if (iRight != iRightEnd) {
+        coeffRight = iRight->second;
+        termRight = iRight->first;
+      }
+    }
+  }
+
+  // construct result 
+
+  Node newLeft, newRight;
+
+  if(childrenRight.size() == 0 && leftConst != zero) {
+    Assert(childrenLeft[0].isConst() && childrenLeft[0].getConst<BitVector>() == leftConst);
+    if (childrenLeft.size() == 1) {
+      // c = 0 ==> false
+      return utils::mkFalse();
+    }
+    // special case - if right is empty and left has a constant, move the constant
+    // TODO: this is inefficient - would be better if constant were at the end in the normal form
+    childrenRight.push_back(utils::mkConst(-leftConst));
+    childrenLeft.erase(childrenLeft.begin());
+  }
+
+  if(childrenLeft.size() == 0) {
+    if (rightConst != zero) {
+      Assert(childrenRight[0].isConst() && childrenRight[0].getConst<BitVector>() == rightConst);
+      if (childrenRight.size() == 1) {
+        // 0 = c ==> false
+        return utils::mkFalse();
+      }
+      // special case - if left is empty and right has a constant, move the constant
+      // TODO: this is inefficient - would be better if constant were at the end in the normal form
+      newLeft = utils::mkConst(-rightConst);
+      childrenRight.erase(childrenRight.begin());
+    }
+    else {
+      newLeft = utils::mkConst(size, (unsigned)0); 
+    }
+  }
+  else if (childrenLeft.size() == 1) {
+    newLeft = childrenLeft[0];
+  }
+  else {
+    newLeft = utils::mkSortedNode(kind::BITVECTOR_PLUS, childrenLeft);
+  }
+
+  if (childrenRight.size() == 0) {
+    newRight = utils::mkConst(size, (unsigned)0);
+  }
+  else if (childrenRight.size() == 1) {
+    newRight = childrenRight[0];
+  }
+  else {
+    newRight = utils::mkSortedNode(kind::BITVECTOR_PLUS, childrenRight);
+  }
+
+  if (newLeft == newRight) {
+    Assert (newLeft == utils::mkConst(size, (unsigned)0));
+    return utils::mkTrue();
+  }
+
+  if (newLeft < newRight) {
+    return newRight.eqNode(newLeft);
+  }
+  
+  return newLeft.eqNode(newRight);
+}
+
+
+template<> inline
+bool RewriteRule<BitwiseEq>::applies(TNode node) {
+  if (node.getKind() != kind::EQUAL ||
+      utils::getSize(node[0]) != 1) {
+    return false;
+  }
+  TNode term;
+  BitVector c;
+  if (node[0].getKind() == kind::CONST_BITVECTOR) {
+    c = node[0].getConst<BitVector>();
+    term = node[1];
+  }
+  else if (node[1].getKind() == kind::CONST_BITVECTOR) {
+    c = node[1].getConst<BitVector>();
+    term = node[0];
+  }
+  else {
+    return false;
+  }
+  switch (term.getKind()) {
+    case kind::BITVECTOR_AND:
+    case kind::BITVECTOR_OR:
+      //operator BITVECTOR_XOR 2: "bitwise xor"
+    case kind::BITVECTOR_NOT:
+    case kind::BITVECTOR_NAND:
+    case kind::BITVECTOR_NOR:
+      //operator BITVECTOR_XNOR 2 "bitwise xnor"
+    case kind::BITVECTOR_COMP:
+    case kind::BITVECTOR_NEG:
+      return true;
+      break;
+    default:
+      break;
+  }
+  return false;
+}
+
+
+static inline Node mkNodeKind(Kind k, TNode node, TNode c) {
+  unsigned i = 0;
+  unsigned nc = node.getNumChildren();
+  NodeBuilder<> nb(k);
+  for(; i < nc; ++i) {
+    nb << node[i].eqNode(c);
+  }
+  return nb;
+}
+
+
+template<> inline
+Node RewriteRule<BitwiseEq>::apply(TNode node) {
+  BVDebug("bv-rewrite") << "RewriteRule<BitwiseEq>(" << node << ")" << std::endl;
+
+  TNode term;
+  BitVector c;
+
+  if (node[0].getKind() == kind::CONST_BITVECTOR) {
+    c = node[0].getConst<BitVector>();
+    term = node[1];
+  }
+  else if (node[1].getKind() == kind::CONST_BITVECTOR) {
+    c = node[1].getConst<BitVector>();
+    term = node[0];
+  }
+
+  bool eqOne = (c == BitVector(1,(unsigned)1));
+
+  switch (term.getKind()) {
+    case kind::BITVECTOR_AND:
+      if (eqOne) {
+        return mkNodeKind(kind::AND, term, utils::mkConst(1, (unsigned)1));
+      }
+      else {
+        return mkNodeKind(kind::OR, term, utils::mkConst(1, (unsigned)0));
+      }
+      break;
+    case kind::BITVECTOR_NAND:
+      if (eqOne) {
+        return mkNodeKind(kind::OR, term, utils::mkConst(1, (unsigned)0));
+      }
+      else {
+        return mkNodeKind(kind::AND, term, utils::mkConst(1, (unsigned)1));
+      }
+      break;
+    case kind::BITVECTOR_OR:
+      if (eqOne) {
+        return mkNodeKind(kind::OR, term, utils::mkConst(1, (unsigned)1));
+      }
+      else {
+        return mkNodeKind(kind::AND, term, utils::mkConst(1, (unsigned)0));
+      }
+      break;
+    case kind::BITVECTOR_NOR:
+      if (eqOne) {
+        return mkNodeKind(kind::AND, term, utils::mkConst(1, (unsigned)0));
+      }
+      else {
+        return mkNodeKind(kind::OR, term, utils::mkConst(1, (unsigned)1));
+      }
+      break;
+    case kind::BITVECTOR_NOT:
+      return term[0].eqNode(utils::mkConst(~c));
+    case kind::BITVECTOR_COMP:
+      Assert(term.getNumChildren() == 2);
+      if (eqOne) {
+        return term[0].eqNode(term[1]);
+      }
+      else {
+        return term[0].eqNode(term[1]).notNode();
+      }
+    case kind::BITVECTOR_NEG:
+      return term[0].eqNode(utils::mkConst(c));
+    default:
+      break;
+  }
+  Unreachable();
+}
+
+
 /**
  * -(c * expr) ==> (-c * expr)
  * where c is a constant
  */
 template<> inline
-bool RewriteRule<NegMult>::applies(Node node) {
+bool RewriteRule<NegMult>::applies(TNode node) {
   if(node.getKind()!= kind::BITVECTOR_NEG ||
      node[0].getKind() != kind::BITVECTOR_MULT) {
     return false; 
@@ -384,7 +686,7 @@ bool RewriteRule<NegMult>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<NegMult>::apply(Node node) {
+Node RewriteRule<NegMult>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl;
   TNode mult = node[0];
   std::vector<Node> children;
@@ -401,25 +703,25 @@ Node RewriteRule<NegMult>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<NegSub>::applies(Node node) {
+bool RewriteRule<NegSub>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_NEG &&
           node[0].getKind() == kind::BITVECTOR_SUB);
 }
 
 template<> inline
-Node RewriteRule<NegSub>::apply(Node node) {
+Node RewriteRule<NegSub>::apply(TNode 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) {
+bool RewriteRule<NegPlus>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_NEG &&
           node[0].getKind() == kind::BITVECTOR_PLUS);
 }
 
 template<> inline
-Node RewriteRule<NegPlus>::apply(Node node) {
+Node RewriteRule<NegPlus>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<NegPlus>(" << node << ")" << std::endl;
   std::vector<Node> children;
   for (unsigned i = 0; i < node[0].getNumChildren(); ++i) {
@@ -455,12 +757,12 @@ inline static void insert(std::hash_map<TNode, Count, TNodeHashFunction>& map, T
 }
 
 template<> inline
-bool RewriteRule<AndSimplify>::applies(Node node) {
+bool RewriteRule<AndSimplify>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_AND);
 }
 
 template<> inline
-Node RewriteRule<AndSimplify>::apply(Node node) {
+Node RewriteRule<AndSimplify>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
 
   // this will remove duplicates
@@ -518,12 +820,12 @@ Node RewriteRule<AndSimplify>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<OrSimplify>::applies(Node node) {
+bool RewriteRule<OrSimplify>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_OR);
 }
 
 template<> inline
-Node RewriteRule<OrSimplify>::apply(Node node) {
+Node RewriteRule<OrSimplify>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl;
 
   // this will remove duplicates
@@ -581,12 +883,12 @@ Node RewriteRule<OrSimplify>::apply(Node node) {
 }
 
 template<> inline
-bool RewriteRule<XorSimplify>::applies(Node node) {
+bool RewriteRule<XorSimplify>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_XOR);
 }
 
 template<> inline
-Node RewriteRule<XorSimplify>::apply(Node node) {
+Node RewriteRule<XorSimplify>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl;
 
 
@@ -676,24 +978,24 @@ Node RewriteRule<XorSimplify>::apply(Node node) {
 
 
 // template<> inline
-// bool RewriteRule<AndSimplify>::applies(Node node) {
+// bool RewriteRule<AndSimplify>::applies(TNode node) {
 //   return (node.getKind() == kind::BITVECTOR_AND);
 // }
 
 // template<> inline
-// Node RewriteRule<AndSimplify>::apply(Node node) {
+// Node RewriteRule<AndSimplify>::apply(TNode node) {
 //   BVDebug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
 //   return resultNode;
 // }
 
 
 // template<> inline
-// bool RewriteRule<>::applies(Node node) {
+// bool RewriteRule<>::applies(TNode node) {
 //   return (node.getKind() == kind::BITVECTOR_CONCAT);
 // }
 
 // template<> inline
-// Node RewriteRule<>::apply(Node node) {
+// Node RewriteRule<>::apply(TNode node) {
 //   BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl;
 //   return resultNode;
 // }
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index f0460643b..252dc4799 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -29,12 +29,12 @@ namespace theory {
 namespace bv {
 
 template<>
-bool RewriteRule<UgtEliminate>::applies(Node node) {
+bool RewriteRule<UgtEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_UGT);
 }
 
 template<>
-Node RewriteRule<UgtEliminate>::apply(Node node) {
+Node RewriteRule<UgtEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<UgtEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1];
@@ -44,12 +44,12 @@ Node RewriteRule<UgtEliminate>::apply(Node node) {
 
 
 template<>
-bool RewriteRule<UgeEliminate>::applies(Node node) {
+bool RewriteRule<UgeEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_UGE);
 }
 
 template<>
-Node RewriteRule<UgeEliminate>::apply(Node node) {
+Node RewriteRule<UgeEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<UgeEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1];
@@ -59,12 +59,12 @@ Node RewriteRule<UgeEliminate>::apply(Node node) {
 
 
 template<>
-bool RewriteRule<SgtEliminate>::applies(Node node) {
+bool RewriteRule<SgtEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SGT);
 }
 
 template<>
-Node RewriteRule<SgtEliminate>::apply(Node node) {
+Node RewriteRule<SgtEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RgewriteRule<UgtEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1];
@@ -74,12 +74,12 @@ Node RewriteRule<SgtEliminate>::apply(Node node) {
 
 
 template<>
-bool RewriteRule<SgeEliminate>::applies(Node node) {
+bool RewriteRule<SgeEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SGE);
 }
 
 template<>
-Node RewriteRule<SgeEliminate>::apply(Node node) {
+Node RewriteRule<SgeEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<SgeEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1];
@@ -88,12 +88,12 @@ Node RewriteRule<SgeEliminate>::apply(Node node) {
 }
 
 template <>
-bool RewriteRule<SltEliminate>::applies(Node node) {
+bool RewriteRule<SltEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SLT); 
 }
 
 template <>
-Node RewriteRule<SltEliminate>::apply(Node node) {
+Node RewriteRule<SltEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<SltEliminate>(" << node << ")" << std::endl;
   
   unsigned size = utils::getSize(node[0]);
@@ -106,12 +106,12 @@ Node RewriteRule<SltEliminate>::apply(Node node) {
 }
 
 template <>
-bool RewriteRule<SleEliminate>::applies(Node node) {
+bool RewriteRule<SleEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SLE); 
 }
 
 template <>
-Node RewriteRule<SleEliminate>::apply(Node node) {
+Node RewriteRule<SleEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")" << std::endl;
   
   unsigned size = utils::getSize(node[0]);
@@ -124,12 +124,12 @@ Node RewriteRule<SleEliminate>::apply(Node node) {
 }
 
 template <>
-bool RewriteRule<CompEliminate>::applies(Node node) {
+bool RewriteRule<CompEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_COMP); 
 }
 
 template <>
-Node RewriteRule<CompEliminate>::apply(Node node) {
+Node RewriteRule<CompEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<CompEliminate>(" << node << ")" << std::endl;
   Node comp = utils::mkNode(kind::EQUAL, node[0], node[1]);
   Node one = utils::mkConst(1, 1);
@@ -139,12 +139,12 @@ Node RewriteRule<CompEliminate>::apply(Node node) {
 }
 
 template <>
-bool RewriteRule<SubEliminate>::applies(Node node) {
+bool RewriteRule<SubEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SUB); 
 }
 
 template <>
-Node RewriteRule<SubEliminate>::apply(Node node) {
+Node RewriteRule<SubEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<SubEliminate>(" << node << ")" << std::endl;
   Node negb = utils::mkNode(kind::BITVECTOR_NEG, node[1]);
   Node a = node[0];
@@ -154,12 +154,12 @@ Node RewriteRule<SubEliminate>::apply(Node node) {
 
 
 template<>
-bool RewriteRule<RepeatEliminate>::applies(Node node) {
+bool RewriteRule<RepeatEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_REPEAT);
 }
 
 template<>
-Node RewriteRule<RepeatEliminate>::apply(Node node) {
+Node RewriteRule<RepeatEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<RepeatEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned amount = node.getOperator().getConst<BitVectorRepeat>().repeatAmount;
@@ -176,12 +176,12 @@ Node RewriteRule<RepeatEliminate>::apply(Node node) {
 }
 
 template<>
-bool RewriteRule<RotateLeftEliminate>::applies(Node node) {
+bool RewriteRule<RotateLeftEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ROTATE_LEFT);
 }
 
 template<>
-Node RewriteRule<RotateLeftEliminate>::apply(Node node) {
+Node RewriteRule<RotateLeftEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<RotateLeftEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned amount = node.getOperator().getConst<BitVectorRotateLeft>().rotateLeftAmount;
@@ -198,12 +198,12 @@ Node RewriteRule<RotateLeftEliminate>::apply(Node node) {
 }
 
 template<>
-bool RewriteRule<RotateRightEliminate>::applies(Node node) {
+bool RewriteRule<RotateRightEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ROTATE_RIGHT);
 }
 
 template<>
-Node RewriteRule<RotateRightEliminate>::apply(Node node) {
+Node RewriteRule<RotateRightEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<RotateRightEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned amount = node.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount;
@@ -220,12 +220,12 @@ Node RewriteRule<RotateRightEliminate>::apply(Node node) {
 }
 
 template<>
-bool RewriteRule<NandEliminate>::applies(Node node) {
+bool RewriteRule<NandEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_NAND);
 }
 
 template<>
-Node RewriteRule<NandEliminate>::apply(Node node) {
+Node RewriteRule<NandEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<NandEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1]; 
@@ -235,12 +235,12 @@ Node RewriteRule<NandEliminate>::apply(Node node) {
 }
 
 template<>
-bool RewriteRule<NorEliminate>::applies(Node node) {
+bool RewriteRule<NorEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_NOR);
 }
 
 template<>
-Node RewriteRule<NorEliminate>::apply(Node node) {
+Node RewriteRule<NorEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<NorEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1]; 
@@ -250,12 +250,12 @@ Node RewriteRule<NorEliminate>::apply(Node node) {
 }
 
 template<>
-bool RewriteRule<XnorEliminate>::applies(Node node) {
+bool RewriteRule<XnorEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_XNOR);
 }
 
 template<>
-Node RewriteRule<XnorEliminate>::apply(Node node) {
+Node RewriteRule<XnorEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<XnorEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1]; 
@@ -265,12 +265,12 @@ Node RewriteRule<XnorEliminate>::apply(Node node) {
 
 
 template<>
-bool RewriteRule<SdivEliminate>::applies(Node node) {
+bool RewriteRule<SdivEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SDIV);
 }
 
 template<>
-Node RewriteRule<SdivEliminate>::apply(Node node) {
+Node RewriteRule<SdivEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<SdivEliminate>(" << node << ")" << std::endl;
 
   TNode a = node[0];
@@ -294,12 +294,12 @@ Node RewriteRule<SdivEliminate>::apply(Node node) {
 
 
 template<>
-bool RewriteRule<SremEliminate>::applies(Node node) {
+bool RewriteRule<SremEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SREM);
 }
 
 template<>
-Node RewriteRule<SremEliminate>::apply(Node node) {
+Node RewriteRule<SremEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<SremEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1];
@@ -320,12 +320,12 @@ Node RewriteRule<SremEliminate>::apply(Node node) {
 }
 
 template<>
-bool RewriteRule<SmodEliminate>::applies(Node node) {
+bool RewriteRule<SmodEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SMOD);
 }
 
 template<>
-Node RewriteRule<SmodEliminate>::apply(Node node) {
+Node RewriteRule<SmodEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   TNode b = node[1];
@@ -359,12 +359,12 @@ Node RewriteRule<SmodEliminate>::apply(Node node) {
 
 
 template<>
-bool RewriteRule<ZeroExtendEliminate>::applies(Node node) {
+bool RewriteRule<ZeroExtendEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ZERO_EXTEND); 
 }
 
 template<>
-Node RewriteRule<ZeroExtendEliminate>::apply(Node node) {
+Node RewriteRule<ZeroExtendEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<ZeroExtendEliminate>(" << node << ")" << std::endl;
 
   TNode bv = node[0];
@@ -379,12 +379,12 @@ Node RewriteRule<ZeroExtendEliminate>::apply(Node node) {
 }
 
 template<>
-bool RewriteRule<SignExtendEliminate>::applies(Node node) {
+bool RewriteRule<SignExtendEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND); 
 }
 
 template<>
-Node RewriteRule<SignExtendEliminate>::apply(Node node) {
+Node RewriteRule<SignExtendEliminate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<SignExtendEliminate>(" << node << ")" << std::endl;
 
   unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 490b413db..ee0e0fc43 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -37,14 +37,14 @@ namespace bv {
  * Left Shift by constant amount 
  */
 template<> inline
-bool RewriteRule<ShlByConst>::applies(Node node) {
+bool RewriteRule<ShlByConst>::applies(TNode node) {
   // if the shift amount is constant
   return (node.getKind() == kind::BITVECTOR_SHL &&
           node[1].getKind() == kind::CONST_BITVECTOR);
 }
 
 template<> inline
-Node RewriteRule<ShlByConst>::apply(Node node) {
+Node RewriteRule<ShlByConst>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl;
   Integer amount = node[1].getConst<BitVector>().toInteger();
   
@@ -73,14 +73,14 @@ Node RewriteRule<ShlByConst>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<LshrByConst>::applies(Node node) {
+bool RewriteRule<LshrByConst>::applies(TNode node) {
   // if the shift amount is constant
   return (node.getKind() == kind::BITVECTOR_LSHR &&
           node[1].getKind() == kind::CONST_BITVECTOR);
 }
 
 template<> inline
-Node RewriteRule<LshrByConst>::apply(Node node) {
+Node RewriteRule<LshrByConst>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl;
   Integer amount = node[1].getConst<BitVector>().toInteger();
   
@@ -109,14 +109,14 @@ Node RewriteRule<LshrByConst>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<AshrByConst>::applies(Node node) {
+bool RewriteRule<AshrByConst>::applies(TNode node) {
   // if the shift amount is constant
   return (node.getKind() == kind::BITVECTOR_ASHR &&
           node[1].getKind() == kind::CONST_BITVECTOR);
 }
 
 template<> inline
-Node RewriteRule<AshrByConst>::apply(Node node) {
+Node RewriteRule<AshrByConst>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl;
   Integer amount = node[1].getConst<BitVector>().toInteger();
   
@@ -151,14 +151,14 @@ Node RewriteRule<AshrByConst>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<BitwiseIdemp>::applies(Node node) {
+bool RewriteRule<BitwiseIdemp>::applies(TNode node) {
   return ((node.getKind() == kind::BITVECTOR_AND ||
            node.getKind() == kind::BITVECTOR_OR) &&
           node[0] == node[1]);
 }
 
 template<> inline
-Node RewriteRule<BitwiseIdemp>::apply(Node node) {
+Node RewriteRule<BitwiseIdemp>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl;
   return node[0]; 
 }
@@ -170,7 +170,7 @@ Node RewriteRule<BitwiseIdemp>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<AndZero>::applies(Node node) {
+bool RewriteRule<AndZero>::applies(TNode node) {
   unsigned size = utils::getSize(node); 
   return (node.getKind() == kind::BITVECTOR_AND  &&
           (node[0] == utils::mkConst(size, 0) ||
@@ -178,7 +178,7 @@ bool RewriteRule<AndZero>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<AndZero>::apply(Node node) {
+Node RewriteRule<AndZero>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 0); 
 }
@@ -190,7 +190,7 @@ Node RewriteRule<AndZero>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<AndOne>::applies(Node node) {
+bool RewriteRule<AndOne>::applies(TNode node) {
   unsigned size = utils::getSize(node);
   Node ones = utils::mkOnes(size); 
   return (node.getKind() == kind::BITVECTOR_AND  &&
@@ -199,7 +199,7 @@ bool RewriteRule<AndOne>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<AndOne>::apply(Node node) {
+Node RewriteRule<AndOne>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl;
   unsigned size = utils::getSize(node);
   
@@ -218,7 +218,7 @@ Node RewriteRule<AndOne>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<OrZero>::applies(Node node) {
+bool RewriteRule<OrZero>::applies(TNode node) {
   unsigned size = utils::getSize(node); 
   return (node.getKind() == kind::BITVECTOR_OR  &&
           (node[0] == utils::mkConst(size, 0) ||
@@ -226,7 +226,7 @@ bool RewriteRule<OrZero>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<OrZero>::apply(Node node) {
+Node RewriteRule<OrZero>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl;
   
   unsigned size = utils::getSize(node); 
@@ -245,7 +245,7 @@ Node RewriteRule<OrZero>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<OrOne>::applies(Node node) {
+bool RewriteRule<OrOne>::applies(TNode node) {
   unsigned size = utils::getSize(node);
   Node ones = utils::mkOnes(size); 
   return (node.getKind() == kind::BITVECTOR_OR  &&
@@ -254,7 +254,7 @@ bool RewriteRule<OrOne>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<OrOne>::apply(Node node) {
+Node RewriteRule<OrOne>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl;
   return utils::mkOnes(utils::getSize(node)); 
 }
@@ -267,13 +267,13 @@ Node RewriteRule<OrOne>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<XorDuplicate>::applies(Node node) {
+bool RewriteRule<XorDuplicate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_XOR &&
           node[0] == node[1]);
 }
 
 template<> inline
-Node RewriteRule<XorDuplicate>::apply(Node node) {
+Node RewriteRule<XorDuplicate>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl;
   return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); 
 }
@@ -285,7 +285,7 @@ Node RewriteRule<XorDuplicate>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<XorOne>::applies(Node node) {
+bool RewriteRule<XorOne>::applies(TNode node) {
   if (node.getKind() != kind::BITVECTOR_XOR) {
     return false; 
   }
@@ -299,7 +299,7 @@ bool RewriteRule<XorOne>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<XorOne>::apply(Node node) {
+Node RewriteRule<XorOne>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl;
   Node ones = utils::mkOnes(utils::getSize(node)); 
   std::vector<Node> children;
@@ -329,7 +329,7 @@ Node RewriteRule<XorOne>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<XorZero>::applies(Node node) {
+bool RewriteRule<XorZero>::applies(TNode node) {
   if (node.getKind() != kind::BITVECTOR_XOR) {
     return false; 
   }
@@ -343,7 +343,7 @@ bool RewriteRule<XorZero>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<XorZero>::apply(Node node) {
+Node RewriteRule<XorZero>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl;
   std::vector<Node> children;
   Node zero = utils::mkConst(utils::getSize(node), 0);
@@ -366,14 +366,14 @@ Node RewriteRule<XorZero>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<BitwiseNotAnd>::applies(Node node) {
+bool RewriteRule<BitwiseNotAnd>::applies(TNode 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<> inline
-Node RewriteRule<BitwiseNotAnd>::apply(Node node) {
+Node RewriteRule<BitwiseNotAnd>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl;
   return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); 
 }
@@ -385,14 +385,14 @@ Node RewriteRule<BitwiseNotAnd>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<BitwiseNotOr>::applies(Node node) {
+bool RewriteRule<BitwiseNotOr>::applies(TNode 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<> inline
-Node RewriteRule<BitwiseNotOr>::apply(Node node) {
+Node RewriteRule<BitwiseNotOr>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl;
   uint32_t size = utils::getSize(node);
   Integer ones = Integer(1).multiplyByPow2(size) - 1; 
@@ -406,14 +406,14 @@ Node RewriteRule<BitwiseNotOr>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<XorNot>::applies(Node node) {
+bool RewriteRule<XorNot>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_XOR &&
           node[0].getKind() == kind::BITVECTOR_NOT &&
           node[1].getKind() == kind::BITVECTOR_NOT); 
 }
 
 template<> inline
-Node RewriteRule<XorNot>::apply(Node node) {
+Node RewriteRule<XorNot>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
   Node a = node[0][0];
   Node b = node[1][0]; 
@@ -427,13 +427,13 @@ Node RewriteRule<XorNot>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<NotXor>::applies(Node node) {
+bool RewriteRule<NotXor>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_NOT &&
           node[0].getKind() == kind::BITVECTOR_XOR); 
 }
 
 template<> inline
-Node RewriteRule<NotXor>::apply(Node node) {
+Node RewriteRule<NotXor>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl;
   Node a = node[0][0];
   Node b = node[0][1];
@@ -448,13 +448,13 @@ Node RewriteRule<NotXor>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<NotIdemp>::applies(Node node) {
+bool RewriteRule<NotIdemp>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_NOT &&
           node[0].getKind() == kind::BITVECTOR_NOT); 
 }
 
 template<> inline
-Node RewriteRule<NotIdemp>::apply(Node node) {
+Node RewriteRule<NotIdemp>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<XorIdemp>(" << node << ")" << std::endl;
   return node[0][0];
 }
@@ -468,14 +468,14 @@ Node RewriteRule<NotIdemp>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<LtSelf>::applies(Node node) {
+bool RewriteRule<LtSelf>::applies(TNode node) {
   return ((node.getKind() == kind::BITVECTOR_ULT ||
            node.getKind() == kind::BITVECTOR_SLT) &&
           node[0] == node[1]);
 }
 
 template<> inline
-Node RewriteRule<LtSelf>::apply(Node node) {
+Node RewriteRule<LtSelf>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<LtSelf>(" << node << ")" << std::endl;
   return utils::mkFalse(); 
 }
@@ -487,14 +487,14 @@ Node RewriteRule<LtSelf>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<LteSelf>::applies(Node node) {
+bool RewriteRule<LteSelf>::applies(TNode node) {
   return ((node.getKind() == kind::BITVECTOR_ULE ||
            node.getKind() == kind::BITVECTOR_SLE) &&
           node[0] == node[1]);
 }
 
 template<> inline
-Node RewriteRule<LteSelf>::apply(Node node) {
+Node RewriteRule<LteSelf>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<LteSelf>(" << node << ")" << std::endl;
   return utils::mkTrue(); 
 }
@@ -506,13 +506,13 @@ Node RewriteRule<LteSelf>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<UltZero>::applies(Node node) {
+bool RewriteRule<UltZero>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULT &&
           node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
 }
 
 template<> inline
-Node RewriteRule<UltZero>::apply(Node node) {
+Node RewriteRule<UltZero>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
   return utils::mkFalse(); 
 }
@@ -524,13 +524,13 @@ Node RewriteRule<UltZero>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<UltSelf>::applies(Node node) {
+bool RewriteRule<UltSelf>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULT &&
           node[1] == node[0]); 
 }
 
 template<> inline
-Node RewriteRule<UltSelf>::apply(Node node) {
+Node RewriteRule<UltSelf>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<UltSelf>(" << node << ")" << std::endl;
   return utils::mkFalse(); 
 }
@@ -543,13 +543,13 @@ Node RewriteRule<UltSelf>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<UleZero>::applies(Node node) {
+bool RewriteRule<UleZero>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULE &&
           node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
 }
 
 template<> inline
-Node RewriteRule<UleZero>::apply(Node node) {
+Node RewriteRule<UleZero>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl;
   return utils::mkNode(kind::EQUAL, node[0], node[1]); 
 }
@@ -561,13 +561,13 @@ Node RewriteRule<UleZero>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<UleSelf>::applies(Node node) {
+bool RewriteRule<UleSelf>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULE &&
           node[1] == node[0]); 
 }
 
 template<> inline
-Node RewriteRule<UleSelf>::apply(Node node) {
+Node RewriteRule<UleSelf>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<UleSelf>(" << node << ")" << std::endl;
   return utils::mkTrue(); 
 }
@@ -580,13 +580,13 @@ Node RewriteRule<UleSelf>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<ZeroUle>::applies(Node node) {
+bool RewriteRule<ZeroUle>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_ULE &&
           node[0] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
 }
 
 template<> inline
-Node RewriteRule<ZeroUle>::apply(Node node) {
+Node RewriteRule<ZeroUle>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node << ")" << std::endl;
   return utils::mkTrue(); 
 }
@@ -598,7 +598,7 @@ Node RewriteRule<ZeroUle>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<UleMax>::applies(Node node) {
+bool RewriteRule<UleMax>::applies(TNode node) {
   if (node.getKind()!= kind::BITVECTOR_ULE) {
     return false; 
   }
@@ -609,7 +609,7 @@ bool RewriteRule<UleMax>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<UleMax>::apply(Node node) {
+Node RewriteRule<UleMax>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<UleMax>(" << node << ")" << std::endl;
   return utils::mkTrue(); 
 }
@@ -621,13 +621,13 @@ Node RewriteRule<UleMax>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<NotUlt>::applies(Node node) {
+bool RewriteRule<NotUlt>::applies(TNode node) {
   return (node.getKind() == kind::NOT &&
           node[0].getKind() == kind::BITVECTOR_ULT);
 }
 
 template<> inline
-Node RewriteRule<NotUlt>::apply(Node node) {
+Node RewriteRule<NotUlt>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl;
   Node ult = node[0];
   Node a = ult[0];
@@ -642,13 +642,13 @@ Node RewriteRule<NotUlt>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<NotUle>::applies(Node node) {
+bool RewriteRule<NotUle>::applies(TNode node) {
   return (node.getKind() == kind::NOT &&
           node[0].getKind() == kind::BITVECTOR_ULE);
 }
 
 template<> inline
-Node RewriteRule<NotUle>::apply(Node node) {
+Node RewriteRule<NotUle>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl;
   Node ult = node[0];
   Node a = ult[0];
@@ -663,7 +663,7 @@ Node RewriteRule<NotUle>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<MultOne>::applies(Node node) {
+bool RewriteRule<MultOne>::applies(TNode node) {
   unsigned size = utils::getSize(node); 
   return (node.getKind() == kind::BITVECTOR_MULT &&
           (node[0] == utils::mkConst(size, 1) ||
@@ -671,7 +671,7 @@ bool RewriteRule<MultOne>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<MultOne>::apply(Node node) {
+Node RewriteRule<MultOne>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<MultOne>(" << node << ")" << std::endl;
   unsigned size = utils::getSize(node); 
   if (node[0] == utils::mkConst(size, 1)) {
@@ -688,7 +688,7 @@ Node RewriteRule<MultOne>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<MultZero>::applies(Node node) {
+bool RewriteRule<MultZero>::applies(TNode node) {
   unsigned size = utils::getSize(node); 
   return (node.getKind() == kind::BITVECTOR_MULT &&
           (node[0] == utils::mkConst(size, 0) ||
@@ -696,7 +696,7 @@ bool RewriteRule<MultZero>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<MultZero>::apply(Node node) {
+Node RewriteRule<MultZero>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<MultZero>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 0); 
 }
@@ -708,7 +708,7 @@ Node RewriteRule<MultZero>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<MultPow2>::applies(Node node) {
+bool RewriteRule<MultPow2>::applies(TNode node) {
   if (node.getKind() != kind::BITVECTOR_MULT)
     return false;
 
@@ -721,7 +721,7 @@ bool RewriteRule<MultPow2>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<MultPow2>::apply(Node node) {
+Node RewriteRule<MultPow2>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl;
 
   std::vector<Node>  children;
@@ -750,7 +750,7 @@ Node RewriteRule<MultPow2>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<PlusZero>::applies(Node node) {
+bool RewriteRule<PlusZero>::applies(TNode node) {
   Node zero = utils::mkConst(utils::getSize(node), 0); 
   return (node.getKind() == kind::BITVECTOR_PLUS &&
           (node[0] == zero ||
@@ -758,7 +758,7 @@ bool RewriteRule<PlusZero>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<PlusZero>::apply(Node node) {
+Node RewriteRule<PlusZero>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<PlusZero>(" << node << ")" << std::endl;
   Node zero = utils::mkConst(utils::getSize(node), 0);
   if (node[0] == zero) {
@@ -775,13 +775,13 @@ Node RewriteRule<PlusZero>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<NegIdemp>::applies(Node node) {
+bool RewriteRule<NegIdemp>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_NEG &&
           node[0].getKind() == kind::BITVECTOR_NEG);
 }
 
 template<> inline
-Node RewriteRule<NegIdemp>::apply(Node node) {
+Node RewriteRule<NegIdemp>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node << ")" << std::endl;
   return node[0][0]; 
 }
@@ -793,13 +793,13 @@ Node RewriteRule<NegIdemp>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<UdivPow2>::applies(Node node) {
+bool RewriteRule<UdivPow2>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_UDIV &&
           utils::isPow2Const(node[1]));
 }
 
 template<> inline
-Node RewriteRule<UdivPow2>::apply(Node node) {
+Node RewriteRule<UdivPow2>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl;
   Node a = node[0];
   unsigned power = utils::isPow2Const(node[1]) -1;
@@ -817,13 +817,13 @@ Node RewriteRule<UdivPow2>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<UdivOne>::applies(Node node) {
+bool RewriteRule<UdivOne>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_UDIV &&
           node[1] == utils::mkConst(utils::getSize(node), 1));
 }
 
 template<> inline
-Node RewriteRule<UdivOne>::apply(Node node) {
+Node RewriteRule<UdivOne>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl;
   return node[0]; 
 }
@@ -835,13 +835,13 @@ Node RewriteRule<UdivOne>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<UdivSelf>::applies(Node node) {
+bool RewriteRule<UdivSelf>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_UDIV &&
           node[0] == node[1]);
 }
 
 template<> inline
-Node RewriteRule<UdivSelf>::apply(Node node) {
+Node RewriteRule<UdivSelf>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<UdivSelf>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 1); 
 }
@@ -853,13 +853,13 @@ Node RewriteRule<UdivSelf>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<UremPow2>::applies(Node node) {
+bool RewriteRule<UremPow2>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_UREM &&
           utils::isPow2Const(node[1]));
 }
 
 template<> inline
-Node RewriteRule<UremPow2>::apply(Node node) {
+Node RewriteRule<UremPow2>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned power = utils::isPow2Const(node[1]) - 1;
@@ -878,13 +878,13 @@ Node RewriteRule<UremPow2>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<UremOne>::applies(Node node) {
+bool RewriteRule<UremOne>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_UREM &&
           node[1] == utils::mkConst(utils::getSize(node), 1));
 }
 
 template<> inline
-Node RewriteRule<UremOne>::apply(Node node) {
+Node RewriteRule<UremOne>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<UremOne>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 0); 
 }
@@ -896,13 +896,13 @@ Node RewriteRule<UremOne>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<UremSelf>::applies(Node node) {
+bool RewriteRule<UremSelf>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_UREM &&
           node[0] == node[1]);
 }
 
 template<> inline
-Node RewriteRule<UremSelf>::apply(Node node) {
+Node RewriteRule<UremSelf>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<UremSelf>(" << node << ")" << std::endl;
   return utils::mkConst(utils::getSize(node), 0); 
 }
@@ -914,7 +914,7 @@ Node RewriteRule<UremSelf>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<ShiftZero>::applies(Node node) {
+bool RewriteRule<ShiftZero>::applies(TNode node) {
   return ((node.getKind() == kind::BITVECTOR_SHL ||
            node.getKind() == kind::BITVECTOR_LSHR ||
            node.getKind() == kind::BITVECTOR_ASHR) &&
@@ -922,7 +922,7 @@ bool RewriteRule<ShiftZero>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<ShiftZero>::apply(Node node) {
+Node RewriteRule<ShiftZero>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node << ")" << std::endl;
   return node[0]; 
 }
@@ -935,7 +935,7 @@ Node RewriteRule<ShiftZero>::apply(Node node) {
  */
 
 template<> inline
-bool RewriteRule<BBPlusNeg>::applies(Node node) {
+bool RewriteRule<BBPlusNeg>::applies(TNode node) {
   if (node.getKind() != kind::BITVECTOR_PLUS) {
     return false; 
   }
@@ -950,7 +950,7 @@ bool RewriteRule<BBPlusNeg>::applies(Node node) {
 }
 
 template<> inline
-Node RewriteRule<BBPlusNeg>::apply(Node node) {
+Node RewriteRule<BBPlusNeg>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node << ")" << std::endl;
 
   std::vector<Node> children;
@@ -976,7 +976,7 @@ Node RewriteRule<BBPlusNeg>::apply(Node node) {
 //  */
 
 // template<> inline
-// bool RewriteRule<BBFactorOut>::applies(Node node) {
+// bool RewriteRule<BBFactorOut>::applies(TNode node) {
 //   if (node.getKind() != kind::BITVECTOR_PLUS) {
 //     return false; 
 //   }
@@ -989,7 +989,7 @@ Node RewriteRule<BBPlusNeg>::apply(Node node) {
 // }
 
 // template<> inline
-// Node RewriteRule<BBFactorOut>::apply(Node node) {
+// Node RewriteRule<BBFactorOut>::apply(TNode node) {
 //   BVDebug("bv-rewrite") << "RewriteRule<BBFactorOut>(" << node << ")" << std::endl;
 //   std::hash_set<TNode, TNodeHashFunction> factors;
 
@@ -1020,12 +1020,12 @@ Node RewriteRule<BBPlusNeg>::apply(Node node) {
 //  */
 
 // template<> inline
-// bool RewriteRule<>::applies(Node node) {
+// bool RewriteRule<>::applies(TNode node) {
 //   return (node.getKind() == );
 // }
 
 // template<> inline
-// Node RewriteRule<>::apply(Node node) {
+// Node RewriteRule<>::apply(TNode 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 c2649e881..f6bbbd8d1 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -512,13 +512,25 @@ RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool preregister
 }
 
 RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) {
-  Node resultNode = LinearRewriteStrategy
-    < RewriteRule<FailEq>,
-      RewriteRule<SimplifyEq>,
-      RewriteRule<ReflexivityEq>
-      >::apply(node);
-  
-  return RewriteResponse(REWRITE_DONE, resultNode); 
+  if (preregister) {
+    Node resultNode = LinearRewriteStrategy
+      < RewriteRule<FailEq>,
+        RewriteRule<SimplifyEq>,
+        RewriteRule<ReflexivityEq>
+        >::apply(node);
+    return RewriteResponse(REWRITE_DONE, resultNode); 
+  }
+
+  else {
+    Node resultNode = LinearRewriteStrategy
+      < RewriteRule<FailEq>,
+        RewriteRule<SimplifyEq>,
+        RewriteRule<ReflexivityEq>
+        //        ,RewriteRule<BitwiseEq>,
+        //        RewriteRule<SolveEq>
+        >::apply(node);
+    return RewriteResponse(REWRITE_DONE, resultNode); 
+  }
 }
 
 
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 78835b75c..3736da639 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -168,7 +168,7 @@ inline Node mkBitOf(TNode node, unsigned index) {
 }
 
 
-inline Node mkConcat(Node node, unsigned repeat) {
+inline Node mkConcat(TNode node, unsigned repeat) {
   Assert (repeat); 
   if(repeat == 1) {
     return node; 
diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp
index 50881af82..7d2b6e333 100644
--- a/src/theory/ite_simplifier.cpp
+++ b/src/theory/ite_simplifier.cpp
@@ -144,19 +144,16 @@ Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVa
 
 Node ITESimplifier::getSimpVar(TypeNode t)
 {
-  if (t.isInteger()) {
-    if (d_simpVarInt.isNull()) {
-      d_simpVarInt = NodeManager::currentNM()->mkVar(t);
-    }
-    return d_simpVarInt;
+  std::hash_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
+  it = d_simpVars.find(t);
+  if (it != d_simpVars.end()) {
+    return (*it).second;
   }
-  if (t.isReal()) {
-    if (d_simpVarReal.isNull()) {
-      d_simpVarReal = NodeManager::currentNM()->mkVar(t);
-    }
-    return d_simpVarReal;
+  else {
+    Node var = NodeManager::currentNM()->mkVar(t);
+    d_simpVars[t] = var;
+    return var;
   }
-  return Node();
 }
 
 
diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h
index 8466c5444..50d37f502 100644
--- a/src/theory/ite_simplifier.h
+++ b/src/theory/ite_simplifier.h
@@ -64,8 +64,7 @@ class ITESimplifier {
 
   NodeMap d_simpConstCache;
   Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
-  Node d_simpVarInt;
-  Node d_simpVarReal;
+  std::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
   Node getSimpVar(TypeNode t);
   Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
 
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 4f9075f52..9e69738d3 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -49,7 +49,7 @@ struct RewriteStackElement {
   /**
    * Construct a fresh stack element.
    */
-  RewriteStackElement(Node node, TheoryId theoryId) :
+  RewriteStackElement(TNode node, TheoryId theoryId) :
     node(node),
     original(node),
     theoryId(theoryId),
@@ -58,7 +58,7 @@ struct RewriteStackElement {
   }
 };
 
-Node Rewriter::rewrite(Node node) {
+Node Rewriter::rewrite(TNode node) {
   return rewriteTo(theory::Theory::theoryOf(node), node);
 }
 
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index dacc4d212..e80606c95 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -96,7 +96,7 @@ public:
    * Rewrites the node using theoryOf() to determine which rewriter to
    * use on the node.
    */
-  static Node rewrite(Node node);
+  static Node rewrite(TNode node);
 
   /**
    * Rewrite an equality between two terms that are already in normal form, so
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d326d0bb7..f72275cb2 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -565,7 +565,7 @@ Node TheoryEngine::ppTheoryRewrite(TNode term)
   for (i = 0; i < nc; ++i) {
     newNode << ppTheoryRewrite(term[i]);
   }
-  Node newTerm = Rewriter::rewrite(newNode);
+  Node newTerm = Rewriter::rewrite(Node(newNode));
   Node newTerm2 = theoryOf(newTerm)->ppRewrite(newTerm);
   if (newTerm != newTerm2) {
     newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2));
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index bb6c93bd6..0b5d62d83 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -51,7 +51,7 @@ namespace CVC4 {
 struct NodeTheoryPair {
   Node node;
   theory::TheoryId theory;
-  NodeTheoryPair(Node node, theory::TheoryId theory)
+  NodeTheoryPair(TNode node, theory::TheoryId theory)
   : node(node), theory(theory) {}
   NodeTheoryPair()
   : theory(theory::THEORY_LAST) {}
-- 
2.30.2