diff options
| author |  qadeer <unknown> | 2014-05-04 21:17:12 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-05-04 21:17:12 -0700 |
| commit | 28d4e2ad2598ff377f121ff2a2a9b0794f386110 (patch) | |
| tree | 5bd85a8938154aabf3eb80751c1f9dd54f980c31 /Test/og/multiset.bpl | |
| parent | 36e016acf963b7c19d59640b11b4a40f2072943e (diff) | |
second checkpoint
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()
|