Test/AbsHoudini/imp1.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

function {:existential true} {:absdomain "ImplicationDomain"} b1(x1: bool, x2: bool) : bool;
function {:existential true} {:absdomain "ImplicationDomain"} b2(x1: bool, x2: bool) : bool;

var x: int;
var flag: bool;

procedure foo ()
  modifies x, flag;
  ensures b1(flag, x == 0);
{
   flag := true;
   x := 0;
}

procedure bar()
  modifies x, flag;
  ensures b2(flag, x == 0);
{
   flag := false;
   x := 0;
}