blob: 8700e91c0956597988d73c9d074c3876181c5d1c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
var x: int;
var y: int;
var z: int;
procedure {:checksum "0"} M();
modifies x, y, z;
implementation {:id "M"} {:checksum "1"} M()
{
z := 0;
call N();
assert y < 0;
}
procedure {:checksum "3"} N();
// Change: fewer modified variables
modifies x;
ensures y < z;
|