diff options
Diffstat (limited to 'Test/test2/Structured.bpl')
| -rw-r--r-- | Test/test2/Structured.bpl | 17 |
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);
|