From 203afaab07f40849ec58aeeb9a4961150a513e8d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Jan 2026 20:22:41 -0800
Subject: [PATCH] address #8376

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/datatype_decl_plugin.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index a8db335b2..d875262b3 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -845,6 +845,8 @@ namespace datatype {
             if (!is_declared(s))
                 return nullptr;
             def & d = get_def(s->get_name());
+            if (n != d.params().size()) 
+                throw default_exception("datatype " + s->get_name().str() + " has " + std::to_string(n) + " parameters, but " + std::to_string(d.params().size()) + " were expected");
             SASSERT(n == d.params().size());
             for (unsigned i = 0; i < n; ++i) {
                 sort* ps = get_datatype_parameter_sort(s, i);