mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-01-11 10:13:14 -08:00
parent 434eb25004 1a4636518c
commit f8f3549c1c
1 changed files with 5 additions and 4 deletions

9
src/ast/datatype_decl_plugin.cpp
View file

@ -654,13 +654,14 @@ namespace datatype {
param_size::size* sz;
obj_map<sort, param_size::size*> S;
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();
S.insert(ps, sz);
}
def & d = get_def(s->get_name());
sz->inc_ref();
S.insert(d.params().get(i), sz);
}
sz = d.sort_size()->subst(S);
for (auto & kv : S) {
kv.m_value->dec_ref();