1 files changed, 2 insertions, 2 deletions
diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index 413db4ca..ede0a31e 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -87,7 +87,7 @@ ensures 0 <= bytesRead && bytesRead <= size;
     }
 
 READ_DEVICE:
-    call Skip() | tid := YieldToWriteCache(tid);
+    par Skip() | tid := YieldToWriteCache(tid);
     call tid := WriteCache(tid, start + size);
     call tid := acquire(tid);
     call tid, tmp := ReadNewsize(tid);
@@ -95,7 +95,7 @@ READ_DEVICE:
     call tid := release(tid);
 
 COPY_TO_BUFFER:
-    call Skip() | YieldToReadCache();
+    par Skip() | YieldToReadCache();
     call ReadCache(start, bytesRead);
 }