blob: 02a91b521fdc70643b4d0986fca2d9eb54c48715 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
method M()
{
N();
assert false; // error
}
method N()
ensures P();
predicate P()
ensures P() == Q();
predicate Q()
ensures Q() == R();
predicate R()
{
true
}
|