original.name="Array_Valid_12"
======
>>> main.whiley
function f(int[] xs) -> (int r)
requires |xs| > 0
ensures r >= 0 && r < |xs|:
    //
    return 0

public export method test():
    //
    int[] xs = [0]
    xs[f([0])] = 1
    assert xs == [1]
    int[] ys = [1,2]
    ys[f(ys)] = 3
    assert (ys[0] == 3) || (ys[1] == 3)


---