3 files changed, 13 insertions, 6 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 896133e46..13c049c85 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -615,8 +615,7 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<BitwiseEq>::applies(TNode node) {
-  if (node.getKind() != kind::EQUAL ||
-      utils::getSize(node[0]) != 1) {
+  if (node.getKind() != kind::EQUAL) {
     return false;
   }
   TNode term;
@@ -636,11 +635,15 @@ bool RewriteRule<BitwiseEq>::applies(TNode node) {
     case kind::BITVECTOR_AND:
     case kind::BITVECTOR_OR:
       //operator BITVECTOR_XOR 2: "bitwise xor"
-    case kind::BITVECTOR_NOT:
     case kind::BITVECTOR_NAND:
     case kind::BITVECTOR_NOR:
       //operator BITVECTOR_XNOR 2 "bitwise xnor"
     case kind::BITVECTOR_COMP:
+      if (utils::getSize(node[0]) != 1) {
+        return false;
+      }
+      break;
+    case kind::BITVECTOR_NOT:
     case kind::BITVECTOR_NEG:
       return true;
       break;
@@ -678,7 +681,7 @@ Node RewriteRule<BitwiseEq>::apply(TNode node) {
     term = node[0];
   }
 
-  bool eqOne = (c == BitVector(1,(unsigned)1));
+  bool eqOne = (c == BitVector(utils::getSize(node[0]),(unsigned)1));
 
   switch (term.getKind()) {
     case kind::BITVECTOR_AND:
@@ -724,7 +727,7 @@ Node RewriteRule<BitwiseEq>::apply(TNode node) {
         return term[0].eqNode(term[1]).notNode();
       }
     case kind::BITVECTOR_NEG:
-      return term[0].eqNode(utils::mkConst(c));
+      return term[0].eqNode(utils::mkConst(-c));
     default:
       break;
   }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d85d8915b..30b9cd098 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -719,6 +719,7 @@ Node TheoryEngine::preprocess(TNode assertion) {
     // If this is an atom, we preprocess its terms with the theory ppRewriter
     if (Theory::theoryOf(current) != THEORY_BOOL) {
       d_ppCache[current] = ppTheoryRewrite(current);
+      Assert(Rewriter::rewrite(d_ppCache[current]) == d_ppCache[current]);
       continue;
     }
 
@@ -735,6 +736,9 @@ Node TheoryEngine::preprocess(TNode assertion) {
       }
       // Mark the substitution and continue
       Node result = builder;
+      if (result != current) {
+        result = Rewriter::rewrite(result);
+      }
       Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): setting " << current << " -> " << result << endl;
       d_ppCache[current] = result;
       toVisit.pop_back();
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 7e06297fb..d925a3366 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -694,7 +694,7 @@ void UnconstrainedSimplifier::processAssertions(vector<Node>& assertions)
     processUnconstrained();
     //    d_substitutions.print(Message.getStream());
     for (it = assertions.begin(); it != iend; ++it) {
-      (*it) = d_substitutions.apply(*it);
+      (*it) = Rewriter::rewrite(d_substitutions.apply(*it));
     }
   }