diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 64f080708..0d7d52eb2 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -334,7 +334,7 @@ namespace datatype { m_manager->raise_exception("invalid datatype instantiation: parameter count mismatch"); return nullptr; } - if (d->sort_size() && d->params().size() == num_parameters - 1) { + if (d->sort_size()) { obj_map S; for (unsigned i = 0; i + 1 < num_parameters; ++i) { sort* r = to_sort(parameters[i + 1].get_ast());