diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 8f408d5cf..a36234cb2 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -34,7 +34,7 @@ namespace smt {
     }
 
     std::ostream& operator<<(std::ostream& out, model_value_dependency const& src) {
-        if (src.is_fresh_value()) return out << "fresh!" << src.get_value()->get_idx();
+        if (src.is_fresh_value()) return out << "fresh!" << src.get_value()->get_idx() << "#" << src.get_value()->get_src()->get_id();
         else return out << "#" << src.get_enode()->get_owner_id();
     }
 
@@ -115,8 +115,11 @@ namespace smt {
                             SASSERT(proc);
                         }
                         else {
-                            TRACE("model", tout << "creating fresh value for #" << mk_pp(r->get_expr(), m) << "\n";);
-                            proc = alloc(fresh_value_proc, mk_extra_fresh_value(r->get_sort()));
+                            TRACE("model", tout << "creating fresh value for #" 
+                                << r->get_expr_id() << " " 
+                                << mk_bounded_pp(r->get_expr(), m) << " " 
+                                << mk_pp(r->get_sort(), m) << "\n";);
+                            proc = alloc(fresh_value_proc, mk_extra_fresh_value(r->get_expr(), r->get_sort()));
                         }
                     }
                     else {
@@ -181,6 +184,11 @@ namespace smt {
             if (already_traversed.contains(s))
                 return true;
             bool visited = true;
+            TRACE("mg_top_sort", tout << "fresh value of sort " << mk_pp(s, m) << "\n";
+            for (enode* r : roots)
+                if (r->get_sort() == s)
+                    tout << mk_pp(r->get_expr(), m) << "\n";
+                );
             for (enode * r : roots) {
                 if (r->get_sort() != s)
                     continue;
@@ -305,14 +313,21 @@ namespace smt {
                   }
                   else {
                       enode * n = curr.get_enode();
+                      sort* s = n->get_sort();
                       SASSERT(n->get_root() == n);
-                      tout << mk_pp(n->get_expr(), m) << "\n";
-                      sort * s = n->get_sort();
                       tout << curr << " " << mk_pp(s, m);
-                      tout << " is_fresh: " << root2proc[n]->is_fresh() << "\n";
+                      tout << mk_bounded_pp(n->get_expr(), m) << " ";
+                      tout << " is_fresh: " << root2proc[n]->is_fresh() << " - deps: ";
+                      dependencies.reset();
+                      model_value_proc* proc = root2proc[n];
+                      SASSERT(proc);
+                      proc->get_dependencies(dependencies);
+                      for (auto const& d : dependencies)
+                          tout << d << " ";
+                      tout << "\n";
                   }
               }
-              m_context->display(tout);
+              // m_context->display(tout);
               );
 
 
@@ -340,10 +355,16 @@ namespace smt {
                     proc->get_dependencies(dependencies);
                     for (model_value_dependency const& d : dependencies) {
                         if (d.is_fresh_value()) {
-                            CTRACE("mg_top_sort", !d.get_value()->get_value(), 
-                                   tout << "#" << n->get_owner_id() << " " << mk_pp(n->get_expr(), m) << " -> " << d << "\n";);
-                            SASSERT(d.get_value()->get_value());
-                            dependency_values.push_back(d.get_value()->get_value());
+                            expr* val = d.get_value()->get_value();
+                            CTRACE("mg_top_sort", !val,
+                                tout << "#" << n->get_owner_id() << " " <<
+                                mk_pp(n->get_expr(), m) << " -> " << d << "\n";);
+                            // there is a cyclic dependency for default(A), where A
+                            // is an array of a datatype with the datatype using A.
+                            if (!val)
+                                val = m_model->get_some_value(d.get_value()->get_sort());
+                            SASSERT(val);
+                            dependency_values.push_back(val);
                         }
                         else {
                             enode * child = d.get_enode();
@@ -446,8 +467,8 @@ namespace smt {
         }
     }
 
-    extra_fresh_value * model_generator::mk_extra_fresh_value(sort * s) {        
-        extra_fresh_value * r = alloc(extra_fresh_value, s, m_fresh_idx);
+    extra_fresh_value * model_generator::mk_extra_fresh_value(expr * src, sort* s) {        
+        extra_fresh_value * r = alloc(extra_fresh_value, src, s, m_fresh_idx);
         m_fresh_idx++;
         m_extra_fresh_values.push_back(r);
         return r;
diff --git a/src/smt/smt_model_generator.h b/src/smt/smt_model_generator.h
index 632557e98..fd99dc6d8 100644
--- a/src/smt/smt_model_generator.h
+++ b/src/smt/smt_model_generator.h
@@ -76,12 +76,14 @@ namespace smt {
        \brief Stub for extra fresh value.
     */
     struct extra_fresh_value {
+        expr*    m_src;
         sort *   m_sort;
         unsigned m_idx;
-        expr *   m_value;
+        expr *   m_value = nullptr;
     public:
-        extra_fresh_value(sort * s, unsigned idx):m_sort(s), m_idx(idx), m_value(nullptr) {}
+        extra_fresh_value(expr * src, sort* s, unsigned idx):m_src(src), m_sort(s), m_idx(idx) {}
         sort * get_sort() const { return m_sort; }
+        expr* get_src() const { return m_src; }
         unsigned get_idx() const { return m_idx; }
         void set_value(expr * n) { SASSERT(!m_value); m_value = n; }
         expr * get_value() const { return m_value; }
@@ -220,7 +222,7 @@ namespace smt {
         void set_context(context * c) { SASSERT(m_context == 0); m_context = c; }
 
         void register_factory(value_factory * f);
-        extra_fresh_value * mk_extra_fresh_value(sort * s);
+        extra_fresh_value * mk_extra_fresh_value(expr * src, sort* s);
         model_value_proc * mk_model_value(enode* r);
         expr * get_some_value(sort * s);
         proto_model & get_model() { SASSERT(m_model); return *m_model; }
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index b766451df..db6b3da3c 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -998,7 +998,7 @@ namespace smt {
 
                     TRACE("array", tout << pp(n, m) << " " << mk_pp(range, m) << " " << range->is_infinite() << "\n";);
                     if (range->is_infinite())
-                        else_val = TAG(void*, mg.mk_extra_fresh_value(range), 1);
+                        else_val = TAG(void*, mg.mk_extra_fresh_value(n->get_expr(), range), 1);
                     else
                         else_val = TAG(void*, mg.get_some_value(range), 0);
                     m_else_values[r] = else_val;