diff options
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
| -rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index dc91d678e..a65fbd961 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -138,7 +138,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ case kind::TO_INTEGER: return RewriteResponse(REWRITE_DONE, t); case kind::TO_REAL: - return RewriteResponse(REWRITE_DONE, t[0]); + case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]); case kind::POW: return RewriteResponse(REWRITE_DONE, t); case kind::PI: @@ -198,7 +198,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ } return RewriteResponse(REWRITE_DONE, t); case kind::TO_REAL: - return RewriteResponse(REWRITE_DONE, t[0]); + case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]); case kind::TO_INTEGER: if(t[0].isConst()) { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(t[0].getConst<Rational>().floor()))); |