fixed a small bug

2 files changed, 26 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;
+}
diff --git a/Test/civl/chris5.bpl.expect b/Test/civl/chris5.bpl.expect
new file mode 100644
index 00000000..32b474f5
--- /dev/null
+++ b/Test/civl/chris5.bpl.expect
@@ -0,0 +1,7 @@
+chris5.bpl(15,3): Error BP5002: A precondition for this call might not hold.
+chris5.bpl(6,3): Related location: This is the precondition that might not hold.
+Execution trace:
+    chris5.bpl(13,3): anon0
+    (0,0): anon00
+
+Boogie program verifier finished with 1 verified, 1 error