summaryrefslogtreecommitdiff
path: root/Test/AbsHoudini/int1.bpl
blob: eb4e6b5158d38d9ce2efc87d79afdfb7d64d64b5 (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]