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


/**
 * Perform a merge sort of integer items.
 */
function loop2(int p, int q) -> (int r)
    requires p > 0 && q > 0
    ensures r == q*p:
    int qq = 0
    int i = 0

    while i< p
       where i <= p
       where qq == q*i:
       i = i+1
       qq = qq + q
    //assert i == p // uncomment this and it verifies!
    assert qq == q*p
    return qq

public export method test():
    assume loop2(5,10) == 50

---