From cff06b528f6daf506b422a9a27a8e00a121ed61a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 Feb 2026 20:57:26 -0800 Subject: [PATCH] fix #8563 - align indices for flat quantifiers with sks vector layout, and also guard creating instantiation equalities with sort checks Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_finder.cpp | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index c90f14429..b10178f20 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -2545,11 +2545,11 @@ namespace smt { // Since we only care about q (and its bindings), it only makes sense to restrict the variables of q. bool asserted_something = false; unsigned num_decls = q->get_num_decls(); - // Remark: sks were created for the flat version of q. + // Remark: sks were created for the flat version of q. SASSERT(get_flat_quantifier(q)->get_num_decls() == sks.size()); SASSERT(sks.size() >= num_decls); for (unsigned i = 0; i < num_decls; ++i) { - expr* sk = sks.get(num_decls - i - 1); + expr *sk = sks.get(sks.size() - i - 1); instantiation_set const* s = get_uvar_inst_set(q, i); if (s == nullptr) continue; // nothing to do @@ -2557,15 +2557,17 @@ namespace smt { if (inv.empty()) continue; // nothing to do ptr_buffer eqs; - for (auto const& kv : inv) { - expr* val = kv.m_key; - eqs.push_back(m.mk_eq(sk, val)); + for (auto const& [val, _] : inv) { + if (val->get_sort() == sk->get_sort()) + eqs.push_back(m.mk_eq(sk, val)); + } + if (!eqs.empty()) { + expr_ref new_cnstr(m); + new_cnstr = m.mk_or(eqs); + TRACE(model_finder, tout << "assert_restriction:\n" << mk_pp(new_cnstr, m) << "\n";); + aux_ctx->assert_expr(new_cnstr); + asserted_something = true; } - expr_ref new_cnstr(m); - new_cnstr = m.mk_or(eqs); - TRACE(model_finder, tout << "assert_restriction:\n" << mk_pp(new_cnstr, m) << "\n";); - aux_ctx->assert_expr(new_cnstr); - asserted_something = true; } return asserted_something; }