diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp
index 83a1f3c58..190acecdf 100644
--- a/src/qe/mbp/mbp_term_graph.cpp
+++ b/src/qe/mbp/mbp_term_graph.cpp
@@ -1177,7 +1177,7 @@ class term_graph::projector {
     }
 
     void lits2pure(expr_ref_vector &res) {
-        expr *e1 = nullptr, *e2 = nullptr, *p1 = nullptr, *p2 = nullptr;
+        expr *e1 = nullptr, *e2 = nullptr, *e = nullptr, *p1 = nullptr, *p2 = nullptr;
         for (auto *lit : m_tg.m_lits) {
             if (m.is_eq(lit, e1, e2)) {
                 if (find_app(e1, p1) && find_app(e2, p2)) {
@@ -1186,6 +1186,13 @@ class term_graph::projector {
                 else
                     TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";);
             }
+            else if (m.is_not(lit, e) && m.is_eq(e, e1, e2)) {
+                if (find_app(e1, p1) && find_app(e2, p2)) {
+                    res.push_back(mk_neq(m, p1, p2));
+                }
+                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))