fix #5297

src/ast/datatype_decl_plugin.cpp

@@ -1082,6 +1082,14 @@ namespace datatype {
         return r;
     }
 
+    bool util::is_recursive_array(sort* a) {
+        array_util autil(m);
+        if (!autil.is_array(a))
+            return false;
+        a = autil.get_array_range_rec(a);                
+        return is_datatype(a) && is_recursive(a);
+    }
+
     bool util::is_enum_sort(sort* s) {
         if (!is_datatype(s)) {
             return false;
@@ -1243,6 +1251,9 @@ namespace datatype {
        defined together in the same mutually recursive definition.
     */
     bool util::are_siblings(sort * s1, sort * s2) {
+        array_util autil(m);
+        s1 = autil.get_array_range_rec(s1);                
+        s2 = autil.get_array_range_rec(s2);                
         if (!is_datatype(s1) || !is_datatype(s2)) {
             return s1 == s2;
         }

src/ast/datatype_decl_plugin.h

@@ -330,6 +330,7 @@ namespace datatype {
         bool is_datatype(sort const* s) const { return is_sort_of(s, fid(), DATATYPE_SORT); }
         bool is_enum_sort(sort* s);
         bool is_recursive(sort * ty);
+        bool is_recursive_array(sort * ty);
         bool is_constructor(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_CONSTRUCTOR); }
         bool is_recognizer(func_decl * f) const { return is_recognizer0(f) || is_is(f); }
         bool is_recognizer0(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_RECOGNISER); }

src/model/array_factory.cpp

@@ -132,13 +132,18 @@ expr * array_factory::get_fresh_value(sort * s) {
         return get_some_value(s);
     }
     sort * range    = get_array_range(s);
-    expr * range_val = m_model.get_fresh_value(range);
-    if (range_val != nullptr) {
-        // easy case
-        func_interp * fi;
-        expr * val = mk_array_interp(s, fi);
-        fi->set_else(range_val);
-        return val;
+    expr* range_val = nullptr;
+
+    if (!m_recursive_fresh) {
+        flet<bool> _recursive(m_recursive_fresh, true);
+        range_val = m_model.get_fresh_value(range);
+        if (range_val != nullptr) {
+            // easy case
+            func_interp* fi;
+            expr* val = mk_array_interp(s, fi);
+            fi->set_else(range_val);
+            return val;
+        }
     }
 
     TRACE("array_factory_bug", tout << "array fresh value: using fresh index, range: " << mk_pp(range, m_manager) << "\n";);

src/model/array_factory.h

@@ -28,6 +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 };
 public:
     array_factory(ast_manager & m, model_core & md);
 

src/model/datatype_factory.cpp

@@ -27,6 +27,8 @@ datatype_factory::datatype_factory(ast_manager & m, model_core & md):
 }
 
 expr * datatype_factory::get_some_value(sort * s) {
+    if (!m_util.is_datatype(s))
+        return m_model.get_some_value(s);
     value_set * set = nullptr;
     if (m_sort2value_set.find(s, set) && !set->empty())
         return *(set->begin());
@@ -77,6 +79,8 @@ bool datatype_factory::is_subterm_of_last_value(app* e) {
    It also updates m_last_fresh_value
 */
 expr * datatype_factory::get_almost_fresh_value(sort * s) {
+    if (!m_util.is_datatype(s))
+        return m_model.get_some_value(s);
     value_set * set = get_value_set(s);
     if (set->empty()) {
         expr * val = get_some_value(s);
@@ -136,6 +140,8 @@ 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);
     TRACE("datatype", tout << "generating fresh value for: " << s->get_name() << "\n";);
     value_set * set = get_value_set(s);
     // Approach 0) 
@@ -162,7 +168,9 @@ expr * datatype_factory::get_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_recursive(s) || !m_util.is_datatype(s_arg) || !m_util.are_siblings(s, s_arg))) {
+            if (!found_fresh_arg && 
+                !m_util.is_recursive_array(s_arg) && 
+                (!m_util.is_recursive(s) || !m_util.is_datatype(s_arg) || !m_util.are_siblings(s, s_arg))) {
                 expr * new_arg = m_model.get_fresh_value(s_arg);
                 if (new_arg != nullptr) {
                     found_fresh_arg = true;
@@ -191,7 +199,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
     // search for constructor...
     unsigned num_iterations = 0;
     if (m_util.is_recursive(s)) {
-        while(true) {
+        while (true) {
             ++num_iterations;
             TRACE("datatype", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
             ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(s);
@@ -207,15 +215,15 @@ expr * datatype_factory::get_fresh_value(sort * s) {
                           << m_util.are_siblings(s, s_arg) << "  is_datatype " 
                           << m_util.is_datatype(s_arg) << " found_sibling " 
                           << found_sibling << "\n";);
-                    if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
+                    if (!found_sibling && m_util.are_siblings(s, s_arg)) {
                         found_sibling = true;
                         expr * maybe_new_arg = nullptr;
-                        if (num_iterations <= 1) {
-                            maybe_new_arg = get_almost_fresh_value(s_arg);
-                        }
-                        else {
+                        if (!m_util.is_datatype(s_arg))
+                            maybe_new_arg = m_model.get_fresh_value(s_arg);
+                        else if (num_iterations <= 1)
+                            maybe_new_arg = get_almost_fresh_value(s_arg);                        
+                        else 
                             maybe_new_arg = get_fresh_value(s_arg);
-                        }
                         if (!maybe_new_arg) {
                             TRACE("datatype", 
                                   tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";);