mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-10 02:50:55 +00:00
Code Activity

Add parameter validation to prevent datatype parameter mismatch segfault

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-01 22:16:32 +00:00
parent d3c3e42d5a
commit 087e475722
1 changed files with 9 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/datatype_decl_plugin.cpp
View file

@ -321,10 +321,14 @@ namespace datatype {
throw invalid_datatype();
}
}
def* d = nullptr;
if (m_defs.find(name.get_symbol(), d) && d->params().size() != num_parameters - 1) {
throw default_exception("datatype has already been registered but with a different number of parameters");
}
sort* s = m_manager->mk_sort(name.get_symbol(),
sort_info(m_family_id, k, num_parameters, parameters, true));
def* d = nullptr;
if (m_defs.find(s->get_name(), d) && d->sort_size() && d->params().size() == num_parameters - 1) {
obj_map<sort, sort_size> S;
for (unsigned i = 0; i + 1 < num_parameters; ++i) {
@ -345,6 +349,10 @@ namespace datatype {
m_manager->raise_exception("invalid datatype");
return nullptr;
}
catch (const default_exception & ex) {
m_manager->raise_exception(ex.what());
return nullptr;
}
}
func_decl * plugin::mk_update_field(