Test/test7/MultipleErrors.bpl


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

procedure P(x: int)
{
start:
  goto A, B;

A:
  assert 0 <= x;
  goto C;

B:
  assert x < 100;
  goto C;

C:
  assert x == 87;
  return;
}