From 63fd5be131e29f84379bee057e8cdb5caa0e5733 Mon Sep 17 00:00:00 2001
From: hgvk94 <hgvk94@gmail.com>
Date: Wed, 11 Oct 2023 17:21:39 -0400
Subject: [PATCH] bug fix #6934

---
 src/qe/mbp/mbp_basic_tg.cpp | 7 +++++--
 src/qe/mbp/mbp_qel.cpp      | 6 +++---
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/qe/mbp/mbp_basic_tg.cpp b/src/qe/mbp/mbp_basic_tg.cpp
index 5eca0415141..fa657d990b0 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 5f7c713ffd7..e062369305e 100644
--- a/src/qe/mbp/mbp_qel.cpp
+++ b/src/qe/mbp/mbp_qel.cpp
@@ -179,9 +179,9 @@ class mbp_qel::impl {
                tout << "\n";);
 
         std::function<bool(expr *)> 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 (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_distinct(e))
                 return true;
             return red_vars.is_marked(e);
         };