From e49e5d7145be73369a4a91a15548ed82ccc0cd2e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 May 2019 06:55:06 +0400 Subject: [PATCH] fix #2297 Signed-off-by: Nikolaj Bjorner --- src/ast/datatype_decl_plugin.cpp | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 9f048ff1b..6ce31755a 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -709,20 +709,22 @@ namespace datatype { if (is_datatype(s)) { param_size::size* sz; obj_map S; + sref_vector refs; unsigned n = get_datatype_num_parameter_sorts(s); def & d = get_def(s->get_name()); SASSERT(n == d.params().size()); for (unsigned i = 0; i < n; ++i) { sort* ps = get_datatype_parameter_sort(s, i); sz = get_sort_size(params, ps); - sz->inc_ref(); + refs.push_back(sz); S.insert(d.params().get(i), sz); } - sz = d.sort_size()->subst(S); - for (auto & kv : S) { - kv.m_value->dec_ref(); + auto ss = d.sort_size(); + if (!ss) { + d.set_sort_size(param_size::size::mk_offset(sort_size::mk_infinite())); + ss = d.sort_size(); } - return sz; + return ss->subst(S); } array_util autil(m); if (autil.is_array(s)) {