blob: 0ee0f1b987c6c302e35c474f8b24c1fb3843a6ff (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
function {:existential true} b0(x:int): bool;
function {:existential true} b1(x:int): bool;
var g: int;
procedure foo()
modifies g;
requires b0(g);
ensures b1(g);
{
if(*) {
g := g + 1;
call foo();
}
}
procedure main()
modifies g;
{
g := 0;
if(*) { g := 5; }
call foo();
}
// Expected: b0(x) = [0,\infty], b1(x) = [0, \infty]
|
