From 6af7e7f7947ba6c3c2790cb3b2cfb9b607e227bd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Jul 2014 18:56:50 +0100 Subject: [PATCH] fix(kernel/expr_eq_fn): take local pp name into account when annotations are considered in the equality test Signed-off-by: Leonardo de Moura --- src/kernel/expr_eq_fn.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp index b06ec57a0..369f8e427 100644 --- a/src/kernel/expr_eq_fn.cpp +++ b/src/kernel/expr_eq_fn.cpp @@ -40,6 +40,7 @@ bool expr_eq_fn::apply(expr const & a, expr const & b) { return mlocal_name(a) == mlocal_name(b) && apply(mlocal_type(a), mlocal_type(b)) && + (!m_compare_binder_info || local_pp_name(a) == local_pp_name(b)); (!m_compare_binder_info || local_info(a) == local_info(b)); case expr_kind::App: m_counter++;