Generate index access constraints for maps and arrays

[lorchrob]

Generate index access constraints for arrays. In other words, for each array access a[i], generate the constraint that i is between 0 and the length of the array minus 1 (inclusive).

If inductive or quantified variables are used in array index accesses, then we universally quantify them in the generated property.

This PR should not be merged until we have support for certain operators with lazy semantics, which we can use to mitigate spurious property violations as in the following example (the generated property for A[i-1] is falsified when i is 0, even though it is in the else branch of the assignment)

A[i] = if i = 0 then 0 else A[i-1] + 1

Side note -- analogous constraints are not generated for map index accesses due to situations like the following:

l = 0 -> m[0];
m = map[]@<int, int> -> (pre m)[0 := 1];

Above, index access constraint 0 in m would raise a counterexample with a single timestep, even though the access is properly guarded, and there is not a straightforward way to address the situation.