1 2 3 4 5 6 7 8 9 10 11 12
var g: int; procedure {:checksum "0"} P(); requires g == 0; implementation {:id "P"} {:checksum "1"} P() { call Q(); assert 0 < g; } procedure {:checksum "3"} Q();