Test/og/houd1.bpl


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

const {:existential true} b0: bool;
const {:existential true} b1: bool;
const {:existential true} b2: bool;

var x:int;

procedure A()
{
  x := x + 1;
  yield;
}

procedure B()
{
  x := 5;
  yield;
  assert b0 ==> (x == 5);
  assert b1 ==> (x >= 5);
  assert b2 ==> (x >= 6);
}