original.name="Requires_Valid_2"
boogie.ignore=true
Whiley2Boogie.issue=79
======
>>> main.whiley
function check(int[] args) -> bool
// No element of args can be negative.
requires all { i in 0..|id(args)| | args[i] >= 0 }:
    //
    return true

function id(int[] args) -> (int[] rs)
ensures |args| == |rs|:
    //  
    return args

public export method test():
    assume check([1,2,3])
---