original.name="While_Invalid_5"
js.execute.ignore=true
======
>>> main.whiley
function extract(int[] ls) -> int[]:
    int i = 0
    int[] r = [1]
    //
    while i < |ls| where |r| > 0:
        r = [0;0]
        i = i + 1
    //
    return r

public export method test():
   assume extract([]) == [1]
   assume extract([1]) == []
---
E704 main.whiley 5,25:31
E721 main.whiley 5,25:31