Fixed an error in the rewriter Pascal pointed out. This was in effectively dead code...

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 6b38daccedecee1001f369e035a528bc088d4423..345109c5bfaca9b66274641671b6cd88ae218c77 100644 (file)
--- 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());
   }