diff --git a/src/model/datatype_factory.cpp b/src/model/datatype_factory.cpp index c01b385d7..480db2a81 100644 --- a/src/model/datatype_factory.cpp +++ b/src/model/datatype_factory.cpp @@ -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);