1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index b2f91e070..6f450d08e 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -284,12 +284,12 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
 
 Node TheoryBV::ppRewrite(TNode t)
 {
-  // if (RewriteRule<BitwiseEq>::applies(t)) {
-  //   Node result = RewriteRule<BitwiseEq>::run<false>(t);
-  //   return Rewriter::rewrite(result);
-  // }
+  if (RewriteRule<BitwiseEq>::applies(t)) {
+	Node result = RewriteRule<BitwiseEq>::run<false>(t);
+    return Rewriter::rewrite(result);
+  }
 
-  if (/*options::bitvectorCoreSolver() && */t.getKind() == kind::EQUAL) {
+  if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) {
     std::vector<Node> equalities;
     Slicer::splitEqualities(t, equalities);
     return utils::mkAnd(equalities);