Test/snapshots/Snapshots3.v0.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

procedure {:checksum "P0$proc#0"} P0();
ensures G();
// Action: verify
implementation {:checksum "P0$impl#0"} P0()
{
}


function {:checksum "F#0"} F() : bool
{
    true
}


function {:checksum "G#0"} G() : bool
{
    F()
}