works-ish

12 files changed, 587 insertions, 1166 deletions

diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index f6ccf16b8..eab6a16fd 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -71,63 +71,24 @@ Node RewriteRule<ConcatExtractMerge>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<ConcatConstantMerge>::applies(TNode node) {
-  return node.getKind() == kind::BITVECTOR_CONCAT;
+  return true;
 }
 
 template<> inline
 Node RewriteRule<ConcatConstantMerge>::apply(TNode node) {
-
-  Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl;
-
-  std::vector<Node> mergedConstants;
-  for (unsigned i = 0, end = node.getNumChildren(); i < end;) {
-    if (node[i].getKind() != kind::CONST_BITVECTOR) {
-      // If not a constant, just add it
-      mergedConstants.push_back(node[i]);
-      ++i;
-    } else {
-      // Find the longest sequence of constants
-      unsigned j = i + 1;
-      while (j < end) {
-        if (node[j].getKind() != kind::CONST_BITVECTOR) {
-          break;
-        } else {
-          ++ j;
-        }
-      }
-      // Append all the constants
-      BitVector current = node[i].getConst<BitVector>();
-      for (unsigned k = i + 1; k < j; ++ k) {
-        current = current.concat(node[k].getConst<BitVector>());
-      }
-      // Add the new merged constant
-      mergedConstants.push_back(utils::mkConst(current));
-      i = j;
-    }
-  }
-
-  Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl;
-
-  return utils::mkConcat(mergedConstants);
+  return rules::ConcatConstantMerge(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
 
 template<> inline
 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);
-  if (extractHigh != length - 1) return false;
-  unsigned extractLow  = utils::getExtractLow(node);
-  if (extractLow != 0) return false;
   return true;
 }
 
 template<> inline
 Node RewriteRule<ExtractWhole>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl;
