original.name="While_Valid_35"
======
>>> main.whiley


function lastIndexOf(int[] xs, int x) -> (int|null r)
ensures r is int ==> xs[r] == x:
    //
    int i = 0
    int last = -1
    //
    while i < |xs| 
        where i >= 0 && last >= -1 && last < |xs|
        where last == -1 || xs[last] == x:
        //
        if xs[i] == x:
            last = i
        i = i + 1
    //
    if last == -1:
        return null
    else:
        return last

public export method test():
    int[] list = [1,2,1,3,1,2]
    assume lastIndexOf(list,0) == null
    assume lastIndexOf(list,1) == 4
    assume lastIndexOf(list,2) == 5
    assume lastIndexOf(list,3) == 3

---