diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index bd0679c85..10e7bc367 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -819,7 +819,8 @@ namespace datatype { for (constructor const* c : d) { ptr_vector s_mul; for (accessor const* a : *c) { - s_mul.push_back(get_sort_size(d.params(), a->range())); + auto* sz = get_sort_size(d.params(), a->range()); + if (sz) s_mul.push_back(sz); } s_add.push_back(param_size::size::mk_times(s_mul)); }