1 files changed, 4 insertions, 4 deletions
diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl
index 0b250b6d..4e4e6dec 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -23,7 +23,7 @@ procedure {:yields} {:stable} Customer()
 }
 
 procedure {:yields} Enter() 
-ensures {:atomic 0} |{ A: assume !b; b := true; return true; }|;
+ensures {:atomic 1} |{ A: assume !b; b := true; return true; }|;
 {
     var status: bool;
     L: 
@@ -41,12 +41,12 @@ ensures {:atomic 0} |{ A: assume !b; b := true; return true; }|;
 	goto L;
 }
 
-procedure CAS(prev: bool, next: bool) returns (status: bool);
-ensures {:atomic -1} |{ 
+procedure {:yields} CAS(prev: bool, next: bool) returns (status: bool);
+ensures {:atomic 0} |{ 
 A: goto B, C; 
 B: assume b == prev; b := next; status := true; return true; 
 C: status := false; return true; 
 }|;
 
 procedure {:yields} Leave();
-ensures {:atomic -1} |{ A: b := false; return true; }|;
+ensures {:atomic 0} |{ A: b := false; return true; }|;