From e0945f57bb550208802a3884ac6ece633bc5ed3f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 18 Feb 2025 21:04:34 -0800 Subject: [PATCH] fix #7554 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. --- src/qe/mbp/mbp_arrays_tg.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/qe/mbp/mbp_arrays_tg.cpp b/src/qe/mbp/mbp_arrays_tg.cpp index 44456666b..76dc5dc2c 100644 --- a/src/qe/mbp/mbp_arrays_tg.cpp +++ b/src/qe/mbp/mbp_arrays_tg.cpp @@ -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)