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

fix(library/max_sharing): conflict with the kernel approximate caching

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-06 13:57:36 -07:00
parent 02662fe489
commit 2ca16a099b
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/max_sharing.cpp
View file

@ -52,7 +52,11 @@ struct max_sharing_fn::imp {
return res;
}
expr operator()(expr const & a) { return apply(a); }
expr operator()(expr const & a) {
// we must disable approximate/opportunistic hash-consing used in the kernel
scoped_expr_caching disable(false);
return apply(a);
}
bool already_processed(expr const & a) const {
auto r = m_cache.find(a);