added more examples

2 files changed, 20 insertions, 1 deletions

diff --git a/Test/og/ghost.bpl b/Test/og/ghost.bpl
index ef40a232..74d16acf 100644
--- a/Test/og/ghost.bpl
+++ b/Test/og/ghost.bpl
@@ -25,3 +25,22 @@ ensures {:right} |{ A: x := x + 2; return true; }|;
   yield;
 }
 
+procedure ghost_0() returns (z: int)
+ensures z == x;
+{
+  z := x;
+}
+
+procedure {:yields} {:layer 1,2} Incr2_0() 
+ensures {:right} |{ A: x := x + 2; return true; }|;
+{
+  var {:ghost} a: int;
+  var {:ghost} b: int;
+
+  yield;
+  call a := ghost_0();
+  par Incr() | Incr();
+  call b := ghost_0();
+  assert {:layer 1} b == a + 2;
+  yield;
+}
diff --git a/Test/og/ghost.bpl.expect b/Test/og/ghost.bpl.expect
index 41374b00..9823d44a 100644
--- a/Test/og/ghost.bpl.expect
+++ b/Test/og/ghost.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 6 verified, 0 errors