From 79043177eedb1a36cd232dee95a530932a3852fb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 29 Dec 2016 19:25:29 -0800
Subject: [PATCH] fix(library/tactic/congruence/congruence_closure): bug in the
 interface between cc and ac modules

---
 .../tactic/congruence/congruence_closure.cpp  | 83 ++++++++++---------
 tests/lean/run/cc_ac_bug.lean                 |  2 +
 2 files changed, 44 insertions(+), 41 deletions(-)
 create mode 100644 tests/lean/run/cc_ac_bug.lean

diff --git a/src/library/tactic/congruence/congruence_closure.cpp b/src/library/tactic/congruence/congruence_closure.cpp
index d7b9403de1..3275b0cc75 100644
--- a/src/library/tactic/congruence/congruence_closure.cpp
+++ b/src/library/tactic/congruence/congruence_closure.cpp
@@ -764,50 +764,51 @@ void congruence_closure::internalize_core(expr const & e, bool toplevel, bool to
     if (has_expr_metavar(e) && !m_state.m_froze_partitions)
         return;
     /* Check whether 'e' has already been internalized. */
-    if (get_entry(e))
-        return;
-
-    switch (e.kind()) {
-    case expr_kind::Var:
-        lean_unreachable();
-    case expr_kind::Sort:
-        break;
-    case expr_kind::Constant:
-    case expr_kind::Local:
-    case expr_kind::Meta:
-        mk_entry_core(e, to_propagate);
-        break;;
-    case expr_kind::Lambda:
-    case expr_kind::Let:
-        mk_entry_core(e, false);
-        break;
-    case expr_kind::Macro:
-        if (is_interpreted_value(e)) {
-            bool interpreted = true;
-            mk_entry_core(e, false, interpreted);
-        } else {
-            for (unsigned i = 0; i < macro_num_args(e); i++)
-                internalize_core(macro_arg(e, i), false, false, some_expr(e));
+    if (!get_entry(e)) {
+        switch (e.kind()) {
+        case expr_kind::Var:
+            lean_unreachable();
+        case expr_kind::Sort:
+            break;
+        case expr_kind::Constant:
+        case expr_kind::Local:
+        case expr_kind::Meta:
             mk_entry_core(e, to_propagate);
-            if (is_annotation(e))
-                push_refl_eq(e, get_annotation_arg(e));
-        }
-        break;
-    case expr_kind::Pi:
-        if (is_arrow(e) && m_ctx.is_prop(binding_domain(e)) && m_ctx.is_prop(binding_body(e))) {
-            to_propagate = toplevel; /*  We must propagate children if arrow is top-level */
-            internalize_core(binding_domain(e), toplevel, to_propagate, some_expr(e));
-            internalize_core(binding_body(e), toplevel, to_propagate, some_expr(e));
-        }
-        if (m_ctx.is_prop(e)) {
+            break;;
+        case expr_kind::Lambda:
+        case expr_kind::Let:
             mk_entry_core(e, false);
-        }
-        break;
-    case expr_kind::App: {
-        internalize_app(e, toplevel, to_propagate);
-        break;
-    }}
+            break;
+        case expr_kind::Macro:
+            if (is_interpreted_value(e)) {
+                bool interpreted = true;
+                mk_entry_core(e, false, interpreted);
+            } else {
+                for (unsigned i = 0; i < macro_num_args(e); i++)
+                    internalize_core(macro_arg(e, i), false, false, some_expr(e));
+                mk_entry_core(e, to_propagate);
+                if (is_annotation(e))
+                    push_refl_eq(e, get_annotation_arg(e));
+            }
+            break;
+        case expr_kind::Pi:
+            if (is_arrow(e) && m_ctx.is_prop(binding_domain(e)) && m_ctx.is_prop(binding_body(e))) {
+                to_propagate = toplevel; /*  We must propagate children if arrow is top-level */
+                internalize_core(binding_domain(e), toplevel, to_propagate, some_expr(e));
+                internalize_core(binding_body(e), toplevel, to_propagate, some_expr(e));
+            }
+            if (m_ctx.is_prop(e)) {
+                mk_entry_core(e, false);
+            }
+            break;
+        case expr_kind::App: {
+            internalize_app(e, toplevel, to_propagate);
+            break;
+        }}
+    }
 
+    /* Remark: if should invoke m_ac.internalize even if the test !get_entry(e) above failed.
+       Reason, the first time e was visited, it may have been visited with a different parent. */
     if (m_state.m_config.m_ac)
         m_ac.internalize(e, parent);
 }
diff --git a/tests/lean/run/cc_ac_bug.lean b/tests/lean/run/cc_ac_bug.lean
new file mode 100644
index 0000000000..386f8fb533
--- /dev/null
+++ b/tests/lean/run/cc_ac_bug.lean
@@ -0,0 +1,2 @@
+example (a b c : nat) (f : nat → nat → nat) : f (b * c) (c * b * a) = f (c * b) (a * c * b) :=
+by ac_refl