-  return node[0];
+  return rules::ExtractWhole(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -187,23 +148,12 @@ Node RewriteRule<ExtractConcat>::apply(TNode node) {
 
 template<> inline
 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(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl;
-
-  // x[i:j][k:l] ~>  x[k+j:l+j]
-  Node child = node[0];
-  unsigned k = utils::getExtractHigh(node);
-  unsigned l = utils::getExtractLow(node);
-  unsigned j = utils::getExtractLow(child);
-
-  Node result = utils::mkExtract(child[0], k + j, l + j);
-  return result;
+  return rules::ExtractExtract(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index aa8c23ac1..8840e2443 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -39,23 +39,14 @@ namespace bv {
  */
 template<> inline
 bool RewriteRule<ExtractBitwise>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_EXTRACT &&
-          (node[0].getKind() == kind::BITVECTOR_AND ||
-           node[0].getKind() == kind::BITVECTOR_OR ||
-           node[0].getKind() == kind::BITVECTOR_XOR ));
+  return true;
 }
 
 template<> inline
 Node RewriteRule<ExtractBitwise>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<ExtractBitwise>(" << node << ")" << std::endl;
-  unsigned high = utils::getExtractHigh(node);
-  unsigned low = utils::getExtractLow(node);
-  std::vector<Node> children; 
-  for (unsigned i = 0; i < node[0].getNumChildren(); ++i) {
-    children.push_back(utils::mkExtract(node[0][i], high, low)); 
-  }
-  Kind kind = node[0].getKind(); 
-  return utils::mkSortedNode(kind, children);
+  Node n1 = rules::ExtractBitwiseAnd(node).d_node;
+  Node n2 = rules::ExtractBitwiseOr(n1).d_node;
+  return rules::ExtractBitwiseXor(n2).d_node;
 }
 
 /**
@@ -65,18 +56,13 @@ Node RewriteRule<ExtractBitwise>::apply(TNode node) {
  */
 template<> inline
 bool RewriteRule<ExtractNot>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_EXTRACT &&
-          node[0].getKind() == kind::BITVECTOR_NOT);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<ExtractNot>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<ExtractNot>(" << node << ")" << std::endl;
-  unsigned low = utils::getExtractLow(node);
-  unsigned high = utils::getExtractHigh(node);
-  Node a = utils::mkExtract(node[0][0], high, low);
-  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, a);
+  return rules::ExtractNot(node).d_node;
 }
 
 /** 
@@ -89,53 +75,13 @@ inline Node RewriteRule<ExtractNot>::apply(TNode node)
 
 template<> inline
 bool RewriteRule<ExtractSignExtend>::applies(TNode node) {
-  if (node.getKind() == kind::BITVECTOR_EXTRACT &&
-      node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND) {
-    return true; 
-  }
-  return false; 
+  return true;
 }
 
 template <>
 inline Node RewriteRule<ExtractSignExtend>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<ExtractSignExtend>(" << node << ")"
-                      << std::endl;
-  TNode extendee = node[0][0];
-  unsigned extendee_size = utils::getSize(extendee);
-
-  unsigned high = utils::getExtractHigh(node);
-  unsigned low = utils::getExtractLow(node);
-
-  Node resultNode;
-  // extract falls on extendee
-  if (high < extendee_size)
-  {
-    resultNode = utils::mkExtract(extendee, high, low);
-  }
-  else if (low < extendee_size && high >= extendee_size)
-  {
-    // if extract overlaps sign extend and extendee
-    Node low_extract = utils::mkExtract(extendee, extendee_size - 1, low);
-    unsigned new_amount = high - extendee_size + 1;
-    resultNode = utils::mkSignExtend(low_extract, new_amount);
-  }
-  else
-  {
-    // extract only over sign extend
-    Assert(low >= extendee_size);
-    unsigned top = utils::getSize(extendee) - 1;
-    Node most_significant_bit = utils::mkExtract(extendee, top, top);
-    std::vector<Node> bits;
-    for (unsigned i = 0; i < high - low + 1; ++i)
-    {
-      bits.push_back(most_significant_bit);
-    }
-    resultNode = utils::mkConcat(bits);
-  }
-  Debug("bv-rewrite") << "                           =>" << resultNode
-                      << std::endl;
-  return resultNode;
+  return rules::ExtractSignExtend(node).d_node;
 }
 
 /**
@@ -1027,201 +973,30 @@ Node RewriteRule<FlattenAssocCommutNoDuplicates>::apply(TNode node) {
   
 template<> inline
 bool RewriteRule<OrSimplify>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_OR);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<OrSimplify>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl;
-
-  NodeManager *nm = NodeManager::currentNM();
-  // this will remove duplicates
-  std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
-  unsigned size = utils::getSize(node);
-  BitVector constant(size, (unsigned)0);
-
-  for (unsigned i = 0; i < node.getNumChildren(); ++i)
-  {
-    TNode current = node[i];
-    // simplify constants
-    if (current.getKind() == kind::CONST_BITVECTOR)
-    {
-      BitVector bv = current.getConst<BitVector>();
-      constant = constant | bv;
-    }
-    else
-    {
-      if (current.getKind() == kind::BITVECTOR_NOT)
-      {
-        insert(subterms, current[0], true);
-      }
-      else
-      {
-        insert(subterms, current, false);
-      }
-    }
-  }
-
-  std::vector<Node> children;
-
-  if (constant == BitVector::mkOnes(size))
-  {
-    return utils::mkOnes(size); 
-  }
-
-  if (constant != BitVector(size, (unsigned)0))
-  {
-    children.push_back(utils::mkConst(constant));
-  }
-
-  std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it =
-      subterms.begin();
-
-  for (; it != subterms.end(); ++it)
-  {
-    if (it->second.pos > 0 && it->second.neg > 0)
-    {
-      // if we have a or ~a
-      return utils::mkOnes(size);
-    }
-    else
-    {
-      // idempotence
-      if (it->second.neg > 0)
-      {
-        // if it only occured negated
-        children.push_back(nm->mkNode(kind::BITVECTOR_NOT, it->first));
-      }
-      else
-      {
-        // if it only occured positive
-        children.push_back(it->first);
-      }
-    }
-  }
-
-  if (children.size() == 0)
-  {
-    return utils::mkZero(size);
-  }
-  return utils::mkSortedNode(kind::BITVECTOR_OR, children);
+  Node n1 = rules::OrSimplifyRmDups(node).d_node;
+  Node n2 = rules::OrSimplifySimpConsts(n1).d_node;
+  Node n3 = rules::OrSimplifyOnes(n2).d_node;
+  Node n4 = rules::OrSimplifyRmZeros(n3).d_node;
+  return rules::OrSimplifyCancel(n4).d_node;
 }
 
 template<> inline
 bool RewriteRule<XorSimplify>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_XOR);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<XorSimplify>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")"
-                      << std::endl;
-
-  NodeManager *nm = NodeManager::currentNM();
-  std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
-  unsigned size = utils::getSize(node);
-  BitVector constant;
-  bool const_set = false;
-
-  for (unsigned i = 0; i < node.getNumChildren(); ++i)
-  {
-    TNode current = node[i];
-    // simplify constants
-    if (current.getKind() == kind::CONST_BITVECTOR)
-    {
-      BitVector bv = current.getConst<BitVector>();
-      if (const_set)
-      {
-        constant = constant ^ bv;
-      }
-      else
-      {
-        const_set = true;
-        constant = bv;
-      }
-    }
-    else
-    {
-      // collect number of occurances of each term and its negation
-      if (current.getKind() == kind::BITVECTOR_NOT)
-      {
-        insert(subterms, current[0], true);
-      }
-      else
-      {
-        insert(subterms, current, false);
-      }
-    }
-  }
-
-  std::vector<Node> children;
-
-  std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it =
-      subterms.begin();
-  unsigned true_count = 0;
-  bool seen_false = false;
-  for (; it != subterms.end(); ++it)
-  {
-    unsigned pos = it->second.pos;  // number of positive occurances
-    unsigned neg = it->second.neg;  // number of negated occurances
-
-    // remove duplicates using the following rules
-    // a xor a ==> false
-    // false xor false ==> false
-    seen_false = seen_false ? seen_false : (pos > 1 || neg > 1);
-    // check what did not reduce
-    if (pos % 2 && neg % 2)
-    {
-      // we have a xor ~a ==> true
-      ++true_count;
-    }
-    else if (pos % 2)
-    {
-      // we had a positive occurence left
-      children.push_back(it->first);
-    }
-    else if (neg % 2)
-    {
-      // we had a negative occurence left
-      children.push_back(nm->mkNode(kind::BITVECTOR_NOT, it->first));
-    }
-    // otherwise both reduced to false
-  }
-
-  std::vector<BitVector> xorConst;
-  BitVector true_bv = BitVector::mkOnes(size);
-  BitVector false_bv(size, (unsigned)0);
-
-  if (true_count)
-  {
-    // true xor ... xor true ==> true (odd)
-    //                       ==> false (even)
-    xorConst.push_back(true_count % 2 ? true_bv : false_bv);
-  }
-  if (seen_false)
-  {
-    xorConst.push_back(false_bv);
-  }
-  if (const_set)
-  {
-    xorConst.push_back(constant);
-  }
-
-  if (xorConst.size() > 0)
-  {
-    BitVector result = xorConst[0];
-    for (unsigned i = 1; i < xorConst.size(); ++i)
-    {
-      result = result ^ xorConst[i];
-    }
-    children.push_back(utils::mkConst(result));
-  }
-
-  Assert(children.size());
-
-  return utils::mkSortedNode(kind::BITVECTOR_XOR, children);
+  Node n1 = rules::XorSimplifyRmDups(node).d_node;
+  Node n2 = rules::XorSimplifySimpConsts(n1).d_node;
+  return rules::XorSimplifyCancel(n2).d_node;
 }
 
 /** 
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 0412e7401..3af5c7ef0 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -164,51 +164,25 @@ inline Node RewriteRule<RepeatEliminate>::apply(TNode node)
 template <>
 inline bool RewriteRule<RotateLeftEliminate>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_ROTATE_LEFT);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<RotateLeftEliminate>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<RotateLeftEliminate>(" << node << ")" << std::endl;
-  TNode a = node[0];
-  unsigned amount =
-      node.getOperator().getConst<BitVectorRotateLeft>().d_rotateLeftAmount;
-  amount = amount % utils::getSize(a); 
-  if (amount == 0) {
-    return a; 
-  }
-
-  Node left   = utils::mkExtract(a, utils::getSize(a)-1 - amount, 0);
-  Node right  = utils::mkExtract(a, utils::getSize(a) -1, utils::getSize(a) - amount);
-  Node result = utils::mkConcat(left, right);
-
-  return result;
+  return rules::RotateLeftEliminate(node).d_node;
 }
 
 template <>
 inline bool RewriteRule<RotateRightEliminate>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_ROTATE_RIGHT);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<RotateRightEliminate>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<RotateRightEliminate>(" << node << ")" << std::endl;
-  TNode a = node[0];
-  unsigned amount =
-      node.getOperator().getConst<BitVectorRotateRight>().d_rotateRightAmount;
-  amount = amount % utils::getSize(a); 
-  if (amount == 0) {
-    return a; 
-  }
-  
-  Node left  = utils::mkExtract(a, amount - 1, 0);
-  Node right = utils::mkExtract(a, utils::getSize(a)-1, amount);
-  Node result = utils::mkConcat(left, right);
-
-  return result;
+  return rules::RotateRightEliminate(node).d_node;
 }
 
 template <>
@@ -248,278 +222,121 @@ inline Node RewriteRule<IntToBVEliminate>::apply(TNode node)
 template <>
 inline bool RewriteRule<NandEliminate>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_NAND &&
-          node.getNumChildren() == 2);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<NandEliminate>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<NandEliminate>(" << node << ")"
-                      << std::endl;
-  NodeManager *nm = NodeManager::currentNM();
-  TNode a = node[0];
-  TNode b = node[1];
-  Node andNode = nm->mkNode(kind::BITVECTOR_AND, a, b);
-  Node result = nm->mkNode(kind::BITVECTOR_NOT, andNode);
-  return result;
+  return rules::NandEliminate(node).d_node;
 }
 
 template <>
 inline bool RewriteRule<NorEliminate>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_NOR && node.getNumChildren() == 2);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<NorEliminate>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<NorEliminate>(" << node << ")"
-                      << std::endl;
-  NodeManager *nm = NodeManager::currentNM();
-  TNode a = node[0];
-  TNode b = node[1];
-  Node orNode = nm->mkNode(kind::BITVECTOR_OR, a, b);
-  Node result = nm->mkNode(kind::BITVECTOR_NOT, orNode);
-  return result;
+  return rules::NorEliminate(node).d_node;
 }
 
 template <>
 inline bool RewriteRule<XnorEliminate>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_XNOR &&
-          node.getNumChildren() == 2);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<XnorEliminate>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<XnorEliminate>(" << node << ")"
-                      << std::endl;
-  NodeManager *nm = NodeManager::currentNM();
-  TNode a = node[0];
-  TNode b = node[1];
-  Node xorNode = nm->mkNode(kind::BITVECTOR_XOR, a, b);
-  Node result = nm->mkNode(kind::BITVECTOR_NOT, xorNode);
-  return result;
+  return rules::XnorEliminate(node).d_node;
 }
 
 template <>
 inline bool RewriteRule<SdivEliminate>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_SDIV);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<SdivEliminate>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<SdivEliminate>(" << node << ")"
-                      << std::endl;
-
-  NodeManager *nm = NodeManager::currentNM();
-  TNode a = node[0];
-  TNode b = node[1];
-  unsigned size = utils::getSize(a);
-
-  Node one = utils::mkConst(1, 1);
-  Node a_lt_0 =
-      nm->mkNode(kind::EQUAL, utils::mkExtract(a, size - 1, size - 1), one);
-  Node b_lt_0 =
-      nm->mkNode(kind::EQUAL, utils::mkExtract(b, size - 1, size - 1), one);
-  Node abs_a =
-      nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a);
-  Node abs_b =
-      nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b);
-
-  Node a_udiv_b =
-      nm->mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UDIV_TOTAL
-                                                    : kind::BITVECTOR_UDIV,
-                 abs_a,
-                 abs_b);
-  Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b);
-
-  Node condition = nm->mkNode(kind::XOR, a_lt_0, b_lt_0);
-  Node result = nm->mkNode(kind::ITE, condition, neg_result, a_udiv_b);
-
-  return result;
+  return rules::SdivEliminate(node).d_node;
 }
 
 template <>
 inline bool RewriteRule<SremEliminate>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_SREM);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<SremEliminate>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<SremEliminate>(" << node << ")"
-                      << std::endl;
-  NodeManager *nm = NodeManager::currentNM();
-  TNode a = node[0];
-  TNode b = node[1];
-  unsigned size = utils::getSize(a);
-
-  Node one = utils::mkConst(1, 1);
-  Node a_lt_0 =
-      nm->mkNode(kind::EQUAL, utils::mkExtract(a, size - 1, size - 1), one);
-  Node b_lt_0 =
-      nm->mkNode(kind::EQUAL, utils::mkExtract(b, size - 1, size - 1), one);
-  Node abs_a =
-      nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a);
-  Node abs_b =
-      nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b);
-
-  Node a_urem_b =
-      nm->mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UREM_TOTAL
-                                                    : kind::BITVECTOR_UREM,
-                 abs_a,
-                 abs_b);
-  Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b);
-
-  Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b);
-
-  return result;
+  return rules::SremEliminate(node).d_node;
 }
 
 template <>
 inline bool RewriteRule<SmodEliminate>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_SMOD);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<SmodEliminate>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")"
-                      << std::endl;
-  NodeManager *nm = NodeManager::currentNM();
-  TNode s = node[0];
-  TNode t = node[1];
-  unsigned size = utils::getSize(s);
-
-  // (bvsmod s t) abbreviates
-  //     (let ((?msb_s ((_ extract |m-1| |m-1|) s))
-  //           (?msb_t ((_ extract |m-1| |m-1|) t)))
-  //       (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s)))
-  //             (abs_t (ite (= ?msb_t #b0) t (bvneg t))))
-  //         (let ((u (bvurem abs_s abs_t)))
-  //           (ite (= u (_ bv0 m))
-  //                u
-  //           (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
-  //                u
-  //           (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
-  //                (bvadd (bvneg u) t)
-  //           (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
-  //                (bvadd u t)
-  //                (bvneg u))))))))
-
-  Node msb_s = utils::mkExtract(s, size - 1, size - 1);
-  Node msb_t = utils::mkExtract(t, size - 1, size - 1);
-
-  Node bit1 = utils::mkConst(1, 1);
-  Node bit0 = utils::mkConst(1, 0);
-
-  Node abs_s =
-      msb_s.eqNode(bit0).iteNode(s, nm->mkNode(kind::BITVECTOR_NEG, s));
-  Node abs_t =
-      msb_t.eqNode(bit0).iteNode(t, nm->mkNode(kind::BITVECTOR_NEG, t));
-
-  Node u = nm->mkNode(kind::BITVECTOR_UREM, abs_s, abs_t);
-  Node neg_u = nm->mkNode(kind::BITVECTOR_NEG, u);
-
-  Node cond0 = u.eqNode(utils::mkConst(size, 0));
-  Node cond1 = msb_s.eqNode(bit0).andNode(msb_t.eqNode(bit0));
-  Node cond2 = msb_s.eqNode(bit1).andNode(msb_t.eqNode(bit0));
-  Node cond3 = msb_s.eqNode(bit0).andNode(msb_t.eqNode(bit1));
-
-  Node result = cond0.iteNode(
-      u,
-      cond1.iteNode(
-          u,
-          cond2.iteNode(
-              nm->mkNode(kind::BITVECTOR_PLUS, neg_u, t),
-              cond3.iteNode(nm->mkNode(kind::BITVECTOR_PLUS, u, t), neg_u))));
-
-  return result;
+  return rules::SmodEliminate(node).d_node;
 }
 
 template <>
 inline bool RewriteRule<ZeroExtendEliminate>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_ZERO_EXTEND); 
+  return true;
 }
 
 template <>
 inline Node RewriteRule<ZeroExtendEliminate>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<ZeroExtendEliminate>(" << node << ")" << std::endl;
-
-  TNode bv = node[0];
-  unsigned amount =
-      node.getOperator().getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
-  if (amount == 0) {
-    return node[0]; 
-  }
-  Node zero = utils::mkConst(amount, 0);
-  Node result = utils::mkConcat(zero, node[0]); 
-
-  return result;
+  return rules::ZeroExtendEliminate(node).d_node;
 }
 
 template <>
 inline bool RewriteRule<SignExtendEliminate>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND); 
+  return true;
 }
 
 template <>
 inline Node RewriteRule<SignExtendEliminate>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<SignExtendEliminate>(" << node << ")" << std::endl;
-
-  unsigned amount =
-      node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
-  if(amount == 0) {
-    return node[0]; 
-  }
-  unsigned size = utils::getSize(node[0]); 
-  Node sign_bit = utils::mkExtract(node[0], size-1, size-1); 
-  Node extension = utils::mkConcat(sign_bit, amount);
-
-  return utils::mkConcat(extension, node[0]);
+  return rules::SignExtendEliminate(node).d_node;
 }
 
 template <>
 inline bool RewriteRule<RedorEliminate>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_REDOR);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<RedorEliminate>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<RedorEliminate>(" << node << ")" << std::endl;
-  TNode a = node[0];
-  unsigned size = utils::getSize(node[0]); 
-  Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkConst( size, 0 ) );
-  return result.negate();
+  return rules::RedorEliminate(node).d_node;
 }
 
 template <>
 inline bool RewriteRule<RedandEliminate>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_REDAND);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<RedandEliminate>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<RedandEliminate>(" << node << ")" << std::endl;
-  TNode a = node[0];
-  unsigned size = utils::getSize(node[0]); 
-  Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkOnes( size ) );
-  return result;
+  return rules::RedandEliminate(node).d_node;
 }
 
 }
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index afaf92c7e..5837fb14d 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -39,15 +39,13 @@ namespace bv {
 template <>
 inline bool RewriteRule<BvIteConstCond>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_ITE && node[0].isConst());
+  return true;
 }
 
 template <>
 inline Node RewriteRule<BvIteConstCond>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<BvIteConstCond>(" << node << ")"
-                      << std::endl;
-  return utils::isZero(node[0]) ? node[2] : node[1];
+  return rules::BvIteConstCond(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -79,22 +77,13 @@ inline Node RewriteRule<BvIteEqualChildren>::apply(TNode node)
 template <>
 inline bool RewriteRule<BvIteConstChildren>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_ITE
-          && utils::getSize(node[1]) == 1
-          && node[1].isConst() && node[2].isConst());
+  return true;
 }
 
 template <>
 inline Node RewriteRule<BvIteConstChildren>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<BvIteConstChildren>(" << node << ")"
-                      << std::endl;
-  if (utils::isOne(node[1]) && utils::isZero(node[2]))
-  {
-    return node[0];
-  }
-  Assert(utils::isZero(node[1]) && utils::isOne(node[2]));
-  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, node[0]);
+  return rules::BvIteConstChildren(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -111,25 +100,14 @@ inline Node RewriteRule<BvIteConstChildren>::apply(TNode node)
 template <>
 inline bool RewriteRule<BvIteEqualCond>::applies(TNode node)
 {
-  return (
-      node.getKind() == kind::BITVECTOR_ITE
-      && ((node[1].getKind() == kind::BITVECTOR_ITE && node[0] == node[1][0])
-          || (node[2].getKind() == kind::BITVECTOR_ITE
-              && node[0] == node[2][0])));
+  return true;
 }
 
 template <>
 inline Node RewriteRule<BvIteEqualCond>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<BvIteEqualCond>(" << node << ")"
-                      << std::endl;
-  Node t0 = node[1].getKind() == kind::BITVECTOR_ITE && node[0] == node[1][0]
-                ? node[1][1]
-                : node[1];
-  Node e1 = node[2].getKind() == kind::BITVECTOR_ITE && node[0] == node[2][0]
-                ? node[2][2]
-                : node[2];
-  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ITE, node[0], t0, e1);
+  Node n1 = rules::BvIteEqualCondThen(node).d_node;
+  return rules::BvIteEqualCondElse(n1).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -143,22 +121,13 @@ inline Node RewriteRule<BvIteEqualCond>::apply(TNode node)
 template <>
 inline bool RewriteRule<BvIteMergeThenIf>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_ITE
-          && node[1].getKind() == kind::BITVECTOR_ITE
-          && node[1][1] == node[2]);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<BvIteMergeThenIf>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<BvIteMergeThenIf>(" << node << ")"
-                      << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
-  Assert(node[1].getKind() == kind::BITVECTOR_ITE);
-  Node cond = nm->mkNode(kind::BITVECTOR_AND,
-                         node[0],
-                         nm->mkNode(kind::BITVECTOR_NOT, node[1][0]));
-  return nm->mkNode(kind::BITVECTOR_ITE, cond, node[1][2], node[2]);
+  return rules::BvIteMergeThenIf(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -172,20 +141,13 @@ inline Node RewriteRule<BvIteMergeThenIf>::apply(TNode node)
 template <>
 inline bool RewriteRule<BvIteMergeElseIf>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_ITE
-          && node[1].getKind() == kind::BITVECTOR_ITE
-          && node[1][2] == node[2]);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<BvIteMergeElseIf>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<BvIteMergeElseIf>(" << node << ")"
-                      << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
-  Assert(node[1].getKind() == kind::BITVECTOR_ITE);
-  Node cond = nm->mkNode(kind::BITVECTOR_AND, node[0], node[1][0]);
-  return nm->mkNode(kind::BITVECTOR_ITE, cond, node[1][1], node[2]);
+  return rules::BvIteMergeElseIf(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -199,22 +161,13 @@ inline Node RewriteRule<BvIteMergeElseIf>::apply(TNode node)
 template <>
 inline bool RewriteRule<BvIteMergeThenElse>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_ITE
-          && node[2].getKind() == kind::BITVECTOR_ITE
-          && node[1] == node[2][1]);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<BvIteMergeThenElse>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<BvIteMergeThenElse>(" << node << ")"
-                      << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
-  Assert(node[2].getKind() == kind::BITVECTOR_ITE);
-  Node cond = nm->mkNode(kind::BITVECTOR_AND,
-                         nm->mkNode(kind::BITVECTOR_NOT, node[0]),
-                         nm->mkNode(kind::BITVECTOR_NOT, node[2][0]));
-  return nm->mkNode(kind::BITVECTOR_ITE, cond, node[2][2], node[1]);
+  return rules::BvIteMergeThenElse(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -228,22 +181,13 @@ inline Node RewriteRule<BvIteMergeThenElse>::apply(TNode node)
 template <>
 inline bool RewriteRule<BvIteMergeElseElse>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_ITE
-          && node[2].getKind() == kind::BITVECTOR_ITE
-          && node[1] == node[2][2]);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<BvIteMergeElseElse>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<BvIteMergeElseElse>(" << node << ")"
-                      << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
-  Assert(node[2].getKind() == kind::BITVECTOR_ITE);
-  Node cond = nm->mkNode(kind::BITVECTOR_AND,
-                         nm->mkNode(kind::BITVECTOR_NOT, node[0]),
-                         node[2][0]);
-  return nm->mkNode(kind::BITVECTOR_ITE, cond, node[2][1], node[1]);
+  return rules::BvIteMergeElseElse(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -256,23 +200,13 @@ inline Node RewriteRule<BvIteMergeElseElse>::apply(TNode node)
 template <>
 inline bool RewriteRule<BvComp>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_COMP
-          && utils::getSize(node[0]) == 1
-          && (node[0].isConst() || node[1].isConst()));
+  return true;
 }
 
 template <>
 inline Node RewriteRule<BvComp>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<BvComp>(" << node << ")" << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
-  if (node[0].isConst())
-  {
-    return utils::isZero(node[0]) ? nm->mkNode(kind::BITVECTOR_NOT, node[1])
-                                  : Node(node[1]);
-  }
-  return utils::isZero(node[1]) ? nm->mkNode(kind::BITVECTOR_NOT, node[0])
-                                : Node(node[0]);
+  return rules::BvComp(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -427,6 +361,8 @@ Node RewriteRule<AndOne>::apply(TNode node) {
 template <>
 inline bool RewriteRule<AndOrXorConcatPullUp>::applies(TNode node)
 {
+  return true;
+  /*
   if (node.getKind() != kind::BITVECTOR_AND
       && node.getKind() != kind::BITVECTOR_OR
       && node.getKind() != kind::BITVECTOR_XOR)
@@ -453,11 +389,16 @@ inline bool RewriteRule<AndOrXorConcatPullUp>::applies(TNode node)
   }
   if (n.isNull()) return false;
   return utils::isZero(n) || utils::isOne(n) || utils::isOnes(n);
+  */
 }
 
 template <>
 inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node)
 {
+  Node n1 = rules::AndPullUp(node).d_node;
+  Node n2 = rules::OrPullUp(n1).d_node;
+  return rules::XorPullUp(n2).d_node;
+  /*
   Debug("bv-rewrite") << "RewriteRule<AndOrXorConcatPullUp>(" << node << ")"
                       << std::endl;
   uint32_t m, my, mz;
@@ -535,6 +476,7 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node)
   }
 
   return res;
+  */
 }
 
 /* -------------------------------------------------------------------------- */
