blob: ad3f1f2703e2e38bdf55d895ce8a5f99a94fb3a0 (
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;
|