From a4a84ed083bc7d40e4f53f90d054060e82b0b5b0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 18 Feb 2025 19:13:12 -0800 Subject: [PATCH] arrays are not necessarily unary --- src/qe/mbp/mbp_arrays_tg.cpp | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/src/qe/mbp/mbp_arrays_tg.cpp b/src/qe/mbp/mbp_arrays_tg.cpp index d2744f72a..bd67d988c 100644 --- a/src/qe/mbp/mbp_arrays_tg.cpp +++ b/src/qe/mbp/mbp_arrays_tg.cpp @@ -378,24 +378,26 @@ struct mbp_array_tg::impl { mark_seen(term); } } - if (!m_use_mdl) return progress; - expr *e1, *e2, *a1, *a2, *i1, *i2; + if (!m_use_mdl) + return progress; for (unsigned i = 0; i < rdTerms.size(); i++) { - e1 = rdTerms.get(i); - a1 = to_app(e1)->get_arg(0); - i1 = to_app(e1)->get_arg(1); + app* e1 = to_app(rdTerms.get(i)); + expr* a1 = e1->get_arg(0); for (unsigned j = i + 1; j < rdTerms.size(); j++) { - e2 = rdTerms.get(j); - a2 = to_app(e2)->get_arg(0); - i2 = to_app(e2)->get_arg(1); - if (!is_seen(e1, e2) && a1->get_id() == a2->get_id()) { + app* e2 = to_app(rdTerms.get(j)); + expr* a2 = e2->get_arg(0); + if (!is_seen(e1, e2) && a1 == e2) { mark_seen(e1, e2); progress = true; - if (m_mdl.are_equal(i1, i2)) { - m_tg.add_eq(i1, i2); - } else { - SASSERT(!m_mdl.are_equal(i1, i2)); - m_tg.add_deq(i1, i2); + for (unsigned k = 1; k < e1->get_num_args(); ++k) { + expr* i1 = e1->get_arg(k); + expr* i2 = e2->get_arg(k); + if (m_mdl.are_equal(i1, i2)) + m_tg.add_eq(i1, i2); + else { + SASSERT(!m_mdl.are_equal(i1, i2)); + m_tg.add_deq(i1, i2); + } } continue; }