bug fix Z3Prover#6934

hgvk94 · Oct 11, 2023 · 63fd5be · 63fd5be
1 parent fcb03aa
commit 63fd5be
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 5 deletions.
diff --git 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
@@ -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);
         };