blob: 5ff7bb4d376ef706564b527f2868709a9d9aa821 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
procedure {:checksum "P0$proc#5"} P0();
requires F0();
ensures F0();
// Action: verify (procedure changed)
implementation {:checksum "P0$impl#0"} P0()
{
call P0();
}
function {:checksum "F0#1"} F0() : bool
{
false
}
|