first check in

2 files changed, 33 insertions, 0 deletions

diff --git a/Test/og/par-incr.bpl b/Test/og/par-incr.bpl
new file mode 100644
index 00000000..7be8f561
--- /dev/null
+++ b/Test/og/par-incr.bpl
@@ -0,0 +1,31 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+var {:layer 0} x: int;
+
+procedure {:yields} {:layer 0,1} Incr();
+ensures {:right} |{ A: x := x + 1; return true; }|;
+
+procedure {:yields} {:layer 1,2} Incr2() 
+ensures {:right} |{ A: x := x + 2; return true; }|;
+{
+  yield;
+  par Incr() | Incr();
+  yield;
+}
+
+procedure {:yields} {:layer 1} Yield()
+{
+   yield;
+}
+
+procedure {:yields} {:layer 2,3} Incr4() 
+ensures {:atomic} |{ A: x := x + 4; return true; }|;
+{
+  yield;
+  par Incr2() | Incr2() | Yield();
+  yield;
+}
+
+
+
diff --git a/Test/og/par-incr.bpl.expect b/Test/og/par-incr.bpl.expect
new file mode 100644
index 00000000..00ddb38b
--- /dev/null
+++ b/Test/og/par-incr.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 4 verified, 0 errors