diff --git a/src/model/datatype_factory.cpp b/src/model/datatype_factory.cpp
index b93703acd..4837bdb90 100644
--- a/src/model/datatype_factory.cpp
+++ b/src/model/datatype_factory.cpp
@@ -97,7 +97,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
         unsigned num            = constructor->get_arity();
         for (unsigned i = 0; i < num; ++i) {
             sort * s_arg        = constructor->get_domain(i);
-            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))) {
                 expr * new_arg = m_model.get_fresh_value(s_arg);
                 if (new_arg != nullptr) {
                     found_fresh_arg = true;
@@ -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);