mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix bug in rewriting of power

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-11-09 07:12:37 -08:00
parent f78980c81c
commit 4d26aabd83
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/ast/rewriter/arith_rewriter.cpp
View file

@ -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;
}