mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-26 22:03:34 +00:00
Code Activity

fix #8563 - align indices for flat quantifiers with sks vector layout, and also guard creating instantiation equalities with sort checks

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-02-16 20:57:26 -08:00
parent c0e8698bae
commit cff06b528f
1 changed files with 12 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/smt_model_finder.cpp
View file

@ -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. // Since we only care about q (and its bindings), it only makes sense to restrict the variables of q.
bool asserted_something = false; bool asserted_something = false;
unsigned num_decls = q->get_num_decls(); 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(get_flat_quantifier(q)->get_num_decls() == sks.size());
SASSERT(sks.size() >= num_decls); SASSERT(sks.size() >= num_decls);
for (unsigned i = 0; i < num_decls; ++i) { 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); instantiation_set const* s = get_uvar_inst_set(q, i);
if (s == nullptr) if (s == nullptr)
continue; // nothing to do continue; // nothing to do
@ -2557,15 +2557,17 @@ namespace smt {
if (inv.empty()) if (inv.empty())
continue; // nothing to do continue; // nothing to do
ptr_buffer<expr> eqs; ptr_buffer<expr> eqs;
for (auto const& kv : inv) { for (auto const& [val, _] : inv) {
expr* val = kv.m_key; if (val->get_sort() == sk->get_sort())
eqs.push_back(m.mk_eq(sk, val)); 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; return asserted_something;
} }