1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 642216b40..6087ab70f 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -100,6 +100,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
     case kind::PLUS:
       return preRewritePlus(t);
     case kind::MULT:
+    case kind::NONLINEAR_MULT:
       return preRewriteMult(t);
     case kind::INTS_DIVISION:
     case kind::INTS_MODULUS:
@@ -148,6 +149,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
     case kind::PLUS:
       return postRewritePlus(t);
     case kind::MULT:
+    case kind::NONLINEAR_MULT:
       return postRewriteMult(t);
     case kind::INTS_DIVISION:
     case kind::INTS_MODULUS:
@@ -222,7 +224,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
 
 
 RewriteResponse ArithRewriter::preRewriteMult(TNode t){
-  Assert(t.getKind()== kind::MULT);
+  Assert(t.getKind()== kind::MULT || t.getKind()== kind::NONLINEAR_MULT);
 
   if(t.getNumChildren() == 2){
     if(t[0].getKind() == kind::CONST_RATIONAL
@@ -316,7 +318,7 @@ RewriteResponse ArithRewriter::postRewritePlus(TNode t){
 }
 
 RewriteResponse ArithRewriter::postRewriteMult(TNode t){
-  Assert(t.getKind()== kind::MULT);
+  Assert(t.getKind()== kind::MULT || t.getKind()==kind::NONLINEAR_MULT);
 
   Polynomial res = Polynomial::mkOne();