original.name="While_Invalid_7"
======
>>> main.whiley
type nat is (int n) where n >= 0

function extract(int[] ls) -> int[]:
    int i = 0
    int[] r = [0; |ls|]
    //
    while i < |ls|:
        r[i] = ls[i]
        i = i + 1
    //
    return r

public export method test():
   assume extract([]) == []
   assume extract([1]) == [1]
   assume extract([1,2]) == [1,2]
   assume extract([1,2,3]) == [1,2,3]
---
E724 main.whiley 8,10