From d4885abdc0579ed40bd23848d5e3ee07d1c3bfa7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 17 Oct 2022 11:00:21 -0700
Subject: [PATCH] fix #6400

bi-implication was treated as an atomic formula leading to incorrect projection.
---
 src/cmd_context/extra_cmds/dbg_cmds.cpp | 14 ++++++++++++--
 src/qe/mbp/mbp_term_graph.cpp           | 24 ++++++++----------------
 src/qe/qe_mbi.cpp                       |  9 ++++-----
 3 files changed, 24 insertions(+), 23 deletions(-)

diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp
index c6f0b479a..278c0a205 100644
--- a/src/cmd_context/extra_cmds/dbg_cmds.cpp
+++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp
@@ -405,8 +405,18 @@ public:
         if (!m.is_bool(*m_a) || !m.is_bool(*m_b))
             throw default_exception("interpolation requires two Boolean arguments");
         expr_ref itp(m);
-        mbi.pogo(ctx.get_solver_factory(), *m_a, *m_b, itp);
-        ctx.regular_stream() << itp << "\n";
+        lbool r = mbi.pogo(ctx.get_solver_factory(), *m_a, *m_b, itp);
+        switch (r) {
+        case l_true:
+            ctx.regular_stream() << "sat\n";
+            break;
+        case l_undef:
+            ctx.regular_stream() << "unknown\n";
+            break;
+        case l_false:
+            ctx.regular_stream() << itp << "\n";
+            break;
+        }
     }
 };
 
diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp
index 47cece75a..4709c8c72 100644
--- a/src/qe/mbp/mbp_term_graph.cpp
+++ b/src/qe/mbp/mbp_term_graph.cpp
@@ -307,9 +307,8 @@ namespace mbp {
     term *term_graph::mk_term(expr *a) {
         expr_ref e(a, m);
         term * t = alloc(term, e, m_app2term);
-        if (t->get_num_args() == 0 && m.is_unique_value(a)){
+        if (t->get_num_args() == 0 && m.is_unique_value(a))
             t->mark_as_interpreted();
-        }
 
         m_terms.push_back(t);
         m_app2term.insert(a->get_id(), t);
@@ -700,30 +699,23 @@ namespace mbp {
                         if (p1 != p2) 
                             res.push_back(m.mk_eq(p1, p2));
                     }
-                    else {
+                    else 
                         TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";);
-                    }
                 }
                 else if (m.is_distinct(lit)) {
                     ptr_buffer<expr> diff;
-                    for (expr* arg : *to_app(lit)) {
-                        if (find_app(arg, p1)) {
+                    for (expr* arg : *to_app(lit)) 
+                        if (find_app(arg, p1)) 
                             diff.push_back(p1);
-                        }
-                    }
-                    if (diff.size() > 1) {
+                    if (diff.size() > 1) 
                         res.push_back(m.mk_distinct(diff.size(), diff.data()));
-                    }
-                    else {
+                    else 
                         TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";);
-                    }
                 }
-                else if (find_app(lit, p1)) {
+                else if (find_app(lit, p1)) 
                     res.push_back(p1);
-                }
-                else {
+                else 
                     TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";);
-                }
             }
             remove_duplicates(res);
             TRACE("qe", tout << "literals: " << res << "\n";);            
diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index b261e44be..dea1b11c0 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -127,6 +127,7 @@ namespace qe {
 
     mbi_result prop_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl)  {
         lbool r = m_solver->check_sat(lits);
+        TRACE("qe", tout << r << " " << lits << "\n");
         switch (r) {
         case l_false:
             lits.reset();
@@ -138,12 +139,10 @@ namespace qe {
             for (unsigned i = 0, sz = mdl->get_num_constants(); i < sz; ++i) {
                 func_decl* c = mdl->get_constant(i);
                 if (is_shared(c)) {
-                    if (m.is_true(mdl->get_const_interp(c))) {
+                    if (m.is_true(mdl->get_const_interp(c))) 
                         lits.push_back(m.mk_const(c));
-                    }
-                    else if (m.is_false(mdl->get_const_interp(c))) {
+                    else if (m.is_false(mdl->get_const_interp(c))) 
                         lits.push_back(m.mk_not(m.mk_const(c)));
-                    }
                 }
             }
             return mbi_sat;
@@ -172,7 +171,7 @@ namespace qe {
             if (m_atom_set.contains(a)) {
                 // continue
             }
-            else if (m.is_eq(a)) {
+            else if (m.is_eq(a) && !m.is_iff(a)) {
                 m_atoms.push_back(a);
                 m_atom_set.insert(a);
             }