blob: d239802db232b846711c263c6dede83b1b9d2bf6 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
|
namespace;
include rt;
// a loop proof only holds while the body leaves the index alone: here the body
// moves i back below 0 once, so t[i] keeps its check and the access faults
int main() {
int[4] t = {}; int s = 0, once = 1;
for (int i = 0; i < 4; i++) { s = s + t[i]; if (once) { once = 0; i = -3000; } }
rt.put_n(s); rt.put_c(10);
return 0;
}
|
