summaryrefslogtreecommitdiff
path: root/Test/AbsHoudini/imp1.bpl
blob: 09be87e76a9222e3e4954b82b1c1938bccf89318 (plain)
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;
}