Test/AbsHoudini/test10.bpl


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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52

// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] %s > %t
// RUN: %diff %s.expect %t
var sdv_7: int;
var sdv_21: int;
function {:existential true} b1(): bool;
function{:existential true}  b2(): bool;
function{:existential true}  b3(): bool;
function{:existential true}  b4(): bool;

procedure push(a:int)
modifies sdv_7, sdv_21;
{
   sdv_21 := sdv_7;
   sdv_7 := a;
}

procedure pop()
modifies sdv_7, sdv_21;
{
   sdv_7 := sdv_21;
   havoc sdv_21;
}

procedure foo()
modifies sdv_7, sdv_21;
requires {:candidate} b1() || (sdv_7 == 0);
ensures{:candidate}  b2() || (sdv_7 == old(sdv_7));
{
   call push(2);
   call pop();
   call bar();
}

procedure bar()
requires{:candidate} b3() || (sdv_7 == 0);
ensures{:candidate}  b4() || (sdv_7 == old(sdv_7));
modifies sdv_7, sdv_21;
{
   call push(1);
   call pop();
}

procedure main()
modifies sdv_7, sdv_21;
{
   sdv_7 := 0;
   call foo();
}

// Expected: All false