diff --git a/src/model/array_factory.cpp b/src/model/array_factory.cpp
index da3278b43..6fab80661 100644
--- a/src/model/array_factory.cpp
+++ b/src/model/array_factory.cpp
@@ -134,8 +134,9 @@ expr * array_factory::get_fresh_value(sort * s) {
     sort * range    = get_array_range(s);
     expr* range_val = nullptr;
     
-    if (!m_recursive_fresh) {
-        flet<bool> _recursive(m_recursive_fresh, true);
+    if (!m_ranges.contains(range)) {
+        ptr_vector<sort>::scoped_stack _s(m_ranges);
+        m_ranges.push_back(range);
         range_val = m_model.get_fresh_value(range);
         if (range_val != nullptr) {
             // easy case
diff --git a/src/model/array_factory.h b/src/model/array_factory.h
index a2ec07f88..c4bfc05df 100644
--- a/src/model/array_factory.h
+++ b/src/model/array_factory.h
@@ -28,7 +28,7 @@ class array_factory : public struct_factory {
     expr * mk_array_interp(sort * s, func_interp * & fi);
     void get_some_args_for(sort * s, ptr_buffer<expr> & args);
     bool mk_two_diff_values_for(sort * s);
-    bool m_recursive_fresh { false };
+    ptr_vector<sort> m_ranges;
 public:
     array_factory(ast_manager & m, model_core & md);