blob: 727e177d7cc73cb0ce16d58f483756d671612e7f (
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;
}
method N()
ensures P();
predicate P()
ensures P() == Q();
predicate Q()
ensures Q() == R();
predicate R()
{
false
}
|