mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-26 17:02:38 +00:00
Code Activity

qe2: eliminate fresh undeclared constant leak (#10172)

Browse source 
spacer_qel could report a bound variable as eliminated (removing it from
vars) while do_qel/qel_project simplifications still left an occurrence of
it in the formula. The variable then surfaced in the qe2 result as a
fresh, undeclared constant (e.g. X!0), so asserting the result failed with
"unknown constant".

After qel_project, scan the formula for any originally-to-eliminate
variable that was dropped from vars yet still occurs in fml, and route it
through other_vars so the existing model-based projection/substitution
replaces it with its model value. The result is logically equivalent and
mentions only declared symbols.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
This commit is contained in:
Nikolaj Bjorner 2026-07-23 10:43:38 -07:00
parent 48f1676f2b
commit caeaaa7d07
1 changed files with 15 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/qe/qe_mbp.cpp
View file

@ -562,6 +562,12 @@ public:
arith_util ari_u(m);
datatype_util dt_u(m);
// Remember the variables we were asked to eliminate. do_qel/qel_project
// can report a variable as eliminated (drop it from vars) while a
// simplification still leaves an occurrence of it in fml. Such a
// variable is a fresh, undeclared constant in the result (issue #10172).
app_ref_vector orig_vars(vars);
do_qel(vars, fml);
qel_project(vars, mdl, fml, m_reduce_all_selects);
flatten_and(fml);
@ -573,6 +579,15 @@ public:
other_vars.push_back(v);
}
// Recover variables that were reported eliminated but still occur in
// fml. Route them through the model-based projection/substitution below
// so they are replaced by their model values instead of leaking out as
// undeclared constants.
for (app* v : orig_vars) {
if (!vars.contains(v) && !other_vars.contains(v) && occurs(v, fml))
other_vars.push_back(v);
}
// project reals, ints and other variables.
if (!other_vars.empty()) {
TRACE(qe, tout << "Other vars: " << other_vars << "\n" << mdl;);