From 3669dc37b3e5d9dd1b68eca88fbbabe26af0f4cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 10 Dec 2025 00:26:21 -0800 Subject: [PATCH] don't unfold recursive defs if there is an uninterpreted subterm, #7671 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/recfun_rewriter.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/rewriter/recfun_rewriter.cpp b/src/ast/rewriter/recfun_rewriter.cpp index af4e75d7e..c14c6152a 100644 --- a/src/ast/rewriter/recfun_rewriter.cpp +++ b/src/ast/rewriter/recfun_rewriter.cpp @@ -34,6 +34,9 @@ br_status recfun_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * for (unsigned i = 0; i < num_args; ++i) if (!m.is_value(args[i])) safe_to_subst = false; + for (auto t : subterms::all(expr_ref(r, m))) + if (is_uninterp(t)) + return BR_FAILED; // check if there is an argument that is a constructor // such that the recursive function can be partially evaluated.