michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(kernel/replace_fn): bug in the cache

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-23 18:33:15 -07:00
parent 61df118339
commit 7d25158254
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/replace_fn.cpp
View file

@ -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;