original.name="While_Invalid_19"
js.execute.ignore=true
======
>>> main.whiley
type nat is (int x) where x >= 0

property same(int[] arr, int n) -> (bool r):
   if n >= 1 && n <= |arr|:
      return all { i in 1..n | arr[i-1] == arr[i] }
   else:
      return false

function create(int start, int end) -> (int[] result)
ensures same(result,|result|) && |result| == (end - start):
    //
    nat i = 1
    nat length = (end - start)
    int[] items = [0;length]
    //
    while i < length 
    where i > 0 && |items| == length
    where same(items,i):
        items[i] = items[i-1]
        i = i + 1
    // Done
    return items

public export method test():
    //
    assume create(0,1) == [0]
    assume create(0,2) == [0,0]
    assume create(0,3) == [0,0,0]
    assume create(1,0) == []
---
E702 main.whiley 13,18:28
E718 main.whiley 13,18:28