blob: a6e6c64aa47e20dfa8faa670d9b9a538f9274b0d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
procedure {:checksum "0"} M(n: int);
implementation {:id "M"} {:checksum "1"} M(n: int)
{
var x: int;
call x := N(n);
assert 0 <= x;
}
procedure {:checksum "3"} N(n: int) returns (r: int);
requires 0 < n;
// Change: weaker postcondition
ensures 0 <= r;
|