From 76182c7e663d68e8a29eda36442cded9c5eabec1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Jan 2026 14:39:19 -0800 Subject: [PATCH] fix #8195 Signed-off-by: Nikolaj Bjorner --- src/ast/datatype_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index bb5e0781e..48dfc1fbe 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -1296,7 +1296,7 @@ namespace datatype { unsigned start = rand(); for (unsigned cj = 0; cj < constructors.size(); ++cj) { func_decl* c = constructors[(start + cj) % constructors.size()]; - if (all_of(*c, [&](sort* s) { return !is_datatype(s); })) { + if (all_of(*c, [&](sort* s) { return !is_datatype(s) && !is_recursive_nested(s); })) { TRACE(util_bug, tout << "non_rec_constructor c: " << func_decl_ref(c, m) << "\n";); result.first = c; result.second = 1;