From e3281e45e7df4d3f0dd2adad3124b47f28fd2eb1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 31 May 2026 17:41:34 -0700 Subject: [PATCH 1/3] add depth guard --- src/model/datatype_factory.cpp | 3 +++ src/model/datatype_factory.h | 2 ++ 2 files changed, 5 insertions(+) diff --git a/src/model/datatype_factory.cpp b/src/model/datatype_factory.cpp index b93703acd..fac858ccc 100644 --- a/src/model/datatype_factory.cpp +++ b/src/model/datatype_factory.cpp @@ -139,6 +139,9 @@ 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); + struct depth_guard { unsigned& d; depth_guard(unsigned& d) : d(d) { ++d; } ~depth_guard() { --d; } } _dg(m_fresh_depth); TRACE(datatype, tout << "generating fresh value for: " << s->get_name() << "\n";); auto& [set, values] = get_value_set(s); // Approach 0) diff --git a/src/model/datatype_factory.h b/src/model/datatype_factory.h index b2a6b75d3..2d8f216b4 100644 --- a/src/model/datatype_factory.h +++ b/src/model/datatype_factory.h @@ -24,6 +24,8 @@ Revision History: class datatype_factory : public struct_factory { datatype_util m_util; obj_map m_last_fresh_value; + unsigned m_fresh_depth = 0; + static const unsigned m_max_fresh_depth = 512; expr * get_last_fresh_value(sort * s); expr * get_almost_fresh_value(sort * s); From 4b32bab0acd132fa5ba02728b8ffde9044d0f0e1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Jun 2026 12:23:42 -0700 Subject: [PATCH 2/3] Fix model generation bugs causing crashes in QF_ABV, UFBVLIA, and UFDT benchmarks 1. Fix Ackermannization model converter (QF_ABV): When solve-eqs or elim-unconstrained eliminates abstract constants introduced by ackermannize_bv, those constants are missing from the model when the Ackermann model converter runs. This causes missing array entries and invalid models. Fix: iterate over ALL entries in ackr_info (not just model constants) to reconstruct missing values via model completion. 2. Fix null dereference in model generator (UFBVLIA): When get_fresh_value returns nullptr (finite sort exhausted) or when m_root2value has no entry for a dependency child, fall back to get_some_value instead of crashing. 3. Fix UNREACHABLE assertions in model finder (UFBVLIA): Handle nested quantifiers as atoms and unsimplified OP_IMPLIES/OP_XOR gracefully instead of aborting. 4. Reduce datatype max fresh depth from 512 to 128 (UFDT): Prevents stack overflow on Linux for deeply recursive datatype models. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ackermannization/ackr_info.h | 4 +++ src/ackermannization/ackr_model_converter.cpp | 27 +++++++++++++++++-- src/model/datatype_factory.h | 2 +- src/smt/smt_model_finder.cpp | 8 ++++-- src/smt/smt_model_generator.cpp | 8 +++++- 5 files changed, 43 insertions(+), 6 deletions(-) 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::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 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 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(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); From a90901b7c508e35b0c7976725bb430bbe1589e9f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 18 Jun 2026 20:01:17 +0000 Subject: [PATCH 3/3] Replace inline depth_guard struct with on_scope_exit in datatype_factory.cpp --- src/model/datatype_factory.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/model/datatype_factory.cpp b/src/model/datatype_factory.cpp index fac858ccc..64f6f7367 100644 --- a/src/model/datatype_factory.cpp +++ b/src/model/datatype_factory.cpp @@ -141,7 +141,8 @@ expr * datatype_factory::get_fresh_value(sort * s) { return m_model.get_fresh_value(s); if (m_fresh_depth >= m_max_fresh_depth) return get_last_fresh_value(s); - struct depth_guard { unsigned& d; depth_guard(unsigned& d) : d(d) { ++d; } ~depth_guard() { --d; } } _dg(m_fresh_depth); + ++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)