. '+Outstanding case split in theory arith'

3 files changed, 11 insertions, 6 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 0eb3f2da7..922110765 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -448,6 +448,9 @@ Node ArithRewriter::rewriteTerm(TNode t){
   }else if(t.getKind() == kind::MINUS){
     Node sub = makeSubtractionNode(t[0],t[1]);
     return rewrite(sub);
+  }else if(t.getKind() == kind::UMINUS){
+    Node sub = makeUnaryMinusNode(t[0]);
+    return rewrite(sub);
   }else{
     Unreachable();
     return Node::null();
@@ -481,13 +484,14 @@ Node ArithRewriter::multPnfByNonZero(TNode pnf, Rational& q){
   return result;
 }
 
-
+Node ArithRewriter::makeUnaryMinusNode(TNode n){
+  Node tmp = NodeManager::currentNM()->mkNode(kind::MULT,d_constants->d_NEGATIVE_ONE_NODE,n);
+  return tmp;
+}
 
 Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){
-  using namespace CVC4::kind;
-  NodeManager* currentNM = NodeManager::currentNM();
-  Node negR = currentNM->mkNode(MULT, d_constants->d_NEGATIVE_ONE_NODE, r);
-  Node diff = currentNM->mkNode(PLUS, l, negR);
+  Node negR = makeUnaryMinusNode(r);
+  Node diff = NodeManager::currentNM()->mkNode(kind::PLUS, l, negR);
 
   return diff;
 }
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 184844dbc..611077038 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -77,6 +77,7 @@ private:
   Node rewritePlus(TNode t);
   Node rewriteMinus(TNode t);
   Node makeSubtractionNode(TNode l, TNode r);
+  Node makeUnaryMinusNode(TNode n);
 
 
   Node var2pnf(TNode variable);
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index bdc32ab21..6ff74f0f9 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -428,7 +428,6 @@ Node TheoryArith::simulatePreprocessing(TNode n){
   }else{
     Node rewritten = rewrite(n);
     Kind k = rewritten.getKind();
-    bool negate = false;
 
     if(rewritten.getKind() == NOT){
       Node sub = simulatePreprocessing(rewritten[0]);
@@ -532,6 +531,7 @@ void TheoryArith::check(Effort level){
     }
     if(enqueuedCaseSplit){
       //d_out->caseSplit();
+      Warning() << "Outstanding case split in theory arith" << endl;
     }
   }
 }