1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 13ee9183f..6f1df5958 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -417,6 +417,9 @@ Node ArithRewriter::rewriteTerm(TNode t){
     return rewritePlus(t);
   }else if(t.getKind() == kind::DIVISION){
     return rewriteConstantDiv(t);
+  }else if(t.getKind() == kind::MINUS){
+    Node sub = makeSubtractionNode(t[0],t[1]);
+    return rewrite(sub);
   }else{
     Unreachable();
     return Node::null();