Fixed bug in handling of break statements

1 files changed, 17 insertions, 0 deletions

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);