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

method g(int x) -> (int r)
requires x >= 0:
    return x

public export method test():
    //
    g(f([0]))


---
E716 main.whiley 13,4:12