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

fix(library/unifier): assertion violation

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-26 09:07:34 -07:00
parent 44c597724b
commit 4c9723e5ed
1 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/library/unifier.cpp
View file

@ -1735,10 +1735,15 @@ struct unifier_fn {
if (!all_local(lhs)) { if (!all_local(lhs)) {
expr rhs_whnf = whnf(rhs, j, relax, aux); expr rhs_whnf = whnf(rhs, j, relax, aux);
if (rhs_whnf != rhs) { if (rhs_whnf != rhs) {
buffer<constraints> alts2; if (is_meta(rhs_whnf)) {
process_flex_rigid_core(lhs, rhs_whnf, j, relax, alts2); // it become a flex-flex constraint
append_auxiliary_constraints(alts2, to_list(aux.begin(), aux.end())); alts.push_back(constraints(mk_eq_cnstr(lhs, rhs_whnf, j, relax)));
alts.append(alts2); } else {
buffer<constraints> alts2;
process_flex_rigid_core(lhs, rhs_whnf, j, relax, alts2);
append_auxiliary_constraints(alts2, to_list(aux.begin(), aux.end()));
alts.append(alts2);
}
} }
} }