mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

Fix MBQI completeness regression for array-valued universal variables

Browse source 
Commit "Term enumeration (#9908)" routed array-valued universal
variables in the model finder through a new ho_var qinfo. Its
populate_inst_sets fills the variable's instantiation set with
synthesized/enumerated array terms. restrict_sks_to_inst_set in
smt_model_checker then builds a large disjunction over that polluted
set, which can make the auxiliary model-check return l_undef. When that
happens the decisive instantiation that the ordinary instantiation sets
already provide is discarded, and MBQI reports unknown instead of the
correct result.

Do not route array-valued universal variables through the
term-enumeration ho_var path; keep the prior behaviour of only marking
m_is_auf = false. This restores completeness on
inputs/issues/iss-5336/bug-5.smt2, which regressed from unsat to
unknown.

Validated by rebuilding z3 and re-running the benchmark with -T:20: it
now returns unsat (byte-exact with the recorded oracle). A sample of
other quantifier benchmarks was unaffected.

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

14
src/smt/smt_model_finder.cpp
View file

@ -2188,10 +2188,16 @@ namespace smt {
process_app(to_app(curr));
}
else if (is_var(curr)) {
if (m_array_util.is_array(curr)) {
insert_qinfo(alloc(ho_var, m, to_var(curr)->get_idx()));
}
m_info->m_is_auf = false;
// Note: array-valued universal variables are intentionally
// not routed through the term-enumeration ho_var path here.
// Doing so populates the variable's instantiation set with
// synthesized array terms; restrict_sks_to_inst_set then
// builds a large disjunction that can make the auxiliary
// model-check in smt_model_checker return l_undef, discarding
// the decisive instantiation that the ordinary instantiation
// sets already provide. That regressed MBQI completeness
// (e.g. inputs/issues/iss-5336/bug-5.smt2 went unsat -> unknown).
m_info->m_is_auf = false; // unexpected occurrence of variable.
}
else {
SASSERT(is_lambda(curr));