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

Merge a61693c129 into d9385e9713

Browse source
This commit is contained in:
Can Cebeci 2026-06-18 16:09:08 -07:00 • committed by GitHub
commit 4196bca61d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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);