From a61693c1290cef134229d00224d94cbdbb6ea5f9 Mon Sep 17 00:00:00 2001 From: Can Cebeci Date: Thu, 18 Jun 2026 15:55:32 -0700 Subject: [PATCH] Prevent special treatment of non-recursive siblings --- src/model/datatype_factory.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/model/datatype_factory.cpp b/src/model/datatype_factory.cpp index b93703acd..66e46d7a2 100644 --- a/src/model/datatype_factory.cpp +++ b/src/model/datatype_factory.cpp @@ -105,7 +105,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) { continue; } } - if (!found_fresh_arg && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) { + if (!found_fresh_arg && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg) && m_util.is_recursive(s_arg)) { recursive = true; expr * last_fresh = get_last_fresh_value(s_arg); args.push_back(last_fresh);