diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index becaeb049..d82b3f1bc 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -67,12 +67,22 @@ expr_ref project_plugin::pick_equality(ast_manager& m, model& model, expr* t) {
     for (expr * e1 : *alit) {
         expr *e2;
         val = model(e1);
+        TRACE("qe", tout << mk_pp(e1, m) << " |-> " << val << "\n";);
         if (val2expr.find(val, e2)) {
             return expr_ref(m.mk_eq(e1, e2), m);
         }
         val2expr.insert(val, e1);
         vals.push_back(val);
     }
+    for (unsigned i = 0; i < alit->get_num_args(); ++i) {
+        for (unsigned j = i + 1; j < alit->get_num_args(); ++j) {
+            expr* e1 = alit->get_arg(i);
+            expr* e2 = alit->get_arg(j);
+            val = m.mk_eq(e1, e2);
+            if (model.is_true(val))
+                return expr_ref(m.mk_eq(e1, e2), m);
+        }
+    }
     UNREACHABLE();
     return expr_ref(nullptr, m);
 }