mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

Fix MBQI model-construction regression on UFLIA (iss-5421)

Browse source 
The term-enumeration change (#9908) added extra lambda definition
equalities (val = term) to the auxiliary restriction context in
restrict_sks_to_inst_set. These extra constraints over-constrain the
auxiliary MBQI solver, causing model construction to fail (smt.mbqi
:failed) and the solver to loop in final-check until timeout on
otherwise-sat UFLIA problems.

Restore the original restriction that constrains each skolem to one of
its inverse values without asserting the lambda-definition equalities.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-07-10 00:56:41 -07:00 • committed by GitHub
parent 1d425e55cd
commit 37f1ac2e5d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/smt/smt_model_finder.cpp
View file

@ -2675,27 +2675,16 @@ namespace smt {
obj_map<expr, expr*> const& inv = s->get_inv_map();
if (inv.empty())
continue; // nothing to do
expr_ref_vector eqs(m), defs(m);
for (auto const& [val, term] : inv) {
if (val->get_sort() == sk->get_sort()) {
if (is_lambda(term)) {
eqs.push_back(m.mk_eq(sk, val));
defs.push_back(m.mk_eq(val, term));
}
else
eqs.push_back(m.mk_eq(sk, val));
}
ptr_buffer<expr> eqs;
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);
for (auto def : defs) {
TRACE(model_finder, tout << "assert_def:\n" << mk_pp(def, m) << "\n";);
aux_ctx->assert_expr(def);
}
asserted_something = true;
}
}