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

fix(library/blast/congruence_closure): cannot assume all subterms have been internalized

Browse source
This commit is contained in:
Daniel Selsam 2016-01-16 11:54:06 -08:00 committed by Leonardo de Moura
parent 19bfbe2df8
commit b2554dcb8f
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/blast/congruence_closure.cpp
View file

@ -1881,7 +1881,9 @@ expr congruence_closure::get_next(name const & R, expr const & e) const {
}
bool congruence_closure::eq_class_heterogeneous(expr const & e) const {
return has_heq_proofs(get_root(get_eq_name(), e));
expr root = get_root(get_eq_name(), e);
if (auto e = m_entries.find(eqc_key(get_eq_name(), root))) return e->m_heq_proofs;
else return false;
}
unsigned congruence_closure::get_mt(name const & R, expr const & e) const {