blob: d6d4332e4d0cf9a672ea53a6781e205b6f119547 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
procedure {:checksum "P1$proc#0"} P1();
// Action: verify
implementation {:checksum "P1$impl#0"} P1()
{
call P2();
}
procedure {:checksum "P2$proc#0"} P2();
// Action: verify
implementation {:checksum "P2$impl#0"} P2()
{
assert 1 != 1;
}
|