original.name="Array_Invalid_24" ====== >>> main.whiley function f(int[] xs) -> (int r) requires |xs| > 0 ensures r < |xs|: // return 0 public export method test(): // int[] xs = [0] xs[f([0])] = 1 assert xs == [1] --- E724 main.whiley 10,7:12