using break statement in the inner loop instead of goto

1 files changed, 3 insertions, 2 deletions

diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl
index 5d532c81..307d55c8 100644
--- a/Test/og/lock2.bpl
+++ b/Test/og/lock2.bpl
@@ -28,7 +28,7 @@ procedure {:yields} Enter()
 ensures {:atomic 1} |{ A: assume b == 0; b := 1; return true; }|;

 {

     var _old, curr: int;

-    L: 

+    while (true) { 

     	yield;

         call _old := CAS(0, 1);

 	yield;

@@ -40,9 +40,10 @@ ensures {:atomic 1} |{ A: assume b == 0; b := 1; return true; }|;
 	    call curr := Read();

 	    yield;

 	    if (curr == 0) {

-	        goto L;

+	        break;

 	    }

 	}

+    }

 }

 

 procedure {:yields} Read() returns (val: int);