mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-05 05:49:13 +00:00
Code Activity

Simplify range assignment in finite_set_decl_plugin

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-10-14 17:15:14 +02:00 • committed by GitHub
parent 6ea8599e0c
commit 52343035f3
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/finite_set_decl_plugin.cpp
View file

@ -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"); m_manager->raise_exception("set.empty requires one sort parameter");
return nullptr; return nullptr;
} }
sort* element_sort = to_sort(parameters[0].get_ast()); range = to_sort(parameters[0].get_ast());
parameter param(element_sort);
range = m_manager->mk_sort(m_family_id, FINITE_SET_SORT, 1, &param);
} }
return mk_empty(range); return mk_empty(range);
case OP_FINITE_SET_SINGLETON: case OP_FINITE_SET_SINGLETON: