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

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