diff options
Diffstat (limited to 'Test/aitest0/Intervals.bpl')
| -rw-r--r-- | Test/aitest0/Intervals.bpl | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl new file mode 100644 index 00000000..49d27b1c --- /dev/null +++ b/Test/aitest0/Intervals.bpl @@ -0,0 +1,19 @@ +const N: int;
+axiom 0 <= N;
+
+procedure P(K: int)
+ requires 0 <= K;
+{
+ var b: bool, x, k: int;
+
+ if (!b) {
+ b := !b;
+ }
+ x := if b then 13 else 10;
+ k := K;
+ while (k != 0) {
+ x := x + k;
+ k := k - 1;
+ }
+ assert 13 <= x;
+}
|