Recursive Variants

[DavePearce]

(see also #126)

For reasons unknown recursive variants fail to verify. A minimal example is:

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