reworked the linear and og implementation based on available variables theory

1 files changed, 5 insertions, 1 deletions

diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
index a5b2768f..8f78fdc5 100644
--- a/Test/og/parallel4.bpl
+++ b/Test/og/parallel4.bpl
@@ -1,15 +1,19 @@
 var a:int;

 

+procedure Allocate() returns ({:linear "tid"} xls: int);

+

 procedure {:entrypoint} main() 

 {

   var {:linear "tid"} i: int;

   var {:linear "tid"} j: int;

+  call i := Allocate();

+  call j := Allocate();

   call i := t(i) | j := t(j);

 }

 

 procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 {

-  assume i == i';

+  i := i';

   call Yield();

   assert a == old(a);

   a := a + 1;