original.name="Old_Valid_17"
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->next == old(l->next))
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
---