original.name="While_Invalid_13"
js.execute.block=true
======
>>> main.whiley
type nat is (int n) where n >= 0

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

public export method test():
   assume extract(0,[]) == 0
   assume extract(0,[1]) == 0
---
E707 main.whiley 9,19
E724 main.whiley 9,19