From d52d16b298f3c2bc2e114ef712e7664534493a1d Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 10 Feb 2014 17:16:56 -0800
Subject: Fixed bug in handling of break statements

---
 Test/test2/Answer         |  2 +-
 Test/test2/Structured.bpl | 17 +++++++++++++++++
 2 files changed, 18 insertions(+), 1 deletion(-)

(limited to 'Test/test2')

diff --git a/Test/test2/Answer b/Test/test2/Answer
index a88587e2..609cf1ed 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -237,7 +237,7 @@ Execution trace:
     Structured.bpl(308,3): anon1_Then
     Structured.bpl(309,5): A
 
-Boogie program verifier finished with 15 verified, 3 errors
+Boogie program verifier finished with 16 verified, 3 errors
 
 -------------------- Where.bpl --------------------
 Where.bpl(8,3): Error BP5001: This assertion might not hold.
diff --git a/Test/test2/Structured.bpl b/Test/test2/Structured.bpl
index 69ea2576..d5ce8cf4 100644
--- a/Test/test2/Structured.bpl
+++ b/Test/test2/Structured.bpl
@@ -325,3 +325,20 @@ procedure Q2() returns (x: int)
     }
   }
 }
+
+// There was once a bug in Boogie's handling of the following break statement.
+procedure BreakIssue(x: int) returns (curr: int)
+  ensures x == 18 || curr == 100;  // holds, because the procedure doesn't
+                                   // actually ever terminate if x != 18
+{
+  while (x != 18) { 
+    while (x != 19) {
+      call curr := Read();
+      if (curr == 0) {
+        break;
+      }
+    }
+  }
+}
+
+procedure Read() returns (val: int);
-- 
cgit v1.2.3