1 files changed, 14 insertions, 0 deletions
diff --git a/Test/civl/chris7.bpl b/Test/civl/chris7.bpl
new file mode 100644
index 00000000..a8fd25d3
--- /dev/null
+++ b/Test/civl/chris7.bpl
@@ -0,0 +1,14 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure{:layer 1}{:extern} P() returns(i:int);
+
+procedure{:yields}{:layer 1,1}{:extern} Y({:layer 1}x:int);
+
+procedure{:yields}{:layer 1,2} A({:layer 1}y:int)
+  ensures {:atomic} |{ A: return true; }|;
+{
+  var{:layer 1} tmp:int;
+  call Y(y);
+  call tmp := P();
+  call Y(tmp);
+}