mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

fix #3219

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-10 16:21:01 -07:00
parent 0768701744
commit 04a19cd1d8
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1161,6 +1161,10 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
if (!is_num_x && !is_irrat_x) if (!is_num_x && !is_irrat_x)
return BR_FAILED; return BR_FAILED;
if (y.is_zero()) {
return BR_FAILED;
}
rational num_y = numerator(y); rational num_y = numerator(y);
rational den_y = denominator(y); rational den_y = denominator(y);
bool is_neg_y = false; bool is_neg_y = false;