Closure implementation proof of imported spec crashes Gobra

[ArquintL]

The following code results in a violation within the desugarer:
main.gobra:

package main

import pkg "pkg"

type Impl struct{
    x *int
}

pred (impl Impl) inv() {
    acc(impl.x)
}

func main() {
    x@ := 0

    cl :=   preserves acc(&x)
            func closureImpl() int {
                x += 42
                return x
            }

    proof cl implements pkg.ClosureSpec{Impl{&x}} {
        unfold Impl{&x}.inv()
        res = cl() as closureImpl
        fold Impl{&x}.inv()
    }
}

pkg/pkg.gobra:

package pkg

type Calls interface {
	pred inv()
}

ghost
requires cs != nil
preserves cs.inv()
func ClosureSpec(ghost cs Calls) (res int)

requires fn implements ClosureSpec{cs}
requires cs != nil && cs.inv()
ensures  cs.inv()
func Invoke(fn func () (int), ghost cs Calls) int {
    return fn() as ClosureSpec{cs}
}