From 075773e51970f854d923a47359802ef59c0eb083 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Feb 2025 00:02:38 -0800 Subject: [PATCH] remove proviso for single index arrays --- src/qe/mbp/mbp_arrays_tg.cpp | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/qe/mbp/mbp_arrays_tg.cpp b/src/qe/mbp/mbp_arrays_tg.cpp index 76dc5dc2c..502b9ca33 100644 --- a/src/qe/mbp/mbp_arrays_tg.cpp +++ b/src/qe/mbp/mbp_arrays_tg.cpp @@ -67,15 +67,11 @@ struct mbp_array_tg::impl { } bool is_wr_on_rhs(expr *lhs, expr *rhs) { - return (is_arr_write(rhs) && !is_arr_write(lhs)); + return is_arr_write(rhs) && !is_arr_write(lhs); } bool is_arr_write(expr *t) { - return m_array_util.is_store1(t) && has_var(to_app(t)); - } - - bool is_arr_write(expr *t, expr*& a, expr*& i, expr*& v) { - return m_array_util.is_store1(t, a, i, v) && has_var(to_app(t)); + return m_array_util.is_store(t) && has_var(to_app(t)); } // Returns true if e has a subterm store(v) where v is a variable to be