fix #7448

Z3Prover · Nov 10, 2024 · 1856ab7 · 1856ab7
1 parent 4f060dd
commit 1856ab7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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);