From c3b344ec47af068a0704c4fff9b2c8189d08eb0c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Aug 2023 16:51:58 -0700 Subject: [PATCH] fix #6865 Signed-off-by: Nikolaj Bjorner --- src/qe/mbp/mbp_basic_tg.cpp | 23 +++++++---------------- 1 file changed, 7 insertions(+), 16 deletions(-) diff --git a/src/qe/mbp/mbp_basic_tg.cpp b/src/qe/mbp/mbp_basic_tg.cpp index 70d25d89b..d85215d17 100644 --- a/src/qe/mbp/mbp_basic_tg.cpp +++ b/src/qe/mbp/mbp_basic_tg.cpp @@ -47,36 +47,27 @@ struct mbp_basic_tg::impl { //they contain variables/are c-ground bool apply() { if (!m_use_mdl) return false; - expr *term, *c, *th, *el; + expr *c, *th, *el; expr_ref nterm(m); bool progress = false; TRACE("mbp_tg", tout << "Iterating over terms of tg";); // Not resetting terms because get_terms calls resize on terms m_tg.get_terms(terms, false); - for (unsigned i = 0; i < terms.size(); i++) { - term = terms.get(i); - // Unsupported operators - SASSERT(!m.is_and(term)); - SASSERT(!m.is_or(term)); - SASSERT(!m.is_distinct(term)); - SASSERT(!m.is_implies(term)); - - if (is_seen(term)) continue; + for (expr* term : terms) { + if (is_seen(term)) + continue; if (m.is_ite(term, c, th, el)) { mark_seen(term); progress = true; if (m_mdl.is_true(c)) { m_tg.add_lit(c); m_tg.add_eq(term, th); - } else { - if (m.is_not(c)) - nterm = to_app(c)->get_arg(0); - else - nterm = m.mk_not(c); + } + else { + nterm = mk_not(m, c); m_tg.add_lit(nterm); m_tg.add_eq(term, el); } - continue; } } return progress;