diff options
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 6 |
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(); |