mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00
Code Activity

Prevent special treatment of non-recursive siblings

Browse source
This commit is contained in:
Can Cebeci 2026-06-18 15:55:32 -07:00
parent d9385e9713
commit a61693c129
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/model/datatype_factory.cpp
View file

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