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

Fix #7259, #7036: unsound MBP array projection with array var in select/store index

Browse source 
The array term-graph projection (mbp_qel) treats an array equality (= a b)
as an implicit partial array equality and eliminates it by merging the
array variable's congruence class. That rewrite is unsound when the array
variable being eliminated occurs inside a select/store index position,
because the index is a first-class term whose value must be preserved.

For example, (select va (= v va)) was rewritten to (select v true) after
merging va into v, turning a model-false literal into a model-true one and
triggering the qe_mbp validation assertions (qe_mbp.cpp:412 for #7259,
qe_mbp.cpp:622 for #7036), or a crash at qsat.cpp:579 in release builds.

Detect when an array variable to be eliminated occurs inside a select or
store index and fall back to the classic model-based projection
(spacer_qe_lite) for such formulas. Both reproducers now return the correct
unsat verdict with no assertion failure, and all unit tests pass.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
This commit is contained in:
Nikolaj Bjorner 2026-07-28 14:36:18 -07:00
parent b0c15fd46c
commit 5bd9e6a009
1 changed files with 44 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/qe/qe_mbp.cpp
View file

@ -420,6 +420,41 @@ public:
e = mk_and(fmls);
return any_of(subterms::all(e), [&](expr* c) { return seq.is_char(c) || seq.is_seq(c); });
}
// The array term-graph projection (mbp_qel) treats an array equality
// (= a b) as an implicit partial array equality and eliminates it via
// class-merging. That rewrite is unsound when such an equality (or an
// array variable being eliminated) occurs inside a select/store *index*
// position, because the index is a first-class term whose value must be
// preserved. Detect that situation so we can fall back to the classic,
// model-based projection which handles it correctly (issues #7259, #7036).
bool has_array_var_in_index(app_ref_vector const& vars, expr* fml) {
array_util au(m);
ptr_vector<app> arr_vars;
for (app* v : vars)
if (au.is_array(v))
arr_vars.push_back(v);
if (arr_vars.empty())
return false;
for (expr* t : subterms::all(expr_ref(fml, m))) {
if (!is_app(t))
continue;
app* a = to_app(t);
bool is_sel = au.is_select(a);
bool is_st = au.is_store(a);
if (!is_sel && !is_st)
continue;
// args[0] is the array; the trailing arg of a store is the stored
// value; everything in between is an index argument.
unsigned n = a->get_num_args();
unsigned last = is_st ? n - 1 : n;
for (unsigned i = 1; i < last; ++i)
for (app* v : arr_vars)
if (occurs(v, a->get_arg(i)))
return true;
}
return false;
}
void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls, vector<mbp::def>* defs = nullptr) {
//don't use mbp_qel on some theories where model evaluation is
//incomplete This is not a limitation of qel. Fix this either by
@ -554,6 +589,15 @@ public:
void spacer_qel(app_ref_vector& vars, model& mdl, expr_ref& fml) {
TRACE(qe, tout << "Before projection:\n" << fml << "\n" << "Vars: " << vars << "\n";);
// The array term-graph projection is unsound when an array variable to
// be eliminated occurs inside a select/store index. Fall back to the
// classic model-based projection in that case (issues #7259, #7036).
if (has_array_var_in_index(vars, fml)) {
TRACE(qe, tout << "array var in index: using model-based projection\n";);
spacer_qe_lite(vars, mdl, fml);
return;
}
model_evaluator eval(mdl, m_params);
eval.set_model_completion(true);
app_ref_vector other_vars(m);