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