summaryrefslogtreecommitdiff
path: root/Test/snapshots/Snapshots2.v3.bpl
blob: fd06e3355478e8ea7944cc4f652bd8f1d8a77286 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
procedure {:checksum "P0$proc#2"} P0();
requires F0();
// Action: verify (function changed)
implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
{
    call P0();
}


function {:checksum "F0#1"} F0() : bool
{
    false
}