Fix segfault on datatype parameter count mismatch

[Copilot]

Z3 segfaults when instantiating a non-parametric datatype with type parameters, e.g., declaring a datatype with mk_datatypes(0 params) then calling mk_datatype_sort(name, 1, params).

Changes

src/ast/datatype_decl_plugin.cpp:

• get_sort_size() (L844-855): Added null-check before SASSERT to return nullptr on parameter count mismatch instead of undefined behavior
• mk_sort() (L327-338): Added early validation to raise clear error message before creating invalid sorts

src/test/parametric_datatype.cpp:

• Added regression test test_parameter_mismatch_error() that exercises the error path

Example

// Before: Segmentation fault
Z3_sort non_parametric = Z3_mk_datatype(ctx, name, 0, nullptr, ...);
Z3_sort params[] = {Z3_mk_int_sort(ctx)};
Z3_sort s = Z3_mk_datatype_sort(ctx, name, 1, params);  // SEGFAULT

// After: Clear error
// Error: invalid datatype instantiation: parameter count mismatch

The fix validates parameter counts match the datatype definition at both the internal (get_sort_size) and API (mk_sort) levels, preventing the crash while providing actionable diagnostics.

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Z3 segfaults instead of erroring out when passing the wrong type parameters to Z3.Datatype.mk_sort_ref_p</issue_title>
<issue_description>I'm going to be using ML syntax here, but not sure if this is an issue specific to the ml API. If you declare your types using Z3.Datatype.mk_datatypes (so no type parameters), but reference them using type parameters, Z3 segfaults instead of erroring out. This is the stack trace:

Datatype::util::get_sort_size(ref_vector<sort, ast_manager> const&, sort*) () from 4.15.4/install/lib/libz3.so           
Datatype::util::compute_datatype_size_functions(svector<symbol, unsigned int> const&) () from 4.15.4/install/lib/libz3.so
Datatype::decl::plugin::end_def_block() () from 4.15.4/install/lib/libz3.so                                              
Datatype::decl::plugin::mk_datatypes(unsigned int, datatype::def* const*, unsigned int, sort* const*, ref_vector<sort, ast_manager>&) ()                          

Happy to give more data if needed!</issue_description>

Comments on the Issue (you are @copilot in this section)

Custom agent used: agentic-workflows
GitHub Agentic Workflows (gh-aw) - Create, debug, and upgrade AI-powered workflows with intelligent prompt routing

• Fixes Z3 segfaults instead of erroring out when passing the wrong type parameters to Z3.Datatype.mk_sort_ref_p #8376

---

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.