From bbe5109c4ed1b1d1f48b8208e1bcb4fda0513c59 Mon Sep 17 00:00:00 2001
From: Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>
Date: Tue, 12 Feb 2013 11:17:29 -0800
Subject: fixed another bug reported by ChrisHaw Added an answer file

---
 Test/og/Answer | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 Test/og/Answer

(limited to 'Test/og/Answer')

diff --git a/Test/og/Answer b/Test/og/Answer
new file mode 100644
index 00000000..712ebfd8
--- /dev/null
+++ b/Test/og/Answer
@@ -0,0 +1,40 @@
+
+-------------------- foo.bpl --------------------
+OwickiGriesDesugared.bpl(179,4): Error BP5001: This assertion might not hold.
+Execution trace:
+    OwickiGriesDesugared.bpl(17,0): anon0
+    OwickiGriesDesugared.bpl(177,0): inline$YieldChecker_PC$0$L1
+
+Boogie program verifier finished with 3 verified, 1 error
+
+-------------------- bar.bpl --------------------
+OwickiGriesDesugared.bpl(171,4): Error BP5001: This assertion might not hold.
+Execution trace:
+    OwickiGriesDesugared.bpl(17,0): anon0
+    OwickiGriesDesugared.bpl(169,0): inline$YieldChecker_PC$0$L1
+OwickiGriesDesugared.bpl(171,4): Error BP5001: This assertion might not hold.
+Execution trace:
+    OwickiGriesDesugared.bpl(68,0): anon0
+    OwickiGriesDesugared.bpl(169,0): inline$YieldChecker_PC$0$L1
+
+Boogie program verifier finished with 2 verified, 2 errors
+
+-------------------- one.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- linear-set.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- linear-set2.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- FlanaganQadeer.bpl --------------------
+
+Boogie program verifier finished with 3 verified, 0 errors
+
+-------------------- DeviceCacheSimplified.bpl --------------------
+
+Boogie program verifier finished with 5 verified, 0 errors
-- 
cgit v1.2.3