From b2554dcb8f45899ccce84f226cd67b6460442930 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Sat, 16 Jan 2016 11:54:06 -0800
Subject: [PATCH] fix(library/blast/congruence_closure): cannot assume all
 subterms have been internalized

---
 src/library/blast/congruence_closure.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp
index 9827808415..7723d867b3 100644
--- a/src/library/blast/congruence_closure.cpp
+++ b/src/library/blast/congruence_closure.cpp
@@ -1881,7 +1881,9 @@ expr congruence_closure::get_next(name const & R, expr const & e) const {
 }
 
 bool congruence_closure::eq_class_heterogeneous(expr const & e) const {
-    return has_heq_proofs(get_root(get_eq_name(), e));
+    expr root = get_root(get_eq_name(), e);
+    if (auto e = m_entries.find(eqc_key(get_eq_name(), root))) return e->m_heq_proofs;
+    else return false;
 }
 
 unsigned congruence_closure::get_mt(name const & R, expr const & e) const {