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

fix(library/unifier): memory violation, and missing set_conflict

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-22 14:09:06 -07:00
parent 25cb1bf6a1
commit 238a0dbfba
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/unifier.cpp
View file

@ -221,7 +221,7 @@ struct unifier_fn {
cnstr_idx_set s; cnstr_idx_set s;
name_to_cnstrs & map = MVar ? m_mvar_occs : m_mlvl_occs; name_to_cnstrs & map = MVar ? m_mvar_occs : m_mlvl_occs;
auto it = map.find(m); auto it = map.find(m);
if (!it) if (it)
s = *it; s = *it;
if (!s.contains(cidx)) { if (!s.contains(cidx)) {
s.insert(cidx); s.insert(cidx);
@ -472,8 +472,10 @@ struct unifier_fn {
lean_assert(!is_choice_cnstr(c)); lean_assert(!is_choice_cnstr(c));
lazy_list<constraints> alts = m_plugin(c, m_ngen.mk_child()); lazy_list<constraints> alts = m_plugin(c, m_ngen.mk_child());
auto r = alts.pull(); auto r = alts.pull();
if (!r) if (!r) {
set_conflict(c.get_justification());
return false; return false;
}
// TODO(Leo): create backtracking point // TODO(Leo): create backtracking point
return true; return true;
} }