blob: 5cbc000aa8affaaec83c2aa1541348190135e771 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
procedure{:yields}{:layer 94,94} H()
{
yield;
}
procedure{:yields}{:layer 94,95} A()
ensures{:atomic} |{ A: return true; }|;
{
yield;
}
procedure{:yields}{:layer 95,95} P()
{
yield;
par A() | H();
yield;
}
|
