1 2 3 4 5 6 7 8 9 10 11 12 13
method M() { N(); assert false; } method N() ensures P(); predicate P() { false }