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

print deq in lits2pure. fix #6877 (#6878)

Browse source
This commit is contained in:
Hari Govind V K 2023-08-26 23:53:15 -04:00 committed by GitHub
parent 63467f9dfa
commit 5ba06f4e28
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/qe/mbp/mbp_term_graph.cpp
View file

@ -1177,7 +1177,7 @@ class term_graph::projector {
}
void lits2pure(expr_ref_vector &res) {
expr *e1 = nullptr, *e2 = nullptr, *p1 = nullptr, *p2 = nullptr;
expr *e1 = nullptr, *e2 = nullptr, *e = nullptr, *p1 = nullptr, *p2 = nullptr;
for (auto *lit : m_tg.m_lits) {
if (m.is_eq(lit, e1, e2)) {
if (find_app(e1, p1) && find_app(e2, p2)) {
@ -1186,6 +1186,13 @@ class term_graph::projector {
else
TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";);
}
else if (m.is_not(lit, e) && m.is_eq(e, e1, e2)) {
if (find_app(e1, p1) && find_app(e2, p2)) {
res.push_back(mk_neq(m, p1, p2));
}
else
TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";);
}
else if (m.is_distinct(lit)) {
ptr_buffer<expr> diff;
for (expr *arg : *to_app(lit))