made some fixes

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: