From 4d26aabd83a607c0187ce332b96c92608f0bf840 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Nov 2020 07:12:37 -0800 Subject: [PATCH] fix bug in rewriting of power Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 594ded1b3..a17172fb1 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1305,8 +1305,11 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res } } - if (is_num_y && y.is_minus_one()) { + if (is_num_y && y.is_minus_one()) { result = m_util.mk_div(m_util.mk_real(1), ensure_real(arg1)); + result = m().mk_ite(m().mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))), + m_util.mk_real(0), + result); return BR_REWRITE2; }