diff --git a/src/model/datatype_factory.cpp b/src/model/datatype_factory.cpp
index b93703acd..fac858ccc 100644
--- a/src/model/datatype_factory.cpp
+++ b/src/model/datatype_factory.cpp
@@ -139,6 +139,9 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
 expr * datatype_factory::get_fresh_value(sort * s) {
     if (!m_util.is_datatype(s))
         return m_model.get_fresh_value(s);
+    if (m_fresh_depth >= m_max_fresh_depth)
+        return get_last_fresh_value(s);
+    struct depth_guard { unsigned& d; depth_guard(unsigned& d) : d(d) { ++d; } ~depth_guard() { --d; } } _dg(m_fresh_depth);
     TRACE(datatype, tout << "generating fresh value for: " << s->get_name() << "\n";);
     auto& [set, values] = get_value_set(s);
     // Approach 0) 
diff --git a/src/model/datatype_factory.h b/src/model/datatype_factory.h
index b2a6b75d3..2d8f216b4 100644
--- a/src/model/datatype_factory.h
+++ b/src/model/datatype_factory.h
@@ -24,6 +24,8 @@ Revision History:
 class datatype_factory : public struct_factory {
     datatype_util         m_util;
     obj_map<sort, expr *> m_last_fresh_value;
+    unsigned              m_fresh_depth = 0;
+    static const unsigned m_max_fresh_depth = 512;
     
     expr * get_last_fresh_value(sort * s);
     expr * get_almost_fresh_value(sort * s);