blob: fac2ecc77d19f09cc3b1e39bfe859f218b457e35 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
// RUN: %diff %s.expect %t
// XFAIL: *
procedure {:yields} X();
ensures {:atomic 0} |{ A: return true; }|;
procedure {:yields} Y();
ensures {:left 0} |{ A: return true; }|;
procedure {:yields} main() {
yield;
call X();
while (*)
// invariant {:terminates} true;
{
call Y();
}
yield;
assert {:phase 1} true;
}
|
