From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Mon, 6 Jun 2016 23:14:18 -0600
Subject: Merging complete.  Everything looks good *crosses fingers*

---
 Test/civl/bar.bpl | 57 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)
 create mode 100644 Test/civl/bar.bpl

(limited to 'Test/civl/bar.bpl')

diff --git a/Test/civl/bar.bpl b/Test/civl/bar.bpl
new file mode 100644
index 00000000..b5068edd
--- /dev/null
+++ b/Test/civl/bar.bpl
@@ -0,0 +1,57 @@
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0,1} g:int;
+
+procedure {:yields} {:layer 1} PB()
+{
+  yield;
+  call Incr();
+  yield;
+}
+
+procedure {:yields} {:layer 0,1} Incr();
+ensures {:atomic}
+|{A:
+  g := g + 1; return true;
+}|;
+
+procedure {:yields} {:layer 0,1} Set(v: int);
+ensures {:atomic}
+|{A:
+  g := v; return true;
+}|;
+
+procedure {:yields} {:layer 1} PC()
+ensures {:layer 1} g == old(g);
+{
+  yield;
+  assert {:layer 1} g == old(g);
+}
+
+procedure {:yields} {:layer 1} PE()
+{
+  call PC();
+}
+
+procedure {:yields} {:layer 1} PD()
+{
+  yield;
+  call Set(3);
+  call PC();
+  assert {:layer 1} g == 3;
+}
+
+procedure {:yields} {:layer 1} Main2()
+{
+  yield;
+  while (*)
+  {
+    async call PB();
+    yield;
+    async call PE();
+    yield;
+    async call PD();
+    yield;
+  }
+  yield;
+}
-- 
cgit v1.2.3