From 215edcf888b7645fd61642309e0a7da22f53f109 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Nov 2019 12:23:03 -0800 Subject: [PATCH] fix; disable rewrite. fix #2715 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 79e414457..e855ec262 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -814,6 +814,7 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul } } +#if 0 if (!m_util.is_int(arg1)) { // (/ (* v1 b) (* v2 d)) --> (* v1/v2 (/ b d)) expr * a, * b, * c, * d; @@ -836,9 +837,12 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul v1 /= v2; result = m_util.mk_mul(m_util.mk_numeral(v1, false), m_util.mk_div(b, d)); + expr_ref z(m_util.mk_real(0), m()); + result = m().mk_ite(m().mk_eq(d, z), m_util.mk_div(arg1, z), result); return BR_REWRITE2; } } +#endif return BR_FAILED; }