diff --git a/tests/regression/77-mem-oob/10-oob-two-loops.c b/tests/regression/77-mem-oob/10-oob-two-loops.c index 5208da5a0b..303aac242e 100644 --- a/tests/regression/77-mem-oob/10-oob-two-loops.c +++ b/tests/regression/77-mem-oob/10-oob-two-loops.c @@ -1,15 +1,17 @@ // PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info --set sem.int.signed_overflow assume_none +#include + int main() { int *p = malloc(1048 * sizeof(int)); for (int i = 0; i < 1048; ++i) { - p[i] = __VERIFIER_nondet_int(); //NOWARN + p[i] = rand(); //NOWARN } int *q = p; while (*q >= 0 && q < p + 1048 * sizeof(int)) { //WARN - if (__VERIFIER_nondet_int()) { + if (rand()) { q++; } else { (*q)--; //WARN