diff options
Diffstat (limited to 'Test/og/Program3.bpl')
-rw-r--r-- | Test/og/Program3.bpl | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Test/og/Program3.bpl b/Test/og/Program3.bpl index e1b014b7..e2c55c8e 100644 --- a/Test/og/Program3.bpl +++ b/Test/og/Program3.bpl @@ -12,11 +12,14 @@ ensures {:phase 1} x >= 8; call Incr(1);
call yield_x();
call Incr(1);
+ call yield_x();
}
procedure {:yields} {:phase 1} q()
{
+ yield;
call Incr(3);
+ yield;
}
procedure {:yields} {:phase 0,1} Incr(val: int);
|