@@ -628,46 +570,13 @@ Node RewriteRule<XorDuplicate>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<XorOne>::applies(TNode node) {
-  if (node.getKind() != kind::BITVECTOR_XOR) {
-    return false; 
-  }
-  Node ones = utils::mkOnes(utils::getSize(node));
-  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-    if (node[i] == ones) {
-      return true; 
-    }
-  }
-  return false; 
+  return true;
 }
 
 template <>
 inline Node RewriteRule<XorOne>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl;
-  NodeManager *nm = NodeManager::currentNM();
-  Node ones = utils::mkOnes(utils::getSize(node));
-  std::vector<Node> children;
-  bool found_ones = false;
-  // XorSimplify should have been called before
-  for (unsigned i = 0; i < node.getNumChildren(); ++i)
-  {
-    if (node[i] == ones)
-    {
-      // make sure only ones occurs only once
-      found_ones = !found_ones;
-    }
-    else
-    {
-      children.push_back(node[i]);
-    }
-  }
-
-  Node result = utils::mkNaryNode(kind::BITVECTOR_XOR, children);
-  if (found_ones)
-  {
-    result = nm->mkNode(kind::BITVECTOR_NOT, result);
-  }
-  return result;
+  return rules::XorZero(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -790,14 +699,12 @@ inline Node RewriteRule<NotXor>::apply(TNode node)
 
 template<> inline
 bool RewriteRule<NotIdemp>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_NOT &&
-          node[0].getKind() == kind::BITVECTOR_NOT); 
+  return true;
 }
 
 template<> inline
 Node RewriteRule<NotIdemp>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<NotIdemp>(" << node << ")" << std::endl;
-  return node[0][0];
+  return rules::NotIdemp(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -810,15 +717,13 @@ Node RewriteRule<NotIdemp>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<LtSelf>::applies(TNode node) {
-  return ((node.getKind() == kind::BITVECTOR_ULT ||
-           node.getKind() == kind::BITVECTOR_SLT) &&
-          node[0] == node[1]);
+  return true;
 }
 
 template<> inline
 Node RewriteRule<LtSelf>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<LtSelf>(" << node << ")" << std::endl;
-  return utils::mkFalse(); 
+  Node n1 = rules::LtSelfUlt(node).d_node;
+  return rules::LtSelfSlt(n1).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -831,15 +736,13 @@ Node RewriteRule<LtSelf>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<LteSelf>::applies(TNode node) {
-  return ((node.getKind() == kind::BITVECTOR_ULE ||
-           node.getKind() == kind::BITVECTOR_SLE) &&
-          node[0] == node[1]);
+  return true;
 }
 
 template<> inline
 Node RewriteRule<LteSelf>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<LteSelf>(" << node << ")" << std::endl;
-  return utils::mkTrue(); 
+  Node n1 = rules::LteSelfUle(node).d_node;
+  return rules::LteSelfSle(n1).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -853,16 +756,13 @@ Node RewriteRule<LteSelf>::apply(TNode node) {
 template <>
 inline bool RewriteRule<ZeroUlt>::applies(TNode node)
 {
-  return (node.getKind() == kind::BITVECTOR_ULT
-          && node[0] == utils::mkZero(utils::getSize(node[0])));
+  return true;
 }
 
 template <>
 inline Node RewriteRule<ZeroUlt>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<ZeroUlt>(" << node << ")" << std::endl;
-  NodeManager *nm = NodeManager::currentNM();
-  return nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, node[0], node[1]));
+  return rules::ZeroUlt(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -875,14 +775,12 @@ inline Node RewriteRule<ZeroUlt>::apply(TNode node)
 
 template<> inline
 bool RewriteRule<UltZero>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_ULT &&
-          node[1] == utils::mkZero(utils::getSize(node[0])));
+  return true;
 }
 
 template<> inline
 Node RewriteRule<UltZero>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
-  return utils::mkFalse(); 
+  return rules::UltZero(node).d_node;
 }
 
 
@@ -893,16 +791,13 @@ Node RewriteRule<UltZero>::apply(TNode node) {
  */
 template<> inline
 bool RewriteRule<UltOne>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_ULT &&
-          node[1] == utils::mkOne(utils::getSize(node[0])));
+  return true;
 }
 
 template <>
 inline Node RewriteRule<UltOne>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<UltOne>(" << node << ")" << std::endl;
-  return NodeManager::currentNM()->mkNode(
-      kind::EQUAL, node[0], utils::mkZero(utils::getSize(node[0])));
+  return rules::UltOne(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -912,18 +807,13 @@ inline Node RewriteRule<UltOne>::apply(TNode node)
  */
 template<> inline
 bool RewriteRule<SltZero>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_SLT &&
-          node[1] == utils::mkZero(utils::getSize(node[0])));
+  return true;
 }
 
 template <>
 inline Node RewriteRule<SltZero>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
-  unsigned size = utils::getSize(node[0]);
-  Node most_significant_bit = utils::mkExtract(node[0], size - 1, size - 1);
-  return NodeManager::currentNM()->mkNode(
-      kind::EQUAL, most_significant_bit, utils::mkOne(1));
+  return rules::SltZero(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -936,14 +826,12 @@ inline Node RewriteRule<SltZero>::apply(TNode node)
 
 template<> inline
 bool RewriteRule<UltSelf>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_ULT &&
-          node[1] == node[0]); 
+  return true;
 }
 
 template<> inline
 Node RewriteRule<UltSelf>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<UltSelf>(" << node << ")" << std::endl;
-  return utils::mkFalse(); 
+  return rules::UltSelf(node).d_node;
 }
 
 
@@ -957,15 +845,13 @@ Node RewriteRule<UltSelf>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<UleZero>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_ULE &&
-          node[1] == utils::mkZero(utils::getSize(node[0])));
+  return true;
 }
 
 template <>
 inline Node RewriteRule<UleZero>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl;
-  return NodeManager::currentNM()->mkNode(kind::EQUAL, node[0], node[1]);
+  return rules::UleZero(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -978,14 +864,12 @@ inline Node RewriteRule<UleZero>::apply(TNode node)
 
 template<> inline
 bool RewriteRule<UleSelf>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_ULE &&
-          node[1] == node[0]); 
+  return true;
 }
 
 template<> inline
 Node RewriteRule<UleSelf>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<UleSelf>(" << node << ")" << std::endl;
-  return utils::mkTrue(); 
+  return rules::UleSelf(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -998,14 +882,12 @@ Node RewriteRule<UleSelf>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<ZeroUle>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_ULE &&
-          node[0] == utils::mkZero(utils::getSize(node[0])));
+  return true;
 }
 
 template<> inline
 Node RewriteRule<ZeroUle>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node << ")" << std::endl;
-  return utils::mkTrue(); 
+  return rules::ZeroUle(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1018,18 +900,12 @@ Node RewriteRule<ZeroUle>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<UleMax>::applies(TNode node) {
-  if (node.getKind()!= kind::BITVECTOR_ULE) {
-    return false; 
-  }
-  uint32_t size = utils::getSize(node[0]); 
-  return (node.getKind() == kind::BITVECTOR_ULE
-          && node[1] == utils::mkOnes(size));
+  return true;
 }
 
 template<> inline
 Node RewriteRule<UleMax>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<UleMax>(" << node << ")" << std::endl;
-  return utils::mkTrue(); 
+  return rules::UleMax(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1042,18 +918,13 @@ Node RewriteRule<UleMax>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<NotUlt>::applies(TNode node) {
-  return (node.getKind() == kind::NOT &&
-          node[0].getKind() == kind::BITVECTOR_ULT);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<NotUlt>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl;
-  Node ult = node[0];
-  Node a = ult[0];
-  Node b = ult[1];
-  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULE, b, a);
+  return rules::NotUlt(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1066,18 +937,13 @@ inline Node RewriteRule<NotUlt>::apply(TNode node)
 
 template<> inline
 bool RewriteRule<NotUle>::applies(TNode node) {
-  return (node.getKind() == kind::NOT &&
-          node[0].getKind() == kind::BITVECTOR_ULE);
+  return true;
 }
 
 template <>
 inline Node RewriteRule<NotUle>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl;
-  Node ult = node[0];
-  Node a = ult[0];
-  Node b = ult[1];
-  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, b, a);
+  return rules::NotUle(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1091,70 +957,14 @@ inline Node RewriteRule<NotUle>::apply(TNode node)
 template <>
 inline bool RewriteRule<MultPow2>::applies(TNode node)
 {
-  if (node.getKind() != kind::BITVECTOR_MULT)
-    return false;
-
-  for (const Node& cn : node)
-  {
-    bool cIsNeg = false;
-    if (utils::isPow2Const(cn, cIsNeg))
-    {
-      return true; 
-    }
-  }
-  return false; 
+  return true;
 }
 
 template <>
 inline Node RewriteRule<MultPow2>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl;
-  NodeManager *nm = NodeManager::currentNM();
-  unsigned size = utils::getSize(node);
-  std::vector<Node>  children;
-  unsigned exponent = 0;
-  bool isNeg = false;
-  for (const Node& cn : node)
-  {
-    bool cIsNeg = false;
-    unsigned exp = utils::isPow2Const(cn, cIsNeg);
-    if (exp) {
-      exponent += exp - 1;
-      if (cIsNeg)
-      {
-        isNeg = !isNeg;
-      }
-    }
-    else {
-      children.push_back(cn);
-    }
-  }
-  if (exponent >= size)
-  {
-    return utils::mkZero(size);
-  }
-
-  Node a;
-  if (children.empty())
-  {
-    a = utils::mkOne(size);
-  }
-  else
-  {
-    a = utils::mkNaryNode(kind::BITVECTOR_MULT, children);
-  }
-
-  if (isNeg && size > 1)
-  {
-    a = nm->mkNode(kind::BITVECTOR_NEG, a);
-  }
-  if (exponent == 0)
-  {
-    return a;
-  }
-  Node extract = utils::mkExtract(a, size - exponent - 1, 0);
-  Node zeros = utils::mkConst(exponent, 0);
-  return utils::mkConcat(extract, zeros); 
+  Node n1 = rules::MultPowX(node).d_node;
+  return rules::MultPowXNeg(n1).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1171,6 +981,7 @@ inline Node RewriteRule<MultPow2>::apply(TNode node)
 
 template<> inline
 bool RewriteRule<ExtractMultLeadingBit>::applies(TNode node) {
+  return true; /*
   if (node.getKind() != kind::BITVECTOR_EXTRACT)
     return false;
   unsigned low = utils::getExtractLow(node);
@@ -1203,10 +1014,13 @@ bool RewriteRule<ExtractMultLeadingBit>::applies(TNode node) {
     return false; 
 
   return true; 
+  */
 }
 
 template<> inline
 Node RewriteRule<ExtractMultLeadingBit>::apply(TNode node) {
+  return rules::ExtractMultLeadingBit(node).d_node;
+  /*
   Debug("bv-rewrite") << "RewriteRule<MultLeadingBit>(" << node << ")" << std::endl;
 
   unsigned bitwidth = utils::getSize(node); 
@@ -1234,6 +1048,7 @@ Node RewriteRule<ExtractMultLeadingBit>::apply(TNode node) {
   Node result = utils::mkConst(bitwidth, 0u); 
   //  std::cout << "MultLeadingBit " << node <<" => " << result <<"\n";
   return result;
+  */
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1246,14 +1061,12 @@ Node RewriteRule<ExtractMultLeadingBit>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<NegIdemp>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_NEG &&
-          node[0].getKind() == kind::BITVECTOR_NEG);
+  return true;
 }
 
 template<> inline
 Node RewriteRule<NegIdemp>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node << ")" << std::endl;
-  return node[0][0]; 
+  return rules::NegIdemp(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1267,6 +1080,8 @@ Node RewriteRule<NegIdemp>::apply(TNode node) {
 template <>
 inline bool RewriteRule<UdivPow2>::applies(TNode node)
 {
+  return true;
+  /*
   bool isNeg = false;
   if (node.getKind() == kind::BITVECTOR_UDIV_TOTAL
       && utils::isPow2Const(node[1], isNeg))
@@ -1274,11 +1089,15 @@ inline bool RewriteRule<UdivPow2>::applies(TNode node)
     return !isNeg;
   }
   return false;
+  */
 }
 
 template <>
 inline Node RewriteRule<UdivPow2>::apply(TNode node)
 {
+  Node n1 = rules::UdivPowX(node).d_node;
+  return rules::UdivPowXNeg(n1).d_node;
+  /*
   Debug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl;
   NodeManager *nm = NodeManager::currentNM();
   unsigned size = utils::getSize(node);
@@ -1302,6 +1121,7 @@ inline Node RewriteRule<UdivPow2>::apply(TNode node)
     ret = nm->mkNode(kind::BITVECTOR_NEG, ret);
   }
   return ret;
+  */
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1314,14 +1134,12 @@ inline Node RewriteRule<UdivPow2>::apply(TNode node)
 
 template <>
 inline bool RewriteRule<UdivZero>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
-          node[1] == utils::mkConst(utils::getSize(node), 0));
+  return true;
 }
 
 template <>
 inline Node RewriteRule<UdivZero>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<UdivZero>(" << node << ")" << std::endl;
-  return utils::mkOnes(utils::getSize(node));
+  return rules::UdivZero(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1334,14 +1152,12 @@ inline Node RewriteRule<UdivZero>::apply(TNode node) {
 
 template <>
 inline bool RewriteRule<UdivOne>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
-          node[1] == utils::mkConst(utils::getSize(node), 1));
+  return true;
 }
 
 template <>
 inline Node RewriteRule<UdivOne>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl;
-  return node[0];
+  return rules::UdivOne(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1355,35 +1171,13 @@ inline Node RewriteRule<UdivOne>::apply(TNode node) {
 template <>
 inline bool RewriteRule<UremPow2>::applies(TNode node)
 {
-  bool isNeg;
-  if (node.getKind() == kind::BITVECTOR_UREM_TOTAL
-      && utils::isPow2Const(node[1], isNeg))
-  {
-    return !isNeg;
-  }
-  return false;
+  return true;
 }
 
 template <>
 inline Node RewriteRule<UremPow2>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
-  TNode a = node[0];
-  bool isNeg = false;
-  unsigned power = utils::isPow2Const(node[1], isNeg) - 1;
-  Node ret;
-  if (power == 0)
-  {
-    ret = utils::mkZero(utils::getSize(node));
-  }
-  else
-  {
-    Node extract = utils::mkExtract(a, power - 1, 0);
-    Node zeros = utils::mkZero(utils::getSize(node) - power);
-    ret = NodeManager::currentNM()->mkNode(
-        kind::BITVECTOR_CONCAT, zeros, extract);
-  }
-  return ret;
+  return rules::UremPowX(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1396,14 +1190,12 @@ inline Node RewriteRule<UremPow2>::apply(TNode node)
 
 template<> inline
 bool RewriteRule<UremOne>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_UREM_TOTAL &&
-          node[1] == utils::mkConst(utils::getSize(node), 1));
+  return true;
 }
 
 template<> inline
 Node RewriteRule<UremOne>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<UremOne>(" << node << ")" << std::endl;
-  return utils::mkConst(utils::getSize(node), 0); 
+  return rules::UremOne(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1416,14 +1208,12 @@ Node RewriteRule<UremOne>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<UremSelf>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_UREM_TOTAL &&
-          node[0] == node[1]);
+  return true;
 }
 
 template<> inline
 Node RewriteRule<UremSelf>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<UremSelf>(" << node << ")" << std::endl;
-  return utils::mkConst(utils::getSize(node), 0); 
+  return rules::UremSelf(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1444,8 +1234,9 @@ bool RewriteRule<ShiftZero>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<ShiftZero>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node << ")" << std::endl;
-  return node[0]; 
+  Node n1 = rules::ShiftZeroShl(node).d_node;
+  Node n2 = rules::ShiftZeroLshr(n1).d_node;
+  return rules::ShiftZeroAshr(n2).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1501,44 +1292,13 @@ inline Node RewriteRule<BBPlusNeg>::apply(TNode node)
 
 template<> inline
 bool RewriteRule<MergeSignExtend>::applies(TNode node) {
-  if (node.getKind() != kind::BITVECTOR_SIGN_EXTEND ||
-      (node[0].getKind() != kind::BITVECTOR_SIGN_EXTEND &&
-       node[0].getKind() != kind::BITVECTOR_ZERO_EXTEND))
-    return false;
   return true;
 }
 
 template<> inline
 Node RewriteRule<MergeSignExtend>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<MergeSignExtend>(" << node << ")" << std::endl;
-  unsigned amount1 =
-      node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
-
-  NodeManager* nm = NodeManager::currentNM();
-  if (node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND) {
-    unsigned amount2 = node[0]
-                           .getOperator()
-                           .getConst<BitVectorZeroExtend>()
-                           .d_zeroExtendAmount;
-    if (amount2 == 0)
-    {
-      NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND);
-      Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount1));
-      nb << op << node[0][0];
-      Node res = nb;
-      return res;
-    }
-    NodeBuilder<> nb(kind::BITVECTOR_ZERO_EXTEND);
-    Node op = nm->mkConst<BitVectorZeroExtend>(
-        BitVectorZeroExtend(amount1 + amount2));
-    nb << op << node[0][0];
-    Node res = nb;
-    return res;
-  }
-  Assert(node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND);
-  unsigned amount2 =
-      node[0].getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
-  return utils::mkSignExtend(node[0][0], amount1 + amount2);
+  Node n1 = rules::MergeSignExtendSign(node).d_node;
+  return rules::MergeSignExtendZero(n1).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1553,33 +1313,12 @@ Node RewriteRule<MergeSignExtend>::apply(TNode node) {
  */
 template <>
 inline bool RewriteRule<ZeroExtendEqConst>::applies(TNode node) {
-  return node.getKind() == kind::EQUAL &&
-         ((node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND &&
-           node[1].isConst()) ||
-          (node[1].getKind() == kind::BITVECTOR_ZERO_EXTEND &&
-           node[0].isConst()));
+  return true;
 }
 
 template <>
 inline Node RewriteRule<ZeroExtendEqConst>::apply(TNode node) {
-  TNode t, c;
-  if (node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND) {
-    t = node[0][0];
-    c = node[1];
-  } else {
-    t = node[1][0];
-    c = node[0];
-  }
-  BitVector c_hi =
-      c.getConst<BitVector>().extract(utils::getSize(c) - 1, utils::getSize(t));
-  BitVector c_lo = c.getConst<BitVector>().extract(utils::getSize(t) - 1, 0);
-  BitVector zero = BitVector(c_hi.getSize(), Integer(0));
-
-  if (c_hi == zero) {
-    return NodeManager::currentNM()->mkNode(kind::EQUAL, t,
-                                            utils::mkConst(c_lo));
-  }
-  return utils::mkFalse();
+  return rules::ZeroExtendEqConst(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1595,15 +1334,20 @@ inline Node RewriteRule<ZeroExtendEqConst>::apply(TNode node) {
  */
 template <>
 inline bool RewriteRule<SignExtendEqConst>::applies(TNode node) {
+  return true;
+  /*
   return node.getKind() == kind::EQUAL &&
          ((node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND &&
            node[1].isConst()) ||
           (node[1].getKind() == kind::BITVECTOR_SIGN_EXTEND &&
            node[0].isConst()));
+           */
 }
 
 template <>
 inline Node RewriteRule<SignExtendEqConst>::apply(TNode node) {
+  return rules::SignExtendEqConst(node).d_node;
+  /*
   TNode t, c;
   if (node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND) {
     t = node[0][0];
@@ -1623,6 +1367,7 @@ inline Node RewriteRule<SignExtendEqConst>::apply(TNode node) {
                                             utils::mkConst(c_lo));
   }
   return utils::mkFalse();
+  */
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1640,6 +1385,8 @@ inline Node RewriteRule<SignExtendEqConst>::apply(TNode node) {
  */
 template <>
 inline bool RewriteRule<ZeroExtendUltConst>::applies(TNode node) {
+  return true;
+  /*
   if (node.getKind() == kind::BITVECTOR_ULT &&
       ((node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND &&
         node[1].isConst()) ||
@@ -1668,10 +1415,14 @@ inline bool RewriteRule<ZeroExtendUltConst>::applies(TNode node) {
     return c_hi == zero;
   }
   return false;
+  */
 }
 
 template <>
 inline Node RewriteRule<ZeroExtendUltConst>::apply(TNode node) {
+  Node n1 = rules::ZeroExtendUltConstLhs(node).d_node;
+  return rules::ZeroExtendUltConstRhs(n1).d_node;
+  /*
   TNode t, c;
   bool is_lhs = node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND;
   if (is_lhs) {
@@ -1688,6 +1439,7 @@ inline Node RewriteRule<ZeroExtendUltConst>::apply(TNode node) {
     return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, t, c_lo);
   }
   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, c_lo, t);
+  */
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1711,6 +1463,8 @@ inline Node RewriteRule<ZeroExtendUltConst>::apply(TNode node) {
 template <>
 inline bool RewriteRule<SignExtendUltConst>::applies(TNode node)
 {
+  return true;
+  /*
   if (node.getKind() == kind::BITVECTOR_ULT
       && ((node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND
            && node[1].isConst())
@@ -1746,11 +1500,15 @@ inline bool RewriteRule<SignExtendUltConst>::applies(TNode node)
                    || (~bv_upper_bits <= bv_c && bv_c <= ~bv_msb_x)));
   }
   return false;
+  */
 }
 
 template <>
 inline Node RewriteRule<SignExtendUltConst>::apply(TNode node)
 {
+  Node n1 = rules::SignExtendUltConstLhs(node).d_node;
+  return rules::SignExtendUltConstRhs(n1).d_node;
+  /*
   TNode x, c;
   bool is_lhs = node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND;
   if (is_lhs)
@@ -1797,6 +1555,7 @@ inline Node RewriteRule<SignExtendUltConst>::apply(TNode node)
   // c[n-1:0] < x
   Assert(bv_c < bv_msb_x || bv_c >= ~bv_msb_x);
   return nm->mkNode(kind::BITVECTOR_ULT, c_lo, x);
+  */
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1856,40 +1615,13 @@ inline Node RewriteRule<MultSlice>::apply(TNode node)
  */
 template<> inline
 bool RewriteRule<UltPlusOne>::applies(TNode node) {
-  if (node.getKind() != kind::BITVECTOR_ULT) return false;
-  TNode x = node[0];
-  TNode y1 = node[1];
-  if (y1.getKind() != kind::BITVECTOR_PLUS) return false;
-  if (y1[0].getKind() != kind::CONST_BITVECTOR &&
-      y1[1].getKind() != kind::CONST_BITVECTOR)
-    return false;
-  
-  if (y1[0].getKind() == kind::CONST_BITVECTOR &&
-      y1[1].getKind() == kind::CONST_BITVECTOR)
-    return false;
-  
-  if (y1.getNumChildren() != 2)
-    return false; 
-
-  TNode one = y1[0].getKind() == kind::CONST_BITVECTOR ? y1[0] : y1[1];
-  if (one != utils::mkConst(utils::getSize(one), 1)) return false;
   return true; 
 }
 
 template <>
 inline Node RewriteRule<UltPlusOne>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<UltPlusOne>(" << node << ")" << std::endl;
-  NodeManager *nm = NodeManager::currentNM();
-  TNode x = node[0];
-  TNode y1 = node[1];
-  TNode y = y1[0].getKind() != kind::CONST_BITVECTOR ? y1[0] : y1[1];
-  unsigned size = utils::getSize(x);
-  Node not_y_eq_1 =
-      nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, y, utils::mkOnes(size)));
-  Node not_y_lt_x =
-      nm->mkNode(kind::NOT, nm->mkNode(kind::BITVECTOR_ULT, y, x));
-  return nm->mkNode(kind::AND, not_y_eq_1, not_y_lt_x);
+  return rules::UltPlusOne(node).d_node;
 }
 
 /* -------------------------------------------------------------------------- */
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index ceff24f25..ddb969716 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -217,17 +217,23 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool prerewrite) {
 
   if (RewriteRule<ExtractConcat>::applies(node)) {
     resultNode = RewriteRule<ExtractConcat>::run<false>(node);
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    if (resultNode != node) {
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
   }
 
   if (RewriteRule<ExtractSignExtend>::applies(node)) {
     resultNode = RewriteRule<ExtractSignExtend>::run<false>(node);
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    if (resultNode != node) {
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
   }
 
   if (RewriteRule<ExtractNot>::applies(node)) {
     resultNode = RewriteRule<ExtractNot>::run<false>(node);
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    if (resultNode != node) {
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
   }
 
   if (options::bvExtractArithRewrite()) {
@@ -263,7 +269,7 @@ RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool prerewrite)
       RewriteRule<ConcatConstantMerge>,
       // Merge the adjacent extracts on constants
       ApplyRuleToChildren<kind::BITVECTOR_CONCAT, ExtractWhole>>::apply(node);
-  return RewriteResponse(REWRITE_DONE, resultNode);
+  return RewriteResponse(resultNode != node ? REWRITE_AGAIN : REWRITE_DONE, resultNode);
 }
 
 RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite)
@@ -284,7 +290,7 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite)
     }
   }
 
-  return RewriteResponse(REWRITE_DONE, resultNode);
+  return RewriteResponse(resultNode != node ? REWRITE_AGAIN : REWRITE_DONE, resultNode);
 }
 
 RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite)
@@ -306,7 +312,7 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite)
     }
   }
 
-  return RewriteResponse(REWRITE_DONE, resultNode);
+  return RewriteResponse(resultNode != node ? REWRITE_AGAIN : REWRITE_DONE, resultNode);
 }
 
 RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite)
@@ -332,7 +338,7 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite)
     }
   }
 
