From 98b4265f81494493a7501e81aea19ab4aa0e156c Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Thu, 2 Jan 2014 21:14:14 -0800
Subject: some more fixes

---
 Test/og/DeviceCache.bpl | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'Test/og')

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index 6bff421c..1c2efdbb 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -118,6 +118,7 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsiz
     var j: int;
     tid := tid';
 
+    par tid := YieldToWriteCache(tid);
     call tid, j := ReadCurrsize(tid);
     while (j < index)
     invariant {:phase 1} ghostLock == tid && currsize <= j && tid == tid';
@@ -141,6 +142,7 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize);
     var j: int;
     tid := tid';
 
+    par tid := YieldToReadCache(tid);
     j := 0;
     while(j < bytesRead)
     invariant {:phase 1} 0 <= j;
-- 
cgit v1.2.3