From 909a8d7c6d238c5167d95df52f81d2896d7f326e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Jan 2019 16:48:04 -0800 Subject: [PATCH] fix(library/compiler/llnf): bug at to_llnf when boxing is enabled --- src/library/compiler/llnf.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp index 38be771811..dce7be3636 100644 --- a/src/library/compiler/llnf.cpp +++ b/src/library/compiler/llnf.cpp @@ -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;