diff --git a/src/ackermannization/ackr_info.h b/src/ackermannization/ackr_info.h
index 67c41bda2..7cb27e2a6 100644
--- a/src/ackermannization/ackr_info.h
+++ b/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);
         }
diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp
index 57d414464..10b70a7f4 100644
--- a/src/ackermannization/ackr_model_converter.cpp
+++ b/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);
     }
 
diff --git a/src/model/datatype_factory.h b/src/model/datatype_factory.h
index 2d8f216b4..c68a87a29 100644
--- a/src/model/datatype_factory.h
+++ b/src/model/datatype_factory.h
@@ -25,7 +25,7 @@ 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;
+    static const unsigned m_max_fresh_depth = 128;
     
     expr * get_last_fresh_value(sort * s);
     expr * get_almost_fresh_value(sort * s);
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 27516b3dc..627f0ea88 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -2163,7 +2163,9 @@ namespace smt {
                 }
 
                 SASSERT(is_quantifier(atom));
-                UNREACHABLE();
+                // Nested quantifiers as atoms are not expected but can occur
+                // in unsimplified formulas. Skip gracefully.
+                return;
             }
 
             void process_literal(expr* atom, polarity pol) {
@@ -2205,7 +2207,9 @@ namespace smt {
                             switch (static_cast<basic_op_kind>(to_app(curr)->get_decl_kind())) {
                             case OP_IMPLIES:
                             case OP_XOR:
-                                UNREACHABLE(); // simplifier eliminated ANDs, IMPLIEs, and XORs
+                                // Implies/XOR should be simplified away but handle gracefully
+                                // by treating as uninterpreted boolean.
+                                process_literal(curr, pol);
                                 break;
                             case OP_OR:
                             case OP_AND:
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 8cf9508d6..4d88e34a0 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/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);