diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index e5b9ee61b..3a3a96bce 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -139,9 +139,7 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param m_manager->raise_exception("set.empty requires one sort parameter"); return nullptr; } - sort* element_sort = to_sort(parameters[0].get_ast()); - parameter param(element_sort); - range = m_manager->mk_sort(m_family_id, FINITE_SET_SORT, 1, ¶m); + range = to_sort(parameters[0].get_ast()); } return mk_empty(range); case OP_FINITE_SET_SINGLETON: