diff options
| -rw-r--r-- | Test/og/lock.bpl | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl index c00560fe..69aba91e 100644 --- a/Test/og/lock.bpl +++ b/Test/og/lock.bpl @@ -20,20 +20,22 @@ procedure {:yields} {:stable} Customer() call Leave();
}
+
+ yield;
}
procedure {:yields} Enter()
ensures {:atomic 1} |{ A: assume !b; b := true; return true; }|;
{
var status: bool;
+ yield;
L:
- yield;
call status := CAS(false, true);
+ yield;
goto A, B;
A:
assume status;
- yield;
return;
B:
|