3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

update Bool rewriter to pull negations up

This commit is contained in:
Nikolaj Bjorner 2021-08-25 17:50:49 -07:00
parent e6264a80ff
commit 2daf569da6

View file

@ -721,9 +721,18 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
result = m().mk_false();
return BR_DONE;
}
if (m().is_not(rhs))
std::swap(lhs, rhs);
if (m().is_not(lhs, lhs)) {
result = m().mk_not(m().mk_eq(lhs, rhs));
return BR_REWRITE2;
}
if (unfolded) {
result = mk_eq(lhs, rhs);
return BR_DONE;
return BR_REWRITE1;
}
expr *la, *lb, *ra, *rb;