mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 11:55:51 +00:00
Code Activity

fix #3045 fix #3046

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-19 07:22:10 -08:00
parent 290b4dfabc
commit a4d81b2847
3 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/tactic/core/pb_preprocess_tactic.cpp
View file

@ -418,8 +418,7 @@ private:
}
bool pure_args(app* a) const {
for (unsigned i = 0; i < a->get_num_args(); ++i) {
expr* e = a->get_arg(i);
for (expr* e : *a) {
m.is_not(e, e);
if (!is_uninterp_const(e) && !m.is_true(e) && !m.is_false(e)) {
return false;
@ -566,7 +565,8 @@ private:
}
else if (pb.is_ge(e)) {
app* a = to_app(e);
SASSERT(pure_args(a));
if (!pure_args(a))
return false;
for (unsigned i = 0; i < a->get_num_args(); ++i) {
args.push_back(a->get_arg(i));
coeffs.push_back(pb.get_coeff(a, i));
@ -575,9 +575,10 @@ private:
}
else if (m.is_or(e)) {
app* a = to_app(e);
SASSERT(pure_args(a));
for (unsigned i = 0; i < a->get_num_args(); ++i) {
args.push_back(a->get_arg(i));
if (!pure_args(a))
return false;
for (expr* arg : *a) {
args.push_back(arg);
coeffs.push_back(rational::one());
}
k = rational::one();