From 087e475722f81b693ec778576a6199402afc2a56 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 1 Feb 2026 22:16:32 +0000 Subject: [PATCH] Add parameter validation to prevent datatype parameter mismatch segfault Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/datatype_decl_plugin.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index d875262b3..8a4a0957c 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -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 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(