Test/AbsHoudini/pred2.bpl


1
2
3
4
5
6
7
8
9
10
11
12

function {:existential true} b0(x:bool): bool;

var g: int;

procedure main()
modifies g;
ensures b0(g == old(g));
{
  if(*) { g := 5; }
  assume g != 5;
}