From 747497b9699963073319ec7f9551cb0113e66870 Mon Sep 17 00:00:00 2001 From: Can Cebeci Date: Fri, 19 Jun 2026 09:08:30 -0700 Subject: [PATCH] Prevent special treatment of non-recursive siblings (#9903) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addressing the following: ``` `https://zenodo.org/records/16740866/files/UFDT.tar.zst?download=1` — ERRORS `4` (signal-11:4) - Error queries: `non-incremental/UFDT/20170428-Barrett/cdt-cade2015/data/distro/process/x2015_09_10_16_46_28_479_1049550.smt_in.smt2`, `non-incremental/UFDT/20170428-Barrett/cdt-cade2015/data/distro/process/x2015_09_10_16_46_29_792_1051661.smt_in.smt2`, `non-incremental/UFDT/20170428-Barrett/cdt-cade2015/data/distro/process/x2015_09_10_16_46_24_262_1043633.smt_in.smt2`, `non-incremental/UFDT/20170428-Barrett/cdt-cade2015/data/distro/process/x2015_09_10_16_46_25_595_1045744.smt_in.smt2` ``` These segfault due to infinite recursion in `datatype_factory::get_fresh_value` (through the call in line 222). Splitting ``` (declare-datatypes ((Nibble$ 0)(Char$ 0)(Char_list$ 0)) (((nibble0$) (nibble1$) (nibble2$) (nibble3$) (nibble4$) (nibble5$) (nibble6$) (nibble7$) (nibble8$) (nibble9$) (nibbleA$) (nibbleB$) (nibbleC$) (nibbleD$) (nibbleE$) (nibbleF$)) ((char$ (selectf$ Nibble$) (selectg$ Nibble$))) ((nil$) (cons$ (hd$ Char$) (tl$ Char_list$))) )) ``` into ``` (declare-datatypes ((Nibble$ 0)(Char$ 0)) (((nibble0$) (nibble1$) (nibble2$) (nibble3$) (nibble4$) (nibble5$) (nibble6$) (nibble7$) (nibble8$) (nibble9$) (nibbleA$) (nibbleB$) (nibbleC$) (nibbleD$) (nibbleE$) (nibbleF$)) ((char$ (selectf$ Nibble$) (selectg$ Nibble$))) )) (declare-datatypes ((Char_list$ 0)) ( ((nil$) (cons$ (hd$ Char$) (tl$ Char_list$))) )) ``` turns them into timeouts --------- Co-authored-by: Can Cebeci Co-authored-by: Nikolaj Bjorner --- src/model/datatype_factory.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/model/datatype_factory.cpp b/src/model/datatype_factory.cpp index b93703acd..4837bdb90 100644 --- a/src/model/datatype_factory.cpp +++ b/src/model/datatype_factory.cpp @@ -97,7 +97,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) { unsigned num = constructor->get_arity(); for (unsigned i = 0; i < num; ++i) { sort * s_arg = constructor->get_domain(i); - 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))) { expr * new_arg = m_model.get_fresh_value(s_arg); if (new_arg != nullptr) { found_fresh_arg = true; @@ -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);