max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/compiler/csimp): bug at join point preservation code

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-27 17:48:02 -07:00
parent c746783c0d
commit 6786b2bcc8
1 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/library/compiler/csimp.cpp
View file

@ -471,6 +471,21 @@ class csimp_fn {
e_y = *e_y_opt;
}
expr new_jp_val = e_y;
/* Some of the new join points in `new_jps` may be replacing join points defined at jp_decl.
So, we must insert them after the old one, and remove them from `new_jps` and `new_jp_cache`. */
unsigned i = saved_fvars_size;
while (i < m_fvars.size()) {
expr curr = m_fvars[i];
auto it = new_jp_cache.find(curr);
if (it != new_jp_cache.end()) {
m_fvars.insert(i+i, it->second);
new_jp_cache.erase(curr);
new_jps.erase_elem(curr);
i = i + 2;
} else {
i = i + 1;
}
}
new_jp_val = mk_let(saved_fvars_size, new_jp_val);
new_jp_val = m_lctx.mk_lambda(zs, new_jp_val);
mark_simplified(new_jp_val);