From 64d8963508ce048d00db3766f4ca597b792c1b95 Mon Sep 17 00:00:00 2001
From: Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>
Date: Sat, 18 May 2013 21:15:20 -0700
Subject: reworked the linear and og implementation based on available
 variables theory

---
 Test/og/parallel4.bpl | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'Test/og/parallel4.bpl')

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;
-- 
cgit v1.2.3