blob: f255c0203489dae90a69223219568fd6747d6437 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
var x: int;
var y: int;
procedure {:checksum "0"} M();
modifies x, y;
implementation {:id "M"} {:checksum "1"} M()
{
y := 0;
call N();
assert y == 0;
}
procedure {:checksum "2"} N();
modifies x;
|