1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
var x: int; var y: int; var z: int; procedure {:checksum "0"} M(); modifies x, y, z; implementation {:checksum "1"} M() { z := 0; call N(); assert y < 0; } procedure {:checksum "3"} N(); modifies x; ensures y < z;