3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
This commit is contained in:
Nikolaj Bjorner 2023-08-17 15:18:36 -07:00
commit 2dbf9bcab2

View file

@ -43,6 +43,8 @@ struct mbp_basic_tg::impl {
void mark_seen(expr *t) { m_seen.mark(t); }
bool is_seen(expr *t) { return m_seen.is_marked(t); }
//Split on all ite terms, irrespective of whether
//they contain variables/are c-ground
bool apply() {
if (!m_use_mdl) return false;
expr *term, *c, *th, *el;
@ -60,7 +62,6 @@ struct mbp_basic_tg::impl {
SASSERT(!m.is_implies(term));
if (is_seen(term)) continue;
if (m_tg.is_cgr(term)) continue;
if (m.is_ite(term, c, th, el)) {
mark_seen(term);
progress = true;