From f4a7268bd7db85e66f9592c06c1f9fdb99fc6d32 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Nov 2015 14:26:33 -0800
Subject: [PATCH] fix(library/blast/congruence_closure): bug in add_eqv_step

---
 src/library/blast/congruence_closure.cpp |  4 ++--
 tests/lean/run/blast_cc13.lean           | 20 ++++++++++++++++++++
 2 files changed, 22 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/blast_cc13.lean

diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp
index 16a0cbeef..f7c58d62d 100644
--- a/src/library/blast/congruence_closure.cpp
+++ b/src/library/blast/congruence_closure.cpp
@@ -754,7 +754,7 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
     m_entries.insert(eqc_key(R, e1), new_n1);
 
     // The hash code for the parents is going to change
-    remove_parents(R, e1);
+    remove_parents(R, e1_root);
 
     // force all m_root fields in e1 equivalence class to point to e2_root
     bool propagate = R == get_iff_name() && is_true_or_false(e2_root);
@@ -771,7 +771,7 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
         it = new_it_n.m_next;
     } while (it != e1);
 
-    reinsert_parents(R, e1);
+    reinsert_parents(R, e1_root);
 
     // update next of e1_root and e2_root, and size of e2_root
     r1 = m_entries.find(eqc_key(R, e1_root));
diff --git a/tests/lean/run/blast_cc13.lean b/tests/lean/run/blast_cc13.lean
new file mode 100644
index 000000000..e231f085f
--- /dev/null
+++ b/tests/lean/run/blast_cc13.lean
@@ -0,0 +1,20 @@
+set_option blast.subst false
+set_option blast.simp  false
+set_option blast.init_depth 10
+set_option blast.inc_depth  100
+
+example (p : nat → nat → Prop) (f : nat → nat) (a b c d : nat) :
+        p (f a) (f b) → a = c → b = d → b = c → p (f c) (f c) :=
+by blast
+
+example (p : nat → nat → Prop) (a b c d : nat) :
+        p a b → a = c → b = d → p c d :=
+by blast
+
+example (p : nat → nat → Prop) (f : nat → nat) (a b c d : nat) :
+        p (f (f (f (f (f (f a))))))
+          (f (f (f (f (f (f b)))))) →
+        a = c → b = d → b = c →
+        p (f (f (f (f (f (f c))))))
+          (f (f (f (f (f (f c)))))) :=
+by blast