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

fix(library/compiler/llnf): bug at to_llnf when boxing is enabled

Browse source
This commit is contained in:
Leonardo de Moura 2019-01-30 16:48:04 -08:00
parent d63bbb3728
commit 909a8d7c6d
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/compiler/llnf.cpp
View file

@ -794,7 +794,7 @@ class to_llnf_fn {
if (first && obj_args.size() > 0) {
r = mk_let_decl(mk_enf_object_type(), r);
}
r = mk_let_decl(info.get_type(), mk_sset(r, info.m_size, (k_info.m_num_objs + k_info.m_num_usizes), offset, args[j]));
r = mk_let_decl(mk_enf_object_type(), mk_sset(r, info.m_size, (k_info.m_num_objs + k_info.m_num_usizes), offset, args[j]));
offset += info.m_size;
first = false;
break;
@ -802,7 +802,7 @@ class to_llnf_fn {
if (first && obj_args.size() > 0) {
r = mk_let_decl(mk_enf_object_type(), r);
}
r = mk_let_decl(info.get_type(), mk_uset(r, k_info.m_num_objs + uidx, args[j]));
r = mk_let_decl(mk_enf_object_type(), mk_uset(r, k_info.m_num_objs + uidx, args[j]));
uidx++;
first = false;
break;