Mysterious issues with monotonicBool.pvl example

[Naum-Tomov]

The original contract from line 63 throws the following exception:

At examples\concepts\parallel\monotonicBool.pvl:65:17:
65 context Perm(contrib[tid], 1\2);
Index may be negative, or exceed the length of the array. (https://utwente.nl/vercors#arrayBounds)

---

This can be fixed by modifying the contract, by adding:
ensures(contrib.length == N);

This shouldn't be necessary and warrants investigation. Furthermore, after fixing this issue, the verification still fails, throwing the following exception:
82 assert b == (\exists int i = 0..N; contrib[i]);
There may be insufficient permission to access this field here. (https://utwente.nl/vercors#perm)

This also doesn't logically make sense, as we should have read permission for that field at that point.

[pieter-bos]

This seems pretty similar to #887