diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp
index a0ebf6f33..084391368 100644
--- a/src/qe/qe_term_graph.cpp
+++ b/src/qe/qe_term_graph.cpp
@@ -780,12 +780,15 @@ namespace qe {
                 expr *rep = nullptr;
                 if (!m_root2rep.find(t.get_id(), rep)) return;
                 obj_hashtable<expr> members;
+                members.insert(rep);
                 term const * r = &t;
                 do {
                     expr* member = mk_pure(*r);
                     SASSERT(member);
-                    if (member != rep && (!is_projected(*r) || !is_solved_eq(rep, member))) {
+                    if (!members.contains(member) &&
+                        (!is_projected(*r) || !is_solved_eq(rep, member))) {
                         res.push_back(m.mk_eq(rep, member));
+                        members.insert(member);
                     }
                     r = &r->get_next();
                 }