simplified yield type chcking and added treiber stack (not fully done)

1 files changed, 1 insertions, 1 deletions

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index bbae8b04..de2faaa8 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -22,12 +22,12 @@ procedure {:yields} {:phase 1} main()
     yield;

     while (*) 

     {

-        yield;

         call tid := Allocate();

         havoc val;

         async call foo(tid, val);

 	yield;

     }

+    yield;

 }

 procedure {:yields} {:phase 0,1} Lock(tid: X);

 ensures {:atomic} |{A: assume l == nil; l := tid; return true; }|;