From 7d25158254d74952b374dbbb7403107562cd45da Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 23 Jul 2014 18:33:15 -0700 Subject: [PATCH] fix(kernel/replace_fn): bug in the cache Signed-off-by: Leonardo de Moura --- src/kernel/replace_fn.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp index 2252f199ff..314349f9df 100644 --- a/src/kernel/replace_fn.cpp +++ b/src/kernel/replace_fn.cpp @@ -27,7 +27,7 @@ struct replace_cache { expr * find(expr const & e, unsigned offset) { unsigned i = hash(e.hash_alloc(), offset) % m_capacity; - if (m_cache[i].m_cell == e.raw()) + if (m_cache[i].m_cell == e.raw() && m_cache[i].m_offset == offset) return &m_cache[i].m_result; else return nullptr;