(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
(see also #126)
For reasons unknown recursive variants fail to verify. A minimal example is: