mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 09:04:07 +00:00
Code Activity

fix #7554

Browse source 
mbp_qel  uses two iterations of saturation.
The first iteration uses only congruences, not the model.
The second iteration uses the model.
Terms are marked as "seen" during either iteration and will not be reprocessed if they are "seen".
All select terms get marked as "seen" to avoid reproducing Ackerman axioms.
But this conflicts with expanding select-store axioms during
the phase of saturation where use_model is allowed.
This commit is contained in:
Nikolaj Bjorner 2025-02-18 21:04:34 -08:00
parent 28f3f8046e
commit e0945f57bb
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/qe/mbp/mbp_arrays_tg.cpp
View file

@ -401,9 +401,13 @@ struct mbp_array_tg::impl {
if (m_array_util.is_select(term) &&
has_var(to_app(term)->get_arg(0))) {
rdTerms.push_back(to_app(term));
if (is_seen(term)) continue;
if (is_seen(term))
continue;
add_rdVar(term);
mark_seen(term);
// select-store axioms are only introduced during m_use_mdl
// so don't mark select-store terms if m_use_mdl is false
if (m_use_mdl || !m_array_util.is_store(to_app(term)->get_arg(0)))
mark_seen(term);
}
}
if (!m_use_mdl)