Test/civl/chris4.bpl


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

// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
procedure{:yields}{:layer 94,95} Test()
{
  yield;
  L:
  yield;
}

procedure{:yields}{:layer 94,95} Test2()
{
  yield;
  assert{:layer 94} 2 + 2 == 3;
  L:
  yield;
}