From 586b07613702027fc685e55994e2a325961ca5b7 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 10 Sep 2012 20:38:35 +0000 Subject: Fixed an error in the rewriter Pascal pointed out. This was in effectively dead code. (Nobody internally made minus nodes.) --- src/theory/arith/arith_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/theory/arith') 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()); } -- cgit v1.2.3