From 1856ab72d9fd4b3e675ea449d7ccdea1ba2267b8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Nov 2024 14:40:28 -0800 Subject: [PATCH] fix #7448 --- src/model/datatype_factory.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/model/datatype_factory.cpp b/src/model/datatype_factory.cpp index c01b385d799..480db2a8140 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);