From e7a15ef3363e69b24b70f0e5de5cecc56d501a2b Mon Sep 17 00:00:00 2001
From: Shaz Qadeer <qadeer@microsoft.com>
Date: Sun, 27 Sep 2015 22:46:45 -0700
Subject: fixed a small bug

---
 Test/civl/chris5.bpl.expect | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 Test/civl/chris5.bpl.expect

(limited to 'Test/civl/chris5.bpl.expect')

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
-- 
cgit v1.2.3