Chalice/tests/regressions/internal-bug-2.chalice


1
2
3
4
5
6
7
8
9
10
11
12
13

class Lala {
    var x;

    predicate inv { acc(x) }

    method koko()
        requires inv
    {
        x := x + 1;
        assert (unfolding inv in x) == old(unfolding inv in x)
    }
}