during printing, track the current handle more explicitly
This is more preparation to generate independent handles when traversing a
scalarset-indexed array. The relative offset for a given array element in the
previous state is not the same as the relative offset in the current state,
because the previous and current states may have different schedules for the
index type.
E.g. given a scalarset(4), the original type contains {0, 1, 2, 3}. The schedule
of this type in the previous state might be the permutation {2, 3, 1, 0} while
the schedule in the current state might be {3, 2, 0, 1}. So when retrieving the
0th element of the array, this is actually at the 2nd element in the current
state and the 3rd element in the previous state.
Github: related to #194 "clearer CEX output with scalarsets"
parent
be2cf345
Please register or sign in to comment