Fix out-of-bounds bug in popl20-prod-cons-eq-wvr
The update
array contains non-det values and is never overwritten.
The array is read, and the obtained value is used to access the done
array.
Without checking that the index is smaller than the array size, this leads to an out-of-bound access.
Last year, ESBMC was the only tool detecting this bug.
Note about the milestone: this fix comes after the deadline, which means that this task needs to be excluded from SVCOMP 2025.