From 89c3079072e93b1a212304e4eaf691d853b4ef5d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 12 Aug 2024 02:47:08 +0200 Subject: [PATCH] chore: fix typo in hash code for `Expr` equality test (#4990) We observed a small performance improvement at https://github.com/leanprover/LNSym/blob/proof_size_expt/Proofs/SHA512/Experiments/Sym30.lean Before: 2.65s After: 2.60s --- src/kernel/expr_eq_fn.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp index 7078565217..c0b0d55a7d 100644 --- a/src/kernel/expr_eq_fn.cpp +++ b/src/kernel/expr_eq_fn.cpp @@ -23,7 +23,7 @@ template class expr_eq_fn { struct key_hasher { std::size_t operator()(std::pair const & p) const { - return hash((size_t)p.first >> 3, (size_t)p.first >> 3); + return hash((size_t)p.first >> 3, (size_t)p.second >> 3); } }; typedef std::unordered_set, key_hasher> cache;