mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix #7448
This commit is contained in:
parent
4f060dd2b1
commit
1856ab72d9
|
@ -217,7 +217,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
|
|||
expr * maybe_new_arg = nullptr;
|
||||
if (!m_util.is_datatype(s_arg))
|
||||
maybe_new_arg = m_model.get_fresh_value(s_arg);
|
||||
else if (num_iterations <= 1 || m_util.is_recursive(s_arg))
|
||||
else if (num_iterations <= 10 && (num_iterations <= 1 || m_util.is_recursive(s_arg)))
|
||||
maybe_new_arg = get_almost_fresh_value(s_arg);
|
||||
else
|
||||
maybe_new_arg = get_fresh_value(s_arg);
|
||||
|
|
Loading…
Reference in a new issue