mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

fix regression, missing idx increment in iterator loop #7566

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-02-25 01:52:42 -08:00
parent a7310462df
commit db997cd64d
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -201,7 +201,8 @@ struct mbp_array_tg::impl {
in = true; in = true;
eq_index = idx; eq_index = idx;
break; break;
} }
++idx;
} }
if (in) { if (in) {
peq p_new = mk_wr_peq(a, p.rhs(), indices); peq p_new = mk_wr_peq(a, p.rhs(), indices);