From a8bb4ba109e6f8cfbbce23789eddfa2350d37a40 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Nov 2015 10:37:44 -0700
Subject: [PATCH] fix(library/blast/congruence_closure): bug in congruence
 closure proof extraction

---
 src/library/blast/congruence_closure.cpp |  8 ++++----
 src/library/blast/congruence_closure.h   |  2 +-
 tests/lean/run/blast_ematch4.lean        | 16 ++++++++++++++++
 3 files changed, 21 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/blast_ematch4.lean

diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp
index 06f0a93c9..9eec3bea6 100644
--- a/src/library/blast/congruence_closure.cpp
+++ b/src/library/blast/congruence_closure.cpp
@@ -654,20 +654,20 @@ void congruence_closure::internalize(expr const & e) {
   This method "inverts" the proof. That is, the m_target goes from root(e) to e after
   we execute it.
 */
-void congruence_closure::invert_trans(name const & R, expr const & e, optional<expr> new_target, optional<expr> new_proof) {
+void congruence_closure::invert_trans(name const & R, expr const & e, bool new_flipped, optional<expr> new_target, optional<expr> new_proof) {
     eqc_key k(R, e);
     auto n = m_entries.find(k);
     lean_assert(n);
     entry new_n = *n;
     if (n->m_target)
-        invert_trans(R, *new_n.m_target, some_expr(e), new_n.m_proof);
+        invert_trans(R, *new_n.m_target, !new_n.m_flipped, some_expr(e), new_n.m_proof);
     new_n.m_target  = new_target;
     new_n.m_proof   = new_proof;
-    new_n.m_flipped = !new_n.m_flipped;
+    new_n.m_flipped = new_flipped;
     m_entries.insert(k, new_n);
 }
 void congruence_closure::invert_trans(name const & R, expr const & e) {
-    invert_trans(R, e, none_expr(), none_expr());
+    invert_trans(R, e, false, none_expr(), none_expr());
 }
 
 void congruence_closure::remove_parents(name const & R, expr const & e) {
diff --git a/src/library/blast/congruence_closure.h b/src/library/blast/congruence_closure.h
index f221963a0..d7cdf12ba 100644
--- a/src/library/blast/congruence_closure.h
+++ b/src/library/blast/congruence_closure.h
@@ -129,7 +129,7 @@ class congruence_closure {
     void mk_entry(name const & R, expr const & e, bool to_propagate);
     void add_occurrence(name const & Rp, expr const & parent, name const & Rc, expr const & child);
     void add_congruence_table(ext_congr_lemma const & lemma, expr const & e);
-    void invert_trans(name const & R, expr const & e, optional<expr> new_target, optional<expr> new_proof);
+    void invert_trans(name const & R, expr const & e, bool new_flipped, optional<expr> new_target, optional<expr> new_proof);
     void invert_trans(name const & R, expr const & e);
     void remove_parents(name const & R, expr const & e);
     void reinsert_parents(name const & R, expr const & e);
diff --git a/tests/lean/run/blast_ematch4.lean b/tests/lean/run/blast_ematch4.lean
new file mode 100644
index 000000000..7e39afb04
--- /dev/null
+++ b/tests/lean/run/blast_ematch4.lean
@@ -0,0 +1,16 @@
+import data.nat
+open algebra nat
+
+section
+open nat
+set_option blast.simp   false
+set_option blast.subst  false
+set_option blast.ematch true
+
+attribute add.comm  [forward]
+attribute add.assoc [forward]
+
+example (a b c : nat) : a + b + b + c = c + b + a + b :=
+by blast
+
+end