Test/lazyinline/foo.bpl


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

var g: int;

procedure A()
requires g == 0;
modifies g;
ensures g == 2;
{
  var x : int;
  x := 4;
  while (g < x) {
    g := g + 1;
    x := x - 1;
  }
  assert x == 2;
}