original.name="Old_Valid_18"
js.compile.ignore=true
boogie.ignore=true
Whiley2Boogie.issue=128
======
>>> main.whiley
type List is null|Node
type Node is &{ List next }

variant unchanged(List l)
where (l is Node) ==> (*l == old(*l))
where (l is Node) ==> unchanged(l->next)

method m(List l)
ensures unchanged(l):
    skip

public export method test():
    List l1 = new {next:null}
    List l2 = new {next:l1}
    //
    m(l2)
    assert l2->next == l1
    assert l1->next == null
---