mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-20 15:40:37 +00:00
Code Activity

Prevent special treatment of non-recursive siblings (#9903)

Browse source 
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 <t-cancebeci@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Can Cebeci 2026-06-19 09:08:30 -07:00 • committed by GitHub
parent 76cceddb73
commit ff87fb227e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/model/datatype_factory.cpp
View file

@ -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);