Merge branch 'dfsg_free'

1 files changed, 19 insertions, 0 deletions

diff --git a/Test/civl/chris5.bpl b/Test/civl/chris5.bpl
new file mode 100644
index 00000000..23ebe424
--- /dev/null
+++ b/Test/civl/chris5.bpl
@@ -0,0 +1,19 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var{:layer 1,1} g:int;
+
+procedure{:layer 1} P(x:int)
+  requires {:layer 1} x == 0;
+{
+}
+
+procedure{:yields}{:layer 1,2} Y(x:int)
+  ensures{:atomic} |{ A: return true; }|;
+{
+  yield;
+  
+  call P(x);
+  assert{:layer 1} x == 0;
+
+  yield;
+}