1 files changed, 15 insertions, 19 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 30568c3ca..863eb5c31 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -204,34 +204,30 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){
   return RewriteResponse(REWRITE_DONE, res.getNode());
 }
 
-RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){
-  TNode left  = t[0];
-  TNode right = t[1];
+// RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){
+//   TNode left  = t[0];
+//   TNode right = t[1];
 
-  Comparison cmp = Comparison::mkNormalComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right));
+//   Polynomial pLeft = Polynomial::parsePolynomial(left);
+  
 
-  Assert(cmp.isNormalForm());
-  return RewriteResponse(REWRITE_DONE, cmp.getNode());
-}
+//   Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right));
+
+//   Assert(cmp.isNormalForm());
+//   return RewriteResponse(REWRITE_DONE, cmp.getNode());
+// }
 
 RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){
   // left |><| right
   TNode left = atom[0];
   TNode right = atom[1];
 
-  if(right.getMetaKind() == kind::metakind::CONSTANT){
-    return postRewriteAtomConstantRHS(atom);
-  }else{
-    Polynomial pleft = Polynomial::parsePolynomial(left);
-    Polynomial pright = Polynomial::parsePolynomial(right);
-
-    Polynomial diff = pleft - pright;
-
-    Constant cZero = Constant::mkConstant(Rational(0));
-    Node reduction = NodeManager::currentNM()->mkNode(atom.getKind(), diff.getNode(), cZero.getNode());
+  Polynomial pleft = Polynomial::parsePolynomial(left);
+  Polynomial pright = Polynomial::parsePolynomial(right);
 
-    return postRewriteAtomConstantRHS(reduction);
-  }
+  Comparison cmp = Comparison::mkComparison(atom.getKind(), pleft, pright);
+  Assert(cmp.isNormalForm());
+  return RewriteResponse(REWRITE_DONE, cmp.getNode());
 }
 
 RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){