1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
var x: int; var y: int; procedure {:entrypoint} {:yields} foo() modifies x, y; { assume x == y; x := x + 1; async call P(); y := y + 1; } procedure {:yields} {:stable} P() requires x != y; { assert x != y; }