From cd94f8541fbc6c5e6258a24de527f8c7ae5b8ca4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Apr 2026 13:54:09 -0700 Subject: [PATCH] fix #9234 Signed-off-by: Nikolaj Bjorner --- src/ast/recfun_decl_plugin.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 9da36b27a..1195a86da 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -437,7 +437,8 @@ namespace recfun { promise_def plugin::mk_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated) { def* d = u().decl_fun(name, n, params, range, is_generated); - SASSERT(!m_defs.contains(d->get_decl())); + if (m_defs.contains(d->get_decl())) + throw default_exception(std::string("recursive function ") + name.str() + " already defined"); m_defs.insert(d->get_decl(), d); return promise_def(&u(), d); }