diff options
| author |  qadeer <unknown> | 2014-01-01 23:50:07 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2014-01-01 23:50:07 -0800 |
| commit | 9beb79c063be35742cf68f272d728b51b945983c (patch) | |
| tree | 5bab2c00af1e6f19db822cc07c04252b54fdf1f3 /Test/og/ticket.bpl | |
| parent | 970965d0b554434d74edac663cdd0d8ab31a2ab4 (diff) | |
fixed examples to deal with yield type checking errors
Diffstat (limited to 'Test/og/ticket.bpl')
| -rw-r--r-- | Test/og/ticket.bpl | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl index 857ca14e..af0c82bf 100644 --- a/Test/og/ticket.bpl +++ b/Test/og/ticket.bpl @@ -30,8 +30,12 @@ requires xls' == mapconstbool(true); var {:linear "tid"} tid: X;
var {:linear "tid"} xls: [X]bool;
+ yield;
+
call xls := Init(xls');
+ par Yield1() | Yield2() | Yield();
+
while (*)
invariant {:phase 1} Inv1(T, t);
invariant {:phase 2} Inv2(T, s, cs);
|