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

fix(library/unifier): bug introduced today in consume_tc_cnstrs

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-27 17:16:30 -07:00
parent bc0a8b8da4
commit d1fe1286c0
1 changed files with 11 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/unifier.cpp
View file

@ -1382,18 +1382,18 @@ struct unifier_fn {
} }
void consume_tc_cnstrs() { void consume_tc_cnstrs() {
for (unsigned i = 0; i < 2; i++) {
while (true) { while (true) {
if (in_conflict()) if (in_conflict()) {
return; return;
if (auto c = m_tc[i]->next_cnstr()) { } else if (auto c = m_tc[0]->next_cnstr()) {
process_constraint(*c);
} else if (auto c = m_tc[1]->next_cnstr()) {
process_constraint(*c); process_constraint(*c);
} else { } else {
break; break;
} }
} }
} }
}
/** /**
\brief Process the following constraints \brief Process the following constraints
@ -1431,6 +1431,8 @@ struct unifier_fn {
/** \brief Process the next constraint in the constraint queue m_cnstrs */ /** \brief Process the next constraint in the constraint queue m_cnstrs */
bool process_next() { bool process_next() {
lean_assert(!m_cnstrs.empty()); lean_assert(!m_cnstrs.empty());
lean_assert(!m_tc[0]->next_cnstr());
lean_assert(!m_tc[1]->next_cnstr());
constraint c = m_cnstrs.min()->first; constraint c = m_cnstrs.min()->first;
m_cnstrs.erase_min(); m_cnstrs.erase_min();
if (is_choice_cnstr(c)) { if (is_choice_cnstr(c)) {