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

Merge pull request #708 from dstaple/master

Browse source 
Removed complete() from handling of y.is_zero() in process_power
This commit is contained in:
Nikolaj Bjorner 2016-08-06 09:06:34 -07:00 • committed by GitHub
commit aee6a7fe4c
1 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -410,14 +410,12 @@ struct purify_arith_proc {
expr * x = args[0]; expr * x = args[0];
expr * zero = u().mk_numeral(rational(0), is_int); expr * zero = u().mk_numeral(rational(0), is_int);
expr * one = u().mk_numeral(rational(1), is_int); expr * one = u().mk_numeral(rational(1), is_int);
if (y.is_zero() && complete()) { if (y.is_zero()) {
// (^ x 0) --> k | x != 0 implies k = 1, x = 0 implies k = 0^0 // (^ x 0) --> k | x != 0 implies k = 1, x = 0 implies k = 0^0
push_cnstr(OR(EQ(x, zero), EQ(k, one))); push_cnstr(OR(EQ(x, zero), EQ(k, one)));
push_cnstr_pr(result_pr); push_cnstr_pr(result_pr);
if (complete()) { push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, is_int ? u().mk_0_pw_0_int() : u().mk_0_pw_0_real())));
push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, is_int ? u().mk_0_pw_0_int() : u().mk_0_pw_0_real()))); push_cnstr_pr(result_pr);
push_cnstr_pr(result_pr);
}
} }
else if (!is_int) { else if (!is_int) {
SASSERT(!y.is_int()); SASSERT(!y.is_int());