Test/snapshots/Snapshots32.v1.bpl


1
2
3
4
5
6
7
8
9
10
11
12

var g: int;

procedure {:checksum "0"} P();
  requires g == 0;

implementation {:id "P"} {:checksum "1"} P()
{
    call Q();
    assert 0 < g;
}

procedure {:checksum "3"} Q();