fixes to type checking code

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; }|;