Merge a90901b7c5 into d9385e9713

src/ackermannization/ackr_info.h

@@ -71,6 +71,10 @@ class ackr_info {
             return rv;
         }
 
+        typedef obj_map<func_decl, app*>::iterator c2t_iterator;
+        c2t_iterator begin_c2t() const { return m_c2t.begin(); }
+        c2t_iterator end_c2t() const { return m_c2t.end(); }
+
         inline app* get_abstr(app* term)  const {
             return m_t2c.find(term);
         }

src/ackermannization/ackr_model_converter.cpp

@@ -103,6 +103,8 @@ void ackr_model_converter::convert_constants(model * source, model * destination
     evaluator.set_model_completion(true);
     array_util autil(m);
 
+    obj_hashtable<func_decl> processed;
+
     for (unsigned i = 0, n = source->get_num_constants(); i < n; ++i) {
         func_decl * const c = source->get_constant(i);
         app * const term = info->find_term(c);
@@ -110,9 +112,30 @@ void ackr_model_converter::convert_constants(model * source, model * destination
         TRACE(ackermannize, tout << mk_ismt2_pp(c, m) << " " << mk_ismt2_pp(term, m) << "\n";);
         if (!term) 
             destination->register_decl(c, value);
-        else if (autil.is_select(term)) 
+        else if (autil.is_select(term)) {
             add_entry(evaluator, term, value, array_interpretations);
-        else 
+            processed.insert(c);
+        }
+        else {
+            add_entry(evaluator, term, value, interpretations);
+            processed.insert(c);
+        }
+    }
+
+    // Process any abstract constants from ackr_info that are missing from the model.
+    // This can happen when downstream tactics (e.g., solve-eqs) eliminate the constant
+    // before it reaches the solver, so it has no model value.
+    for (auto it = info->begin_c2t(); it != info->end_c2t(); ++it) {
+        func_decl * const c = it->m_key;
+        if (processed.contains(c))
+            continue;
+        app * const term = it->m_value;
+        expr_ref value(m);
+        value = evaluator(m.mk_const(c));
+        TRACE(ackermannize, tout << "missing from model: " << mk_ismt2_pp(c, m) << " " << mk_ismt2_pp(term, m) << " -> " << value << "\n";);
+        if (autil.is_select(term))
+            add_entry(evaluator, term, value, array_interpretations);
+        else
             add_entry(evaluator, term, value, interpretations);
     }
 

src/model/datatype_factory.cpp

@@ -139,6 +139,10 @@ 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);
+    ++m_fresh_depth;
+    on_scope_exit _dg([&]() { --m_fresh_depth; });
     TRACE(datatype, tout << "generating fresh value for: " << s->get_name() << "\n";);
     auto& [set, values] = get_value_set(s);
     // Approach 0) 

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 = 128;
     
     expr * get_last_fresh_value(sort * s);
     expr * get_almost_fresh_value(sort * s);

src/smt/smt_model_generator.cpp

@@ -143,6 +143,8 @@ namespace smt {
             CTRACE(model, n == 0, 
                    tout << mk_pp(r->get_expr(), m) << "\nsort:\n" << mk_pp(s, m) << "\n";
                    tout << "is_finite: " << m_model->is_finite(s) << "\n";);
+            if (!n)
+                n = m_model->get_some_value(s);
         }
         return alloc(expr_wrapper_proc, to_app(n));
     }
@@ -371,7 +373,11 @@ namespace smt {
                             TRACE(mg_top_sort, tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_expr(), m) << "): " 
                                   << mk_pp(child->get_expr(), m) << " " << mk_pp(child->get_root()->get_expr(), m) << "\n";);
                             child = child->get_root();
-                            dependency_values.push_back(m_root2value[child]);
+                            app * child_val = nullptr;
+                            m_root2value.find(child, child_val);
+                            if (!child_val)
+                                child_val = to_app(m_model->get_some_value(child->get_sort()));
+                            dependency_values.push_back(child_val);
                         }
                     }
                     val = proc->mk_value(*this, dependency_values);