blob: e1fec0ed79ce6e15a1ee503b4241dcdd520d9e6f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
procedure {:checksum "0"} M();
implementation {:id "M"} {:checksum "2"} M()
{
if (*)
{
assert 1 == 1;
}
else
{
assert 2 != 2; // error
}
assert 3 != 3; // error
}
|