Test/og/one.bpl


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

var x:int;

procedure A()
modifies x;
{
  x := x;
}

procedure {:yields} B()
{
  x := 5;
  yield;
  assert x == 5;
}