diff options
Diffstat (limited to 'Test/og/multiset.bpl')
| -rw-r--r-- | Test/og/multiset.bpl | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl index 3305b63f..459cb470 100644 --- a/Test/og/multiset.bpl +++ b/Test/og/multiset.bpl @@ -339,6 +339,8 @@ procedure {:yields} {:phase 1} Yield1() requires {:phase 1} Inv(valid, elt, owner);
ensures {:phase 1} Inv(valid, elt, owner);
{
+ yield;
+ assert {:phase 1} Inv(valid, elt, owner);
}
procedure {:yields} {:phase 2} Yield12()
|