1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 09cfabdc8..bc8604e85 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -261,11 +261,14 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){
   }else if(reduction.getKind() == kind::LT){
     Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]);
     reduction = currNM->mkNode(kind::NOT, geq);
-  }else if( Options::current()->rewriteArithEqualities && reduction.getKind() == kind::EQUAL){
+  }
+  /* BREADCRUMB : Move this rewrite into preprocessing
+  else if( Options::current()->rewriteArithEqualities && reduction.getKind() == kind::EQUAL){
     Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]);
     Node leq = currNM->mkNode(kind::LEQ, reduction[0], reduction[1]);
     reduction = currNM->mkNode(kind::AND, geq, leq);
   }
+  */
 
 
   return RewriteResponse(REWRITE_DONE, reduction);