diff options
Diffstat (limited to 'Test/doomed')
| -rw-r--r-- | Test/doomed/doomed.bpl | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/Test/doomed/doomed.bpl b/Test/doomed/doomed.bpl index 741a54c5..9029383d 100644 --- a/Test/doomed/doomed.bpl +++ b/Test/doomed/doomed.bpl @@ -36,6 +36,22 @@ procedure evilloop(x:int) }
}
+procedure evilnested(x:int)
+{
+ var i : int;
+ var j : int;
+ i:=x-1;
+ j:=1;
+ while (i>=0) {
+ while (j<=i) {
+ assert j<x;
+ j := j+1;
+ }
+ i := i - 1;
+ }
+}
+
+
procedure evilpath(x:int)
{
var y : int;
|