1 2 3 4 5 6 7 8 9
procedure {:checksum "0"} P(b: bool); implementation {:id "P"} {:checksum "2"} P(p: bool) { var l: [int]bool; l := (lambda n: int :: false); assert l[0]; }