NullPointerException in WyalFilePrinter

[DavePearce]

The following Whiley generates a NullPointerException in WyalFilePrinter:

function permute(int[] xs) -> (int[] rs, int[] witness)
ensures |rs| == |witness|
ensures |xs| == |witness|:
    //
    int[] ws = [0; |xs|] // ghost "witness"
    //
    return xs,ws

public export method test():
    int[] ys
    int[] ws
    //
    ys,ws = permute([1,2,3])
    assume ys == [1,2,3] && ws == [0,1,2]

This looks like it has something to do with multiple returns.

[DavePearce]

UPDATE. Yes, this is to do with the postcondition macro permute_ensures_0 which is presumably failing.

[DavePearce]

Here is a smaller example:

function f(int x) -> (int r1, int r2)
ensures r1 >= r2:
    //
    return x, (x+1)

function g(int x) -> (int r):
    int a
    int b
    a,b = f(x)
    return a+b

[DavePearce]

The problem here is that we need syntax for extracting the result of a function which has multiple returns.