Chalice/tests/regressions/workitem-10223.chalice


1
2
3
4
5
6
7
8

class Lala {
    var next: Lala;
    var x: int;
    predicate inv {
        acc(next) && acc(x) &&
        (next != null ==> (next.inv && unfolding next.inv in this.x > next.x))
    }
}