From 2288931b4669e2f13b9892a1d9bbc0c1e6268370 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Mon, 11 Jun 2018 22:48:24 -0700
Subject: [PATCH] fix mk_unpure_equalities

---
 src/qe/qe_term_graph.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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();
                 }