From db997cd64d7036f8d212a44e542fcf30eeef5585 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 25 Feb 2025 01:52:42 -0800
Subject: [PATCH] fix regression, missing idx increment in iterator loop #7566

---
 src/qe/mbp/mbp_arrays_tg.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/qe/mbp/mbp_arrays_tg.cpp b/src/qe/mbp/mbp_arrays_tg.cpp
index 502b9ca33..40c3360f4 100644
--- a/src/qe/mbp/mbp_arrays_tg.cpp
+++ b/src/qe/mbp/mbp_arrays_tg.cpp
@@ -201,7 +201,8 @@ struct mbp_array_tg::impl {
                 in = true;
                 eq_index = idx;
                 break;
-            }          
+            }  
+            ++idx;
         }
         if (in) {
             peq p_new = mk_wr_peq(a, p.rhs(), indices);