From: Tim King <taking@cs.nyu.edu>
Date: Mon, 10 Sep 2012 20:38:35 +0000 (+0000)
Subject: Fixed an error in the rewriter Pascal pointed out. This was in effectively dead code... 
X-Git-Tag: cvc5-1.0.0~7819
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=586b07613702027fc685e55994e2a325961ca5b7;p=cvc5.git

Fixed an error in the rewriter Pascal pointed out. This was in effectively dead code. (Nobody internally made minus nodes.)
---

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 6b38dacce..345109c5b 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -61,7 +61,7 @@ RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){
     }
   }else{
     Polynomial minuend = Polynomial::parsePolynomial(t[0]);
-    Polynomial subtrahend = Polynomial::parsePolynomial(t[0]);
+    Polynomial subtrahend = Polynomial::parsePolynomial(t[1]);
     Polynomial diff = minuend - subtrahend;
     return RewriteResponse(REWRITE_DONE, diff.getNode());
   }