-  return RewriteResponse(REWRITE_DONE, resultNode);
+  return RewriteResponse(resultNode != node ? REWRITE_AGAIN : REWRITE_DONE, resultNode);
 }
 
 RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool prerewrite) {
@@ -422,31 +428,22 @@ RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool prerewrite){
 
 RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) {
   Node resultNode = node;
-
-  /*
-  RewriteResponse response = rules::NegIdemp(node);
-  if (response.d_node != node)
-  {
-    return response;
-  }
-  */
-
   resultNode = LinearRewriteStrategy
     < RewriteRule<EvalNeg>,
       RewriteRule<NegIdemp>,
       RewriteRule<NegSub>
       >::apply(node);
   
-  if (RewriteRule<NegPlus>::applies(node)) {
-    resultNode = RewriteRule<NegPlus>::run<false>(node);
+  if (RewriteRule<NegPlus>::applies(resultNode)) {
+    resultNode = RewriteRule<NegPlus>::run<false>(resultNode);
     if (resultNode != node) {
       return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
     }
   }
   
   if(!prerewrite) {
-    if (RewriteRule<NegMult>::applies(node)) {
-      resultNode = RewriteRule<NegMult>::run<false>(node);
+    if (RewriteRule<NegMult>::applies(resultNode)) {
+      resultNode = RewriteRule<NegMult>::run<false>(resultNode);
       if (resultNode != node) {
         return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
       }
@@ -481,7 +478,9 @@ RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool prerewrite){
 
   if(RewriteRule<UdivPow2>::applies(node)) {
     resultNode = RewriteRule<UdivPow2>::run <false> (node);
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    if (resultNode != node) {
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
   }
 
   resultNode =
@@ -496,7 +495,9 @@ RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool prerewrite)
 
   if(RewriteRule<UremPow2>::applies(node)) {
     resultNode = RewriteRule<UremPow2>::run <false> (node);
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    if (resultNode != node) {
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
   }
 
   resultNode = LinearRewriteStrategy
@@ -534,7 +535,9 @@ RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool prerewrite) {
   Node resultNode = node; 
   if(RewriteRule<ShlByConst>::applies(node)) {
     resultNode = RewriteRule<ShlByConst>::run <false> (node);
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    if (resultNode != node) {
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
   }
 
   resultNode = LinearRewriteStrategy
@@ -549,7 +552,9 @@ RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool prerewrite) {
   Node resultNode = node; 
   if(RewriteRule<LshrByConst>::applies(node)) {
     resultNode = RewriteRule<LshrByConst>::run <false> (node);
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    if (resultNode != node) {
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
   }
 
   resultNode = LinearRewriteStrategy
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 68262e468..90a0debf5 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -50,6 +50,10 @@ Node mkIndexedOp(Kind k, uint32_t arg)
   switch (k) {
     case kind::BITVECTOR_REPEAT:
       return nm->mkConst<BitVectorRepeat>(BitVectorRepeat(arg));
+    case kind::BITVECTOR_SIGN_EXTEND:
+      return nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(arg));
+    case kind::BITVECTOR_ZERO_EXTEND:
+      return nm->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(arg));
     default:
       return Node::null();
   }
@@ -106,7 +110,37 @@ uint32_t getIndex(TNode node, size_t index)
     }
     Unreachable();
   }
-  if (node.getKind() == kind::BITVECTOR_EXTRACT)
+  else if (node.getKind() == kind::BITVECTOR_SIGN_EXTEND)
+  {
+    if (index == 0)
+    {
+      return node.getOperator()
+          .getConst<BitVectorSignExtend>()
+          .d_signExtendAmount;
+    }
+    Unreachable();
+  }
+  else if (node.getKind() == kind::BITVECTOR_ROTATE_LEFT)
+  {
+    if (index == 0)
+    {
+      return node.getOperator()
+          .getConst<BitVectorRotateLeft>()
+          .d_rotateLeftAmount;
+    }
+    Unreachable();
+  }
+  else if (node.getKind() == kind::BITVECTOR_ROTATE_RIGHT)
+  {
+    if (index == 0)
+    {
+      return node.getOperator()
+          .getConst<BitVectorRotateRight>()
+          .d_rotateRightAmount;
+    }
+    Unreachable();
+  }
+  else if (node.getKind() == kind::BITVECTOR_EXTRACT)
   {
     if (index == 0)
     {
@@ -118,7 +152,7 @@ uint32_t getIndex(TNode node, size_t index)
     }
     Unreachable();
   }
-  Unreachable();
+  Unreachable() << node.getKind();
 }
 
 /* ------------------------------------------------------------------------- */
@@ -172,8 +206,13 @@ unsigned isPow2Const(const BitVector& bv)
   {
     return p;
   }
+  return false;
+}
+
+unsigned isNegPow2Const(const BitVector& bv)
+{
   BitVector nbv = -bv;
-  p = nbv.isPow2();
+  unsigned p = nbv.isPow2();
   if (p != 0)
   {
     return p;
@@ -181,6 +220,11 @@ unsigned isPow2Const(const BitVector& bv)
   return false;
 }
 
+uint32_t zeroes(const BitVector& bv) {
+  const Integer& bvVal = bv.toInteger();
+  return bvVal.isZero() ? bv.getSize() : bv.getSize() - bvVal.length();
+}
+
 bool isBvConstTerm(TNode node)
 {
   if (node.getNumChildren() == 0)
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 23d85478b..0418f6510 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -76,6 +76,9 @@ bool isOne(TNode node);
 unsigned isPow2Const(TNode node, bool& isNeg);
 
 unsigned isPow2Const(const BitVector& bv);
+unsigned isNegPow2Const(const BitVector& bv);
+
+uint32_t zeroes(const BitVector& bv);
 
 /* Returns true if node or all of its children is const. */
 bool isBvConstTerm(TNode node);
diff --git a/src/theory/rewriter/compiler.py b/src/theory/rewriter/compiler.py
index d406c5b99..ae686f001 100755
--- a/src/theory/rewriter/compiler.py
+++ b/src/theory/rewriter/compiler.py
@@ -63,6 +63,9 @@ op_to_kind = {
 op_to_const_eval = {
     Op.BVSHL: lambda args: "({}.leftShift({}))".format(args[0], args[1]),
     Op.BVNEG: lambda args: "(-{})".format(args[0]),
+    Op.BVULE: lambda args: f"({args[0]} <= {args[1]})",
+    Op.BVUGE: lambda args: f"({args[0]} >= {args[1]})",
+    Op.BVULT: lambda args: f"({args[0]} < {args[1]})",
     Op.EXTRACT: lambda args: "({2}.extract({0}, {1}))".format(*args),
     Op.BVNOT: lambda args: "(~{})".format(args[0]),
     Op.BVAND: lambda args: "({} & {})".format(args[0], args[1]),
@@ -71,14 +74,17 @@ op_to_const_eval = {
     Op.CONCAT: lambda args: "({}.concat({}))".format(args[0], args[1]),
     Op.PLUS: lambda args: "({} + {})".format(args[0], args[1]),
     Op.MINUS: lambda args: "({} - {})".format(args[0], args[1]),
+    Op.MULT: lambda args: "({} * {})".format(args[0], args[1]),
+    Op.LEQ: lambda args: "({} <= {})".format(args[0], args[1]),
     Op.LT: lambda args: "({} < {})".format(args[0], args[1]),
     Op.GEQ: lambda args: "({} >= {})".format(args[0], args[1]),
     Op.NOT: lambda args: "(!{})".format(args[0]),
     Op.AND: lambda args: "({})".format(" && ".join(args)) if len(args) > 0 else "true",
     Op.OR: lambda args: "({})".format(" || ".join(args)) if len(args) > 0 else "true",
     Op.EQ: lambda args: "({} == {})".format(args[0], args[1]),
-    Op.BITS: lambda args: "bv::utils::bits({})".format(args[0]),
+    Op.ZEROES: lambda args: "bv::utils::zeroes({})".format(args[0]),
     Op.POW2: lambda args: "bv::utils::isPow2Const({})".format(args[0]),
+    Op.NPOW2: lambda args: "bv::utils::isNegPow2Const({})".format(args[0]),
 }
 
 op_to_lfsc = {
@@ -652,6 +658,8 @@ def expr_to_code(expr):
             return "({} == {})".format(args[0], args[1])
         elif expr.op == Op.GET_KIND:
             return f"{args[0]}.getKind()"
+        elif expr.op == Op.IS_BITVECTOR_NODE:
+            return f"{args[0]}.getType().isBitVector()"
         elif expr.op == Op.GET_NUM_CHILDREN:
             return f"{args[0]}.getNumChildren()"
         elif expr.op == Op.BV_SIZE:
@@ -670,16 +678,15 @@ def expr_to_code(expr):
         elif expr.op == Op.MK_NODE:
             kind = expr.children[0].val
 
-            list_arg = None
+            has_list_arg = False
             for child in expr.children:
                 if child.sort and child.sort.base == BaseSort.List:
-                    list_arg = child.sort
+                    has_list_arg = True
                     break
 
             arg_str = None
-            if list_arg:
+            if has_list_arg:
                 vec = fresh_name("__vec")
-                print(expr)
                 default = expr_to_code(
                     default_val(expr.children[0].val, expr.children[1].sort)
                 )
@@ -723,7 +730,7 @@ def expr_to_code(expr):
                     f"std::vector<Node>({args[0]}.begin() + {args[1]}, {args[0]}.end())"
                 )
             else:
-                return f"std::vector<Node>({args[0]}.begin() + {args[1]}, {args[0]}.begin() + {args[2]} + 1)"
+                return f"std::vector<Node>({args[0]}.begin() + {args[1]}, {args[0]}.begin() + {args[2]})"
         elif expr.op == Op.GET_INDEX:
             return "bv::utils::getIndex({}, {})".format(args[0], args[1])
         elif expr.sort and expr.sort.const:
@@ -814,7 +821,7 @@ def cfg_to_code(name, block, cfg):
     if isinstance(block, CFGLoop):
         body = cfg_to_code(name, block.body, cfg)
         return """
-        for ({} = 0; {} < {}.getNumChildren(); {}++) {{
+        for ({} = 0; {} < {}; {}++) {{
          {}
         }}""".format(
             block.loop_var,
@@ -896,6 +903,7 @@ def rule_to_match_ir(cfg, out_block, node_var, out_var, lhs):
         expr, node, match_instrs, const_match_instrs, vars_seen, in_loop, last
     ):
         if expr.sort.base == BaseSort.BitVec:
+            match_instrs.append(Assert(Fn(Op.IS_BITVECTOR_NODE, [node]), in_loop))
             width = expr.sort.children[0]
             if isinstance(width, Var) and not width.name in vars_seen:
                 bv_size_expr = Fn(Op.BV_SIZE, [node])
@@ -1043,14 +1051,14 @@ def rule_to_match_ir(cfg, out_block, node_var, out_var, lhs):
                                 child.children[0].sort = Sort(BaseSort.Bool, [], True)
 
                             remainder_expr = Assign(
-                                list_child, Fn(Op.GET_CHILDREN, [node, var, cond])
+                                list_child, mk_node(Op.GET_CHILDREN, node, var, cond)
                             )
 
                         has_non_remainder = len(nlist_children) != 0
                         last = last and (not has_non_remainder)
                         curr_block = match_instrs
 
-                        if expr.op in nary_ops and has_non_remainder:
+                        if expr.op in nary_ops and len(nlist_children) == len(expr.children):
                             curr_block.append(
                                 Assert(
                                     Fn(
@@ -1101,7 +1109,11 @@ def rule_to_match_ir(cfg, out_block, node_var, out_var, lhs):
                             )
 
                             curr_block.append(
-                                CFGLoop(loop_idx, node, CFGSeq(loop_body))
+                                CFGLoop(
+                                    loop_idx,
+                                    mk_node(Op.GET_NUM_CHILDREN, node),
+                                    CFGSeq(loop_body),
+                                )
                             )
                             if i != 0:
                                 curr_block.append(
@@ -1117,7 +1129,7 @@ def rule_to_match_ir(cfg, out_block, node_var, out_var, lhs):
                             # If we only have a list argument, e.g. (bvadd xs)
                             curr_block.append(remainder_expr)
 
-                        if not prev_in_loop:
+                        if has_non_remainder and not prev_in_loop:
                             match_instrs.append(Assert(BoolConst(False), False))
                     elif expr.op in associative_ops:
                         nlist_children = [
@@ -1126,7 +1138,7 @@ def rule_to_match_ir(cfg, out_block, node_var, out_var, lhs):
                             if child.sort.base != BaseSort.List
                         ]
 
-                        curr_idx = None
+                        next_idx = IntConst(0)
                         curr_block = match_instrs
                         prev_in_loop = in_loop
                         for i, child in list(enumerate(expr.children)):
@@ -1141,30 +1153,38 @@ def rule_to_match_ir(cfg, out_block, node_var, out_var, lhs):
                                 )
                                 conds = []
                                 loop_body = []
-                                if curr_idx:
-                                    cond = Fn(Op.LT, [curr_idx, var_i])
+                                if i != 0:
+                                    cond = mk_node(Op.LEQ, next_idx, var_i)
                                     infer_types(None, cond)
                                     loop_body.append(Assert(cond, in_loop))
-                                else:
-                                    curr_idx = IntConst(0)
 
                                 loop_body.append(
-                                    Assign(child, Fn(Op.SLICE, [node, curr_idx, var_i]))
+                                    Assign(child, Fn(Op.SLICE, [node, next_idx, var_i]))
                                 )
 
-                                curr_idx = var_i
+                                if Op.CONCAT and isinstance(child.sort.children[0].children[0], Var):
+                                    len_var = child.sort.children[0].children[0]
+                                    list_node = Fn(Op.MK_NODE, [KindConst(Op.CONCAT), child])
+                                    list_node.sort = Sort(BaseSort.BitVec, [len_var])
+                                    list_len = Fn(Op.BV_SIZE, [list_node])
+                                    loop_body.append(
+                                        Assign(len_var, list_len)
+                                    )
+
+                                max_val = mk_node(
+                                    Op.PLUS,
+                                    mk_node(Op.GET_NUM_CHILDREN, node),
+                                    IntConst(1),
+                                )
+                                next_idx = var_i
                                 curr_block.append(
-                                    CFGLoop(var_i, node, CFGSeq(loop_body))
+                                    CFGLoop(var_i, max_val, CFGSeq(loop_body))
                                 )
                                 curr_block = loop_body
                             else:
-                                curr_idx = Fn(Op.PLUS, [curr_idx, IntConst(1)])
-                                infer_types(None, curr_idx)
-
-                                cond = Fn(
-                                    Op.LT, [curr_idx, Fn(Op.GET_NUM_CHILDREN, [node])]
+                                cond = mk_node(
+                                    Op.LT, next_idx, mk_node(Op.GET_NUM_CHILDREN, node)
                                 )
-                                infer_types(None, cond)
 
                                 # Make sure that we are not out-of-bounds
                                 curr_block.append(Assert(cond, in_loop))
@@ -1176,7 +1196,7 @@ def rule_to_match_ir(cfg, out_block, node_var, out_var, lhs):
 
                                 # Get child node for loop index
                                 curr_block.append(
-                                    Assign(loop_var, Fn(Op.GET_CHILD, [node, curr_idx]))
+                                    Assign(loop_var, Fn(Op.GET_CHILD, [node, next_idx]))
                                 )
 
                                 last_non_list_child = (
@@ -1186,20 +1206,32 @@ def rule_to_match_ir(cfg, out_block, node_var, out_var, lhs):
                                 if last_non_list_child:
                                     rhs = Fn(
                                         Op.SLICE,
-                                        [node, Fn(Op.PLUS, [curr_idx, IntConst(1)])],
+                                        [node, Fn(Op.PLUS, [next_idx, IntConst(1)])],
                                     )
                                     infer_types(None, rhs)
                                     curr_block.append(Assign(expr.children[-1], rhs))
+
+                                    # TODO: merge with other case
+                                    remainder = expr.children[-1]
+                                    if Op.CONCAT and isinstance(remainder.sort.children[0].children[0], Var):
+                                        len_var = remainder.sort.children[0].children[0]
+                                        list_node = Fn(Op.MK_NODE, [KindConst(Op.CONCAT), remainder])
+                                        list_node.sort = Sort(BaseSort.BitVec, [len_var])
+                                        list_len = Fn(Op.BV_SIZE, [list_node])
+                                        curr_block.append(
+                                            Assign(len_var, list_len)
+                                        )
                                 expr_to_ir(
                                     child,
                                     loop_var,
-                                    loop_body,
+                                    curr_block,
                                     const_match_instrs,
                                     vars_seen,
                                     True,
                                     last=last and (last_child or last_non_list_child),
                                 )
-                        if not prev_in_loop:
+                                next_idx = mk_node(Op.PLUS, next_idx, IntConst(1))
+                        if in_loop and not prev_in_loop:
                             match_instrs.append(Assert(BoolConst(False), False))
                         last = False
                     # Remaining ops
@@ -1235,7 +1267,7 @@ def rule_to_match_ir(cfg, out_block, node_var, out_var, lhs):
             match_instrs.append(Return(out_var))
 
     vars_seen = set()
-    match_instrs = [Assign(out_var, node_var)]
+    match_instrs = []
     const_match_instrs = []
     expr_to_ir(
         lhs,
@@ -1251,6 +1283,7 @@ def rule_to_match_ir(cfg, out_block, node_var, out_var, lhs):
 
 
 def gen_rule(rule):
+    print(f"Compiling {rule.name}")
     node_var = Var("__node", rule.lhs.sort)
     out_var = Var("__ret", Sort(rule.rhs.sort.base, rule.rhs.sort.children))
 
@@ -1269,14 +1302,14 @@ def gen_rule(rule):
     var_counts = defaultdict(int)
     var_counts["__ret"] = 2
     cfg_count_vars(var_counts, match_block)
-    cfg_count_vars(var_counts, cfg)
-    # match_block = cfg_optimize(var_counts, match_block)
+    match_block = cfg_optimize(out_var, var_counts, match_block)
     # cfg = cfg_optimize(var_counts, cfg)
 
     cfg_vars = cfg_collect_vars(match_block)
     var_decls = ""
     for var in cfg_vars:
-        var_decls += "{} {};\n".format(sort_to_code(var.sort), var.name)
+        if var != node_var:
+            var_decls += "{} {};\n".format(sort_to_code(var.sort), var.name)
 
     body = cfg_to_code(name_to_enum(rule.name), match_block, cfg)
 
@@ -1614,6 +1647,7 @@ def rule_to_lfsc(rule):
 
 def type_check(rules):
     for rule in rules:
+        print(f"Type checking {rule.name}")
         infer_types(rule.rvars, rule.lhs)
         assign_names(rule.lhs)
         infer_types(rule.rvars, rule.rhs)
diff --git a/src/theory/rewriter/ir.py b/src/theory/rewriter/ir.py
index bb0422912..989fde4dd 100644
--- a/src/theory/rewriter/ir.py
+++ b/src/theory/rewriter/ir.py
@@ -1,6 +1,6 @@
 from collections import defaultdict
 
-from node import collect_vars, count_vars, subst, BoolConst, Var, Node, Fn
+from node import collect_vars, count_vars, subst, BaseSort, BoolConst, Var, Node, Fn, Op
 
 
 class CFGEdge:
@@ -186,27 +186,43 @@ def optimize_cfg(out_var, entry, cfg):
             edge.cond = subst(edge.cond, substs)
 
 
-def cfg_collect_vars(node):
+def cfg_collect_vars(node, sorts=False):
     cfg_vars = set()
     if isinstance(node, CFGLoop):
         cfg_vars.add(node.loop_var)
-        cfg_vars.update(cfg_collect_vars(node.domain))
-        cfg_vars.update(cfg_collect_vars(node.body))
+        cfg_vars.update(cfg_collect_vars(node.domain, sorts))
+        cfg_vars.update(cfg_collect_vars(node.body, sorts))
     elif isinstance(node, CFGSeq) or isinstance(node, CFGNode):
         for instr in node.instrs:
-            cfg_vars.update(cfg_collect_vars(instr))
+            cfg_vars.update(cfg_collect_vars(instr, sorts))
     elif isinstance(node, CFGCond):
         for case in node.cases:
-            cfg_vars.update(cfg_collect_vars(case[0]))
-            cfg_vars.update(cfg_collect_vars(case[1]))
+            cfg_vars.update(cfg_collect_vars(case[0], sorts))
+            cfg_vars.update(cfg_collect_vars(case[1], sorts))
     elif isinstance(node, Assign):
         cfg_vars.add(node.name)
-        cfg_vars.update(cfg_collect_vars(node.expr))
+        cfg_vars.update(cfg_collect_vars(node.expr, sorts))
+    elif isinstance(node, Assert):
+        cfg_vars.update(cfg_collect_vars(node.expr, sorts))
+    elif isinstance(node, Return):
+        cfg_vars.update(cfg_collect_vars(node.expr, sorts))
+    elif isinstance(node, Return):
+        cfg_vars.update(cfg_collect_vars(node.expr, sorts))
+    elif isinstance(node, Node):
+        if isinstance(node, Var):
+            cfg_vars.add(node)
+        else:
+            for child in node.children:
+                cfg_vars.update(cfg_collect_vars(child, sorts))
+        if sorts and node.sort:
+            for child in node.sort.children:
+                cfg_vars.update(cfg_collect_vars(child, sorts))
     return cfg_vars
 
 def cfg_count_vars(var_counts, node):
     if isinstance(node, CFGLoop):
         var_counts[node.loop_var.name] += 1
+        cfg_count_vars(var_counts, node.body)
     elif isinstance(node, CFGSeq) or isinstance(node, CFGNode):
         for instr in node.instrs:
             cfg_count_vars(var_counts, instr)
@@ -218,23 +234,44 @@ def cfg_count_vars(var_counts, node):
         cfg_count_vars(var_counts, node.expr)
     elif isinstance(node, Assert):
         cfg_count_vars(var_counts, node.expr)
+    elif isinstance(node, Return):
+        cfg_count_vars(var_counts, node.expr)
     elif isinstance(node, Node):
+        # TODO: Hack-y way to avoid eliminating list variables
+        if isinstance(node, Fn):
+            if node.op == Op.SLICE:
+                cfg_count_vars(var_counts, node.children[0])
+            elif node.op == Op.MK_NODE:
+                for child in node.children:
+                    print(child)
+                    if child.sort and child.sort.base == BaseSort.List:
+                        cfg_count_vars(var_counts, child)
+
         if isinstance(node, Var):
             var_counts[node.name] += 1
         else:
             for child in node.children:
                 cfg_count_vars(var_counts, child)
+        if node.sort:
+            for child in node.sort.children:
+                cfg_count_vars(var_counts, child)
+
 
-def cfg_optimize(var_counts, node):
+def cfg_optimize(out_var, var_counts, node):
+    print(var_counts)
     def remove_unused_vars(node):
         if isinstance(node, CFGLoop):
-            node
+            new_body = remove_unused_vars(node.body)
+            return CFGLoop(node.loop_var, node.domain, new_body)
         elif isinstance(node, CFGSeq) or isinstance(node, CFGNode):
             new_instrs = []
             for instr in node.instrs:
                 new_instr = remove_unused_vars(instr)
                 if new_instr:
-                    new_instrs.append(new_instr)
+                    if isinstance(new_instr, CFGSeq):
+                        new_instrs.extend(new_instr.instrs)
+                    else:
+                        new_instrs.append(new_instr)
             return CFGSeq(new_instrs)
         elif isinstance(node, CFGCond):
             new_cases = []
@@ -250,7 +287,8 @@ def cfg_optimize(var_counts, node):
     substs = dict()
     def elim_single_use_vars(node):
         if isinstance(node, CFGLoop):
-            node
+            new_body = elim_single_use_vars(node.body)
+            return CFGLoop(node.loop_var, node.domain, new_body)
         elif isinstance(node, CFGSeq) or isinstance(node, CFGNode):
             new_instrs = []
             for instr in node.instrs:
@@ -267,6 +305,8 @@ def cfg_optimize(var_counts, node):
             res = None
             new_expr = elim_single_use_vars(node.expr)
             if var_counts[node.name.name] == 1:
+                # TODO: hack-y type inference
+                new_expr.sort = node.name.sort
                 substs[node.name.name] = new_expr
             else:
                 res = Assign(node.name, new_expr)
@@ -288,7 +328,53 @@ def cfg_optimize(var_counts, node):
         else:
             return node
 
-    return elim_single_use_vars(remove_unused_vars(node))
+    def delay_assigns(delayed_assigns, node):
+        if isinstance(node, CFGLoop):
+            new_body = delay_assigns(delayed_assigns, node.body)
+            return CFGLoop(node.loop_var, node.domain, new_body)
+        elif isinstance(node, CFGSeq) or isinstance(node, CFGNode):
+            new_instrs = []
+            for instr in node.instrs:
+                new_instr = delay_assigns(delayed_assigns, instr)
+                if new_instr:
+                    new_instrs.append(new_instr)
+            return CFGSeq(new_instrs)
+        elif isinstance(node, CFGCond):
+            instrs = []
+            new_cases = []
+            for case in node.cases:
+                cond_vars = cfg_collect_vars(case[0], True)
+
+                for delayed_assign in delayed_assigns:
+                    if delayed_assign.name in cond_vars:
+                        instrs.extend(delayed_assigns)
+                        delayed_assigns.clear()
+                        break
+
+                new_cases.append((case[0], delay_assigns(delayed_assigns, case[1])))
+            return CFGSeq(instrs + [CFGCond(new_cases)])
+        elif isinstance(node, Assign):
+            if node.name != out_var:
+                delayed_assigns.append(node)
+                return None
+            else:
+                return CFGSeq(delayed_assigns + [node])
+        elif isinstance(node, Assert):
+            expr_vars = cfg_collect_vars(node.expr, True)
+            instrs = []
+            print("DELAYED", delayed_assigns)
+            print("DELAYED", expr_vars)
+            for delayed_assign in delayed_assigns:
+                if delayed_assign.name in expr_vars:
+                    instrs.extend(delayed_assigns)
+                    delayed_assigns.clear()
+                    break
+            instrs.append(node)
+            return CFGSeq(instrs)
+        else:
+            return node
+
+    return delay_assigns([], elim_single_use_vars(remove_unused_vars(node)))
 
 def cfg_to_str(cfg):
     result = ''
diff --git a/src/theory/rewriter/node.py b/src/theory/rewriter/node.py
index d78518d61..96b6fb68f 100644
--- a/src/theory/rewriter/node.py
+++ b/src/theory/rewriter/node.py
@@ -79,8 +79,10 @@ class Op(Enum):
     PLUS = auto()
     MINUS = auto()
     MULT = auto()
+    LEQ = auto()
     LT = auto()
     GEQ = auto()
+    LEFT_SHIFT = auto()
 
     ###########################################################################
     # Theory-independent
@@ -94,6 +96,7 @@ class Op(Enum):
     ###########################################################################
 
     GET_KIND = auto()
+    IS_BITVECTOR_NODE = auto()
     GET_CHILD = auto()
     GET_CHILDREN = auto()
     GET_NUM_CHILDREN = auto()
@@ -106,7 +109,8 @@ class Op(Enum):
     BV_VAL = auto()
     APPEND = auto()
     POW2 = auto()
-    BITS = auto()
+    NPOW2 = auto()
+    ZEROES = auto()
     SLICE = auto()
 
     ###########################################################################
@@ -136,6 +140,7 @@ class BaseSort(Enum):
     Int = auto()
     Kind = auto()
     List = auto()
+    Node = auto()
     Fail = auto()
 
 
@@ -329,7 +334,6 @@ def are_types_compatible(t1, t2):
         return are_types_compatible(t1, t2.children[0])
     return False
 
-
 def infer_types(context, node):
     if node.sort:
         # Sort has already been computed for this node, skip
@@ -367,7 +371,7 @@ def infer_types(context, node):
                 Op.BVULT, Op.BVULE
         ]:
             assert node.children[0].sort.base == BaseSort.BitVec
-            assert node.children[0].sort == node.children[1].sort
+            # assert node.children[0].sort == node.children[1].sort
             sort = Sort(BaseSort.Bool, [])
         elif node.op in [Op.BVREDAND, Op.BVREDOR]:
             assert node.children[0].sort.base == BaseSort.BitVec
@@ -400,11 +404,17 @@ def infer_types(context, node):
             assert all(
                 are_types_compatible(arg_sort, child.sort)
                 for child in node.children)
-            sort = Sort(BaseSort.BitVec, [
-                Fn(Op.PLUS, [
-                    child.sort.children[0] for child in node.children
-                ])
-            ])
+
+            sizes = []
+            for child in node.children:
+                if child.sort.base == BaseSort.BitVec:
+                    sizes.append(child.sort.children[0])
+                else:
+                    assert child.sort.base == BaseSort.List
+                    sizes.append(child.sort.children[0].children[0])
+
+            total_size = sizes[0] if len(sizes) == 1 else Fn(Op.PLUS, sizes)
+            sort = Sort(BaseSort.BitVec, [total_size])
         elif node.op in [Op.ZERO_EXTEND, Op.SIGN_EXTEND]:
             assert len(node.children) == 2
             assert node.children[0].sort.base == BaseSort.Int
@@ -467,11 +477,11 @@ def infer_types(context, node):
                         node.children[0].sort.children[:])
         elif node.op in [Op.BVCONST]:
             sort = Sort(BaseSort.BitVec, [node.children[1]])
-        elif node.op in [Op.PLUS, Op.MINUS]:
+        elif node.op in [Op.PLUS, Op.MINUS, Op.MULT]:
             assert node.children[0].sort.base == BaseSort.Int
             assert node.children[1].sort.base == BaseSort.Int
             sort = Sort(BaseSort.Int, [])
-        elif node.op in [Op.LT, Op.GEQ]:
+        elif node.op in [Op.LEQ, Op.LT, Op.GEQ]:
             assert node.children[0].sort.base == BaseSort.Int
             assert node.children[1].sort.base == BaseSort.Int
             sort = Sort(BaseSort.Bool, [])
@@ -479,9 +489,9 @@ def infer_types(context, node):
             assert node.children[0].sort.base == BaseSort.Bool
             assert node.children[1].sort.base == BaseSort.Bool
             sort = Sort(BaseSort.Bool, [])
-        elif node.op in [Op.BITS]:
+        elif node.op in [Op.ZEROES]:
             sort = Sort(BaseSort.Int, [], True)
-        elif node.op in [Op.POW2]:
+        elif node.op in [Op.POW2, Op.NPOW2]:
             sort = Sort(BaseSort.Int, [], True)
         elif node.op in [Op.AND, Op.OR]:
             assert all(child.sort.base == BaseSort.Bool or (
@@ -490,10 +500,6 @@ def infer_types(context, node):
                        for child in node.children)
             # TODO: Check that list is used correctly
             sort = Sort(BaseSort.Bool, [])
-            print("######")
-            print(node)
-            print([child.sort for child in node.children])
-            print("######")
         elif node.op == Op.FAIL:
             sort = Sort(BaseSort.Fail, [], True)
         elif node.op == Op.MAP:
@@ -504,6 +510,10 @@ def infer_types(context, node):
         elif node.op == Op.GET_NUM_CHILDREN:
             node.sort = Sort(BaseSort.Int, [], True)
             return
+        elif node.op == Op.GET_CHILDREN:
+            # TODO: Not always correct
+            node.sort = Sort(BaseSort.List, [node.children[0].sort], False)
+            return
         else:
             print('Unsupported operator: {}'.format(node.op))
             assert False
@@ -516,6 +526,9 @@ def infer_types(context, node):
         sort = Sort(BaseSort.Bool, [])
         sort.const = True
 
+    if sort:
+        for child in sort.children:
+            infer_types(context, child)
     node.sort = sort
 
 
@@ -526,3 +539,9 @@ def assign_names(node):
     node.name = fresh_name('node')
     for child in node.children:
         assign_names(child)
+
+def mk_node(op, *args):
+    n = Fn(op, list(args))
+    infer_types(None, n)
+    return n
+
diff --git a/src/theory/rewriter/parser.py b/src/theory/rewriter/parser.py
index 82fa426ad..14707b187 100644
--- a/src/theory/rewriter/parser.py
+++ b/src/theory/rewriter/parser.py
@@ -33,7 +33,7 @@ symbol_to_op = {
     'bvor': Op.BVOR,
     'bvxor': Op.BVXOR,
     'bvnand': Op.BVNAND,
-    'bvnor': Op.BVNOT,
+    'bvnor': Op.BVNOR,
     'bvxnor': Op.BVXNOR,
     'concat': Op.CONCAT,
     'bvite': Op.BVITE,
@@ -49,13 +49,16 @@ symbol_to_op = {
     'xor': Op.XOR,
     '+': Op.PLUS,
     '-': Op.MINUS,
+    '*': Op.MULT,
     '<': Op.LT,
     '>=': Op.GEQ,
+    '<<': Op.LEFT_SHIFT,
     '=': Op.EQ,
     'ite': Op.ITE,
 
     'pow2': Op.POW2,
-    'bits': Op.BITS,
+    'npow2': Op.NPOW2,
+    'zeroes': Op.ZEROES,
 }
 
 
@@ -65,7 +68,7 @@ def bv_to_int(s):
 
 
 def symbol():
-    special_chars = '=' + '_' + '+' + '-' + '<' + '>'
+    special_chars = '=' + '_' + '+' + '-' + '<' + '>' + '*'
     return pp.Word(pp.alphas + special_chars, pp.alphanums + special_chars)
 
 
diff --git a/src/theory/rewriter/rules/basic.rules b/src/theory/rewriter/rules/basic.rules
index a66a93845..0d1b140c2 100644
--- a/src/theory/rewriter/rules/basic.rules
+++ b/src/theory/rewriter/rules/basic.rules
@@ -10,11 +10,9 @@
     ((= p (+ q 1)) (concat xs ((_ extract o r) x) ys)))
 )
 
-/*
-(define-rule ConcatConstantMerge ((n Int :const) (m Int :const) (o Int :const) (p Int :const) (q Int :const) (r Int :const) (xs (_ BitVec n) :list) (ys (_ BitVec m) :list))
-  (concat xs (_ bv o p) (_ bv q r) ys)
-  (concat xs (concat (_ bv o p) (_ bv q r)) ys))
-*/
+(define-rule ConcatConstantMerge ((n Int :const) (m Int :const) (o Int :const) (p Int :const) (c1 (_ BitVec o) :const) (c2 (_ BitVec p) :const) (q Int :const) (r Int :const) (xs (_ BitVec n) :list) (ys (_ BitVec m) :list))
+  (concat xs c1 c2 ys)
+  (concat xs (concat c1 c2) ys))
 
 (define-rule ExtractWhole ((i Int :const) (n Int :const) (x (_ BitVec n)))
   ((_ extract i 0) x)
@@ -25,7 +23,7 @@
 
 (define-rule ExtractExtract ((i Int :const) (j Int :const) (k Int :const) (l Int :const) (x (_ BitVec n)))
   ((_ extract i j) ((_ extract k l) x))
-  ((_ extract (+ k j) (+ l j)) x))
+  ((_ extract (+ i l) (+ j l)) x))
 
 (define-rule SimplifyEq ((x (_ BitVec n)))
   (= x x)
@@ -47,7 +45,7 @@
   ((_ extract i j) (bvxor xs))
   (bvxor (map (lambda (x (_ BitVec n)) ((_ extract i j) x)) xs)))
 
-(define-rule ExtractNot ((i Int :const) (j Int :const) (x (_ BitVec n)))
+(define-rule ExtractNot ((i Int :const) (j Int :const) (n Int :const) (x (_ BitVec n)))
   ((_ extract i j) (bvnot x))
   (bvnot ((_ extract i j) x)))
 
@@ -98,7 +96,7 @@
   (bvneg (bvadd xs))
   (bvadd (map (lambda (x (_ BitVec n)) (bvneg x)) xs)))
 
-(define-rule AndSimplifyRmDups ((x (_ BitVec n)) (xs (_ BitVec n) :list))
+(define-rule AndSimplifyRmDups ((n Int :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
   (bvand x x xs)
   (bvand x xs))
 
@@ -118,7 +116,7 @@
   (bvand x (bvnot x) xs)
   (_ bv 0 n))
 
-(define-rule OrSimplifyRmDups ((x (_ BitVec n)) (xs (_ BitVec n) :list))
+(define-rule OrSimplifyRmDups ((n Int :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
   (bvor x x xs)
   (bvor x xs))
 
@@ -209,15 +207,15 @@
 
 /* IntToBVEliminate: COMPLEX */
 
-(define-rule NandEliminate ((x (_ BitVec n)) (y (_ BitVec n)))
+(define-rule NandEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
     (bvnand x y)
     (bvnot (bvand x y)))
 
-(define-rule NorEliminate ((x (_ BitVec n)) (y (_ BitVec n)))
+(define-rule NorEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
     (bvnor x y)
     (bvnot (bvor x y)))
 
-(define-rule XnorEliminate ((x (_ BitVec n)) (y (_ BitVec n)))
+(define-rule XnorEliminate ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
     (bvxnor x y)
     (bvnot (bvxor x y)))
 
@@ -262,13 +260,13 @@
             (bvadd x_urem_y y)
             (bvneg x_urem_y)))))))
 
-(define-rule ZeroExtendEliminate ((i Int :const) (x (_ BitVec n)))
+(define-rule ZeroExtendEliminate ((n Int :const) (i Int :const) (x (_ BitVec n)))
   ((_ zero_extend i) x)
   (cond
     ((= i 0) x)
     (concat (_ bv 0 i) x)))
 
-(define-rule SignExtendEliminate ((i Int :const) (n Int :const) (x (_ BitVec n)))
+(define-rule SignExtendEliminate ((n Int :const) (i Int :const) (n Int :const) (x (_ BitVec n)))
   ((_ sign_extend i) x)
   (cond
     ((= i 0) x)
@@ -286,13 +284,13 @@
  * Simplification
  ******************************************************************************/
 
-(define-rule BvIteConstCond ((m (_ BitVec 1) :const) (x (_ BitVec n)) (y (_ BitVec n)))
+(define-rule BvIteConstCond ((n Int :const) (m (_ BitVec 1) :const) (x (_ BitVec n)) (y (_ BitVec n)))
   (bvite m x y)
   (cond
     ((= m (_ bv 1 1)) x)
     y))
 
-(define-rule BvIteEqualChildren ((c (_ BitVec 1)) (x (_ BitVec m)))
+(define-rule BvIteEqualChildren ((m Int :const) (c (_ BitVec 1)) (x (_ BitVec m)))
   (bvite c x x)
   x)
 
@@ -302,27 +300,27 @@
     ((and (= n (_ bv 1 1)) (= m (_ bv 0 1))) c)
     (true (bvnot c))))
 
-(define-rule BvIteEqualCondThen ((c (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)) (z (_ BitVec n)))
+(define-rule BvIteEqualCondThen ((n Int :const) (c (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)) (z (_ BitVec n)))
   (bvite c (bvite c x y) z)
   (bvite c x z))
 
-(define-rule BvIteEqualCondElse ((c (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)) (z (_ BitVec n)))
+(define-rule BvIteEqualCondElse ((n Int :const) (c (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)) (z (_ BitVec n)))
   (bvite c x (bvite c y z))
   (bvite c x z))
 
-(define-rule BvIteMergeThenIf ((c0 (_ BitVec 1)) (c1 (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)))
+(define-rule BvIteMergeThenIf ((n Int :const) (c0 (_ BitVec 1)) (c1 (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)))
   (bvite c0 (bvite c1 x y) x)
   (bvite (bvand c0 (bvnot c1)) y x))
 
-(define-rule BvIteMergeElseIf ((c0 (_ BitVec 1)) (c1 (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)))
+(define-rule BvIteMergeElseIf ((n Int :const) (c0 (_ BitVec 1)) (c1 (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)))
   (bvite c0 (bvite c1 x y) y)
   (bvite (bvand c0 c1) x y))
 
-(define-rule BvIteMergeThenElse ((c0 (_ BitVec 1)) (c1 (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)))
+(define-rule BvIteMergeThenElse ((n Int :const) (c0 (_ BitVec 1)) (c1 (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)))
   (bvite c0 x (bvite c1 x y))
   (bvite (bvand (bvnot c0) (bvnot c1)) y x))
 
-(define-rule BvIteMergeElseElse ((c0 (_ BitVec 1)) (c1 (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)))
+(define-rule BvIteMergeElseElse ((n Int :const) (c0 (_ BitVec 1)) (c1 (_ BitVec 1)) (x (_ BitVec n)) (y (_ BitVec n)))
   (bvite c0 x (bvite c1 y x))
   (bvite (bvand (bvnot c0) c1) y x))
 
@@ -353,34 +351,62 @@
     ((>= n m) ((_ repeat m) ((_ extract (- m 1) (- m 1)) x)))
     (concat ((_ repeat n) ((_ extract (- m 1) (- m 1)) x)) ((_ extract (- m 1) n) x))))
 
-/*
-(define-rule AndPullUp ((n Int :const) (m Int :const) (o Int :const) (p Int :const) (i Int :const) (xs (_ BitVec m) :list) (ys (_ BitVec o) :list) (zs (_ BitVec p) :list))
-  (bvand (concat xs (_ bv i n) ys) zs)
+(define-rule AndPullUp ((n Int :const) (m Int :const) (o Int :const) (p Int :const) (c (_ BitVec n) :const) (xs (_ BitVec m) :list) (ys (_ BitVec o) :list) (zs (_ BitVec p) :list))
+  (bvand zs (concat xs c ys))
   (cond
-    ((or (= i 0) (= i 1) (= (_ bv i n) (bvnot (_ bv 0 n))))
-      (concat
-        (bvand ((_ extract (- p 1) (+ n o)) (bvand zs)) (concat xs))
-        (bvand ((_ extract (- (+ n o) 1) o) (bvand zs)) (_ bv i n))
-        (bvand ((_ extract (- o 1) 0) (bvand zs)) (concat ys))))))
-
-(define-rule OrPullUp ((n Int :const) (m Int :const) (o Int :const) (p Int :const) (i Int :const) (xs (_ BitVec m) :list) (ys (_ BitVec o) :list) (zs (_ BitVec p) :list))
-  (bvor (concat xs (_ bv i n) ys) zs)
+    ((or (= c (_ bv 0 n)) (= c (_ bv 1 n)) (= c (bvnot (_ bv 0 n))))
+      (cond
+        ((= m 0)
+          (concat
+            (bvand ((_ extract (- (+ n o) 1) o) (bvand zs)) c)
+            (bvand ((_ extract (- o 1) 0) (bvand zs)) (concat ys))))
+        ((= o 0)
+          (concat
+            (bvand ((_ extract (- p 1) n) (bvand zs)) (concat xs))
+            (bvand ((_ extract (- n 1) 0) (bvand zs)) c)))
+        (true
+          (concat
+            (bvand ((_ extract (- p 1) (+ n o)) (bvand zs)) (concat xs))
+            (bvand ((_ extract (- (+ n o) 1) o) (bvand zs)) c)
+            (bvand ((_ extract (- o 1) 0) (bvand zs)) (concat ys))))))))
+
+(define-rule OrPullUp ((n Int :const) (m Int :const) (o Int :const) (p Int :const) (c (_ BitVec n) :const) (xs (_ BitVec m) :list) (ys (_ BitVec o) :list) (zs (_ BitVec p) :list))
+  (bvor zs (concat xs c ys))
   (cond
-    ((or (= i 0) (= i 1) (= (_ bv i n) (bvnot (_ bv 0 n))))
-      (concat
-        (bvor ((_ extract (- p 1) (+ n o)) (bvor zs)) (concat xs))
-        (bvor ((_ extract (- (+ n o) 1) o) (bvor zs)) (_ bv i n))
-        (bvor ((_ extract (- o 1) 0) (bvor zs)) (concat ys))))))
-
-(define-rule XorPullUp ((n Int :const) (m Int :const) (o Int :const) (p Int :const) (i Int :const) (xs (_ BitVec m) :list) (ys (_ BitVec o) :list) (zs (_ BitVec p) :list))
-  (bvxor (concat xs (_ bv i n) ys) zs)
+    ((or (= c (_ bv 0 n)) (= c (_ bv 1 n)) (= c (bvnot (_ bv 0 n))))
+      (cond
+        ((= m 0)
+          (concat
+            (bvor ((_ extract (- (+ n o) 1) o) (bvor zs)) c)
+            (bvor ((_ extract (- o 1) 0) (bvor zs)) (concat ys))))
+        ((= o 0)
+          (concat
+            (bvor ((_ extract (- p 1) n) (bvor zs)) (concat xs))
+            (bvor ((_ extract (- n 1) 0) (bvor zs)) c)))
+        (true
+          (concat
+            (bvor ((_ extract (- p 1) (+ n o)) (bvor zs)) (concat xs))
+            (bvor ((_ extract (- (+ n o) 1) o) (bvor zs)) c)
+            (bvor ((_ extract (- o 1) 0) (bvor zs)) (concat ys))))))))
+
+(define-rule XorPullUp ((n Int :const) (m Int :const) (o Int :const) (p Int :const) (c (_ BitVec n) :const) (xs (_ BitVec m) :list) (ys (_ BitVec o) :list) (zs (_ BitVec p) :list))
+  (bvxor zs (concat xs c ys))
   (cond
-    ((or (= i 0) (= i 1) (= (_ bv i n) (bvnot (_ bv 0 n))))
-      (concat
-        (bvxor ((_ extract (- p 1) (+ n o)) (bvxor zs)) (concat xs))
-        (bvxor ((_ extract (- (+ n o) 1) o) (bvxor zs)) (_ bv i n))
-        (bvxor ((_ extract (- o 1) 0) (bvxor zs)) (concat ys))))))
-*/
+    ((or (= c (_ bv 0 n)) (= c (_ bv 1 n)) (= c (bvnot (_ bv 0 n))))
+      (cond
+        ((= m 0)
+          (concat
+            (bvxor ((_ extract (- (+ n o) 1) o) (bvxor zs)) c)
+            (bvxor ((_ extract (- o 1) 0) (bvxor zs)) (concat ys))))
+        ((= o 0)
+          (concat
+            (bvxor ((_ extract (- p 1) n) (bvxor zs)) (concat xs))
+            (bvxor ((_ extract (- n 1) 0) (bvxor zs)) c)))
+        (true
+          (concat
+            (bvxor ((_ extract (- p 1) (+ n o)) (bvxor zs)) (concat xs))
+            (bvxor ((_ extract (- (+ n o) 1) o) (bvxor zs)) c)
+            (bvxor ((_ extract (- o 1) 0) (bvxor zs)) (concat ys))))))))
 
 (define-rule XorOne ((n Int :const) (xs (_ BitVec n) :list))
   (bvxor (bvnot (_ bv 0 n)) xs)
@@ -390,27 +416,27 @@
   (bvxor (_ bv 0 n) xs)
   (bvxor xs))
 
-(define-rule NotXor ((x (_ BitVec n)) (xs (_ BitVec n) :list))
+(define-rule NotXor ((n Int :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
   (bvnot (bvxor x xs))
   (bvxor (bvnot x) xs))
 
-(define-rule NotIdemp ((x (_ BitVec n)))
+(define-rule NotIdemp ((n Int :const) (x (_ BitVec n)))
     (bvnot (bvnot x))
     x)
 
-(define-rule LtSelfUlt ((x (_ BitVec n)))
+(define-rule LtSelfUlt ((n Int :const) (x (_ BitVec n)))
     (bvult x x)
     false)
 
-(define-rule LtSelfSlt ((x (_ BitVec n)))
+(define-rule LtSelfSlt ((n Int :const) (x (_ BitVec n)))
     (bvslt x x)
     false)
 
-(define-rule LteSelfUle ((x (_ BitVec n)))
+(define-rule LteSelfUle ((n Int :const) (x (_ BitVec n)))
     (bvule x x)
     true)
 
-(define-rule LteSelfSle ((x (_ BitVec n)))
+(define-rule LteSelfSle ((n Int :const) (x (_ BitVec n)))
     (bvsle x x)
     true)
 
@@ -460,27 +486,25 @@
     (not (bvule x y))
     (bvult y x))
 
-/*
-(define-rule MultPowX ((n Int :const) (c Int :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
-    (bvmul (_ bv c n) xs)
+(define-rule MultPowX ((n Int :const) (c (_ BitVec n) :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
+    (bvmul c xs)
     (cond 
-      ((>= (pow2 c) n) (_ bv 0 n))
-      ((< 0 (pow2 c)) (concat ((_ extract (- n (+ (pow2 c) 1)) 0) (bvmul xs)) (_ bv 0 (pow2 c))))))
-*/
+      ((< n (pow2 c)) (_ bv 0 n))
+      ((= 1 (pow2 c)) (bvmul xs))
+      ((< 0 (pow2 c)) (concat ((_ extract (- n (pow2 c)) 0) (bvmul xs)) (_ bv 0 (- (pow2 c) 1))))))
 
-/* TODO: make pow2 neg */
-/*
-(define-rule MultPowXNeg ((n Int :const) (c Int :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
-    (bvmul (_ bv c n) xs)
+(define-rule MultPowXNeg ((n Int :const) (c (_ BitVec n) :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
+    (bvmul c xs)
     (cond 
-      ((>= (pow2 c) n) (_ bv 0 n))
-      ((< 0 (pow2 c)) (concat ((_ extract (- n (+ (pow2 c) 1)) 0) (bvneg (bvmul xs))) (_ bv 0 (pow2 c))))))
+      ((< n (npow2 c)) (_ bv 0 n))
+      ((= 1 (npow2 c)) (bvneg (bvmul xs)))
+      ((and (< 1 n) (< 0 (npow2 c))) (concat ((_ extract (- n (npow2 c)) 0) (bvneg (bvmul xs))) (_ bv 0 (- (npow2 c) 1))))
+      ((< 0 (npow2 c)) (concat ((_ extract (- n (npow2 c)) 0) (bvneg (bvmul xs))) (_ bv 0 (- (npow2 c) 1))))))
 
-(define-rule ExtractMultLeadingBit ((n1 Int :const) (n2 Int :const) (n3 Int :const) (n4 Int :const) (i Int :const) (j Int :const) (c1 Int :const) (c2 Int :const) (xs (_ BitVec n3) :list) (ys (_ BitVec n4) :list))
-  ((_ extract i j) (bvmul (concat (_ bv c1 n1) xs) (concat (_ bv c2 n2) ys)))
+(define-rule ExtractMultLeadingBit ((n1 Int :const) (n2 Int :const) (n3 Int :const) (n4 Int :const) (i Int :const) (j Int :const) (c1 (_ BitVec n1) :const) (c2 (_ BitVec n1) :const) (xs (_ BitVec n3) :list) (ys (_ BitVec n4) :list))
+  ((_ extract i j) (bvmul (concat c1 xs) (concat c2 ys)))
   (cond
-    ((< (- (+ n1 n1 n3 n3) (+ (- n1 (bits c1)) (- n2 (bits c2)))) j) (_ bv 0 (+ n1 n3)))))
-*/
+    ((< (- (* 2 (+ (- i j) 1)) (+ (zeroes c1) (zeroes c2))) j) (_ bv 0 (+ (- i j) 1)))))
 
 (define-rule NegIdemp ((n Int :const) (x (_ BitVec n)))
     (bvneg (bvneg x))
@@ -490,15 +514,19 @@
 (define-rule UdivPowX ((n Int :const) (c (_ BitVec n) :const) (x (_ BitVec n)))
     (bvudiv x c)
     (cond 
-      ((< 0 (pow2 c)) ((_ extract (- n 1) (pow2 c)) x))))
+      ((= 1 (pow2 c)) x)
+      ((< 0 (pow2 c)) (concat (_ bv 0 (- (pow2 c) 1)) ((_ extract (- n 1) (- (pow2 c) 1)) x)))))
 
 /* TODO: make pow2 neg */
-/*
 (define-rule UdivPowXNeg ((n Int :const) (c (_ BitVec n) :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
     (bvudiv x (_ bv c n))
     (cond 
-      ((< 0 (pow2 c)) (bvneg ((_ extract (- n 1) (pow2 c)) x)))))
-*/
+      ((and (< 1 n) (= 1 (npow2 c))) (bvneg x))
+      ((= 1 (npow2 c)) (bvneg x))
+      ((and (< 1 n) (< 0 (pow2 c)))
+        (bvneg (concat (_ bv 0 (- (npow2 c) 1)) ((_ extract (- n 1) (- (npow2 c) 1)) x))))
+      ((< 0 (pow2 c))
+        (concat (_ bv 0 (- (npow2 c) 1)) ((_ extract (- n 1) (- (npow2 c) 1)) x)))))
 
 (define-rule UdivZero ((n Int :const) (x (_ BitVec n)))
     (bvudiv x (_ bv 0 n))
@@ -512,7 +540,8 @@
 (define-rule UremPowX ((n Int :const) (c (_ BitVec n) :const) (x (_ BitVec n)))
     (bvurem x c)
     (cond 
-      ((< 0 (pow2 c)) ((_ extract (- (pow2 c) 1) 0) x))))
+      ((= 1 (pow2 c)) (_ bv 0 n))
+      ((< 1 (pow2 c)) (concat (_ bv 0 (- n (- (pow2 c) 1))) ((_ extract (- (pow2 c) 2) 0) x)))))
 
 (define-rule UremOne ((n Int :const) (x (_ BitVec n)))
     (bvudiv x (_ bv 1 n))
@@ -544,127 +573,51 @@
     ((= j 0) ((_ sign_extend i) x))
     (true ((_ zero_extend (+ i j)) x))))
 
-(define-rule ZeroExtendEqConst ((i Int :const) (n Int :const) (m Int :const) (x (_ BitVec n)))
-  (= ((_ zero_extend i) x) (_ bv m n))
+(define-rule ZeroExtendEqConst ((n Int :const) (m Int :const) (npm Int :const) (c (_ BitVec npm) :const) (x (_ BitVec n)))
+  (= ((_ zero_extend m) x) c)
   (cond
-    ((= ((_ extract (- (+ n m) 1) n) (_ bv m n)) (_ bv 0 n)) (= x ((_ extract (- n 1) 0) (_ bv m n))))
-    false))
-
-(define-rule UltPlusOne ( (n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
-  (bvult x (bvadd y (_ bv 1 n)))
-  (and (bvult (bvnot y) x) (not (= y (bvnot (_ bv 0 n))))))
-
-/*
-(define-rule MultSltMult ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
-  (bvslt (bvmul ) (bvmul ))
-  (and (bvult (bvnot y) x) (not (= y (bvnot (_ bv 0 n))))))
-*/
+    ((= ((_ extract (- (+ n m) 1) n) c) (_ bv 0 m)) false)
+    (= x ((_ extract (- n 1) 0) c))))
 
-/******************************************************************************
- * Experimental
- ******************************************************************************/
-
-/*
-(define-rule LteSelfUle ((x (_ BitVec n)))
-    (bvule x x)
-    true)
-
-(define-rule NegIdemp ((n Int :const) (x (_ BitVec n)))
-    (bvneg (bvneg x))
-    x)
-
-(define-rule ZeroExtendEliminate ((i Int :const) (x (_ BitVec n)))
-  ((_ zero_extend i) x)
+(define-rule SignExtendEqConst ((n Int :const) (m Int :const) (npm Int :const) (c (_ BitVec npm) :const) (x (_ BitVec n)))
+  (= ((_ sign_extend m) x) c)
   (cond
-    ((= i 0) x)
-    (concat (_ bv 0 i) x)))
-
-
-(define-rule UleMax ((n Int :const) (x (_ BitVec n)))
-    (bvule x (bvnot (_ bv 0 n)))
-    true)
-
-(define-rule AndCancel ((x Bool) (xs Bool :list))
-    (and x (not x) xs)
-    false)
-
-(define-rule AndRemDups ((x Bool) (xs Bool :list))
-    (and x x xs)
-    (and xs))
-
-(define-rule IffTrue ((x Bool))
-  (= true x)
-  x)
-
-(define-rule IffFalse ((x Bool))
-  (= true x)
-  (not x))
-
-(define-rule IffSelf ((x Bool))
-  (= x x)
-  true)
-
-(define-rule IffCancel ((x Bool))
-  (= x (not x))
-  false)
-*/
-
-/* Double eq rules */
-
-
-/*
-(define-rule XorTrue ((x Bool))
-  (xor true x)
-  (not x))
-
-(define-rule XorFalse ((x Bool))
-  (xor false x)
-  x)
-
-(define-rule XorSelf ((x Bool))
-  (xor x x)
-  false)
-
-(define-rule XorSelfNeg ((x Bool))
-  (xor x (not x))
-  true)
-*/
-
-/*
-(define-rule IffCancel ((x Bool) (xs (List Bool)))
-    (and x (not x) xs)
-    false)
-
-(define-rule IffCancel ((x Bool) (xs Bool :list))
-    (and x (not x) xs)
-    false)
-
-; (declare-const x Bool)
-; (declare-const xs Bool)
-; (assert (not (= (and x (not x) xs) false)))
-; (check-sat)
-;
-; ^^^
-; Make argument for why it is sufficient to only check this form
-
-; :list/:multiple
+    ((or
+      (and (= ((_ extract (- n 1) (- n 1)) c) (_ bv 0 1)) (= ((_ extract (- (+ m n) 1) n) c) (_ bv 0 (- (+ n m) 1))))
+      (and (= ((_ extract (- n 1) (- n 1)) c) (_ bv 1 1)) (= ((_ extract (- (+ m n) 1) n) c) (bvnot (_ bv 0 (- (+ n m) 1))))))
+    (= x ((_ extract (- n 1) 0) c)))
+    false))
 
-(define-rule IffCancel ((x Bool))
-    (! and x x :binary)
-    x)
+(define-rule ZeroExtendUltConstLhs ((n Int :const) (m Int :const) (npm Int :const) (c (_ BitVec npm) :const) (x (_ BitVec n)))
+  (bvult ((_ zero_extend m) x) c)
+  (cond
+    ((and (not (= n npm)) (= ((_ extract (- (+ n m) 1) n) c) (_ bv 0 m))) (bvult x ((_ extract (- n 1) 0) c)))))
 
-; (and t t s u)
-; (and t (and t (and s u)))
-; (and (and (and t t) s) u)
+(define-rule ZeroExtendUltConstRhs ((n Int :const) (m Int :const) (npm Int :const) (c (_ BitVec npm) :const) (x (_ BitVec n)))
+  (bvult c ((_ zero_extend m) x))
+  (cond
+    ((and (not (= n npm)) (= ((_ extract (- (+ n m) 1) n) c) (_ bv 0 m))) (bvult ((_ extract (- n 1) 0) c) x))))
 
-; have an attribute for fixed number of children
+(define-rule SignExtendUltConstLhs ((n Int :const) (m Int :const) (npm Int :const) (c (_ BitVec npm) :const) (x (_ BitVec n)))
+  (bvult ((_ sign_extend m) x) c)
+  (let ((n1 (- n 1)))
+    (cond
+      ((or (bvule c (bvshl (_ bv 1 npm) (_ bv n1 npm))) (bvuge c (bvshl (bvnot (_ bv 0 npm)) (_ bv n1 npm)))) (bvult x ((_ extract n1 0) c)))
+      ((and (bvult (bvshl (_ bv 1 npm) (_ bv n1 npm)) c) (bvule c (bvshl (bvnot (_ bv 0 npm)) (_ bv n1 npm)))) (= ((_ extract n1 n1) x) (_ bv 0 1)))
+    )
+  )
+)
 
-(define-rule IffCancelTwo ((x Bool))
-    (= (not x) x)
-    false)
+(define-rule SignExtendUltConstRhs ((n Int :const) (m Int :const) (npm Int :const) (c (_ BitVec npm) :const) (x (_ BitVec n)))
+  (bvult c ((_ sign_extend m) x))
+  (let ((n1 (- n 1)))
+    (cond
+      ((or (bvult c (bvshl (_ bv 1 npm) (_ bv n1 npm))) (bvuge c (bvnot (bvshl (_ bv 1 npm) (_ bv n1 npm))))) (bvult ((_ extract n1 0) c) x))
+      ((and (bvule (bvnot (bvshl (bvnot (_ bv 0 npm)) (_ bv n1 npm))) c) (bvule c (bvnot (bvshl (_ bv 1 npm) (_ bv n1 npm))))) (= ((_ extract n1 n1) x) (_ bv 1 1)))
+    )
+  )
+)
 
-; (declare-rule ...)
-; (define-strategy
-; ...
-; )
-*/
+(define-rule UltPlusOne ( (n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
+  (bvult x (bvadd y (_ bv 1 n)))
+  (and (bvult (bvnot y) x) (not (= y (bvnot (_ bv 0 n))))))