From ba6c23bbc5d2e080a75a159d82f8c5c934372c60 Mon Sep 17 00:00:00 2001 From: Hari Govind V K Date: Sat, 14 Oct 2023 04:06:15 -0400 Subject: [PATCH] bug fix #6934 (#6940) --- src/qe/mbp/mbp_basic_tg.cpp | 7 +++++-- src/qe/mbp/mbp_qel.cpp | 3 ++- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/qe/mbp/mbp_basic_tg.cpp b/src/qe/mbp/mbp_basic_tg.cpp index 5eca04151..fa657d990 100644 --- a/src/qe/mbp/mbp_basic_tg.cpp +++ b/src/qe/mbp/mbp_basic_tg.cpp @@ -130,12 +130,15 @@ struct mbp_basic_tg::impl { for (auto a1 : *c) { for (auto a2 : *c) { if (a1 == a2) continue; - if (m_mdl.are_equal(a1, a2)) { + expr_ref e(m.mk_eq(a1, a2), m); + if (m_mdl.is_true(e)) { m_tg.add_eq(a1, a2); eq = true; break; - } else + } else { + SASSERT(m_mdl.is_false(e)); m_tg.add_deq(a1, a2); + } } } if (eq) diff --git a/src/qe/mbp/mbp_qel.cpp b/src/qe/mbp/mbp_qel.cpp index 5f7c713ff..5778419c1 100644 --- a/src/qe/mbp/mbp_qel.cpp +++ b/src/qe/mbp/mbp_qel.cpp @@ -181,7 +181,8 @@ public: std::function non_core = [&](expr *e) { if (is_app(e) && is_partial_eq(to_app(e))) return true; - if (m.is_ite(e) || m.is_or(e) || m.is_implies(e) || m.is_and(e) || m.is_distinct(e)) + if (m.is_ite(e) || m.is_or(e) || m.is_implies(e) || + m.is_distinct(e)) return true; return red_vars.is_marked(e); };