1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 941394138..cecbefdee 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -261,8 +261,13 @@ 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::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);
 }