Fix loops with non-deterministic bound

Instead of adding a "while (1)", I should have added a
"while (__VERIFIER_nondet_bool())" whenever the loop condition
was empty.

Author: MartinSpiessl

c/loop-zilu/benchmark01_conjunctive.c

@@ -28,7 +28,7 @@ int main() {
   int y = __VERIFIER_nondet_int();
 
   if (!(x==1 && y==1)) return 0;
-  while (1) {
+  while (__VERIFIER_nondet_bool()) {
     x=x+y;
     y=x;
   }

c/loop-zilu/benchmark03_linear.c

@@ -33,7 +33,7 @@ int main() {
   _Bool flag = __VERIFIER_nondet_bool();
   x = 0; y = 0;
   if (!(i==0 && j==0)) return 0;
-  while (1) {
+  while (__VERIFIER_nondet_bool()) {
     x++;
     y++;
     i+=x;

c/loop-zilu/benchmark06_conjunctive.c

@@ -31,7 +31,7 @@ int main() {
   int k = __VERIFIER_nondet_int();
   j=0;
   if (!(x+y==k)) return 0;
-  while (1) {
+  while (__VERIFIER_nondet_bool()) {
     if(j==i) {x++;y--;} else {y++;x--;} j++;
   }
   __VERIFIER_assert(x+y==k);

c/loop-zilu/benchmark12_linear.c

@@ -29,7 +29,7 @@ int main() {
   int t = __VERIFIER_nondet_int();
 
   if (!(x!=y && y==t)) return 0;
-  while (1) {
+  while (__VERIFIER_nondet_bool()) {
     if(x>0) y=y+x;
   }
   __VERIFIER_assert(y>=t);

c/loop-zilu/benchmark16_conjunctive.c

@@ -24,7 +24,7 @@ int main() {
   int i = __VERIFIER_nondet_int();
   int k = __VERIFIER_nondet_int();
   if (!(0 <= k && k <= 1 && i == 1)) return 0;
-  while (1) {
+  while (__VERIFIER_nondet_bool()) {
     i = i + 1;
     k = k - 1;
   }

c/loop-zilu/benchmark22_conjunctive.c

@@ -24,7 +24,7 @@ int main() {
   int x = __VERIFIER_nondet_int();
   int y = __VERIFIER_nondet_int();
   if (!(x==1 && y==0)) return 0;
-  while (1) {
+  while (__VERIFIER_nondet_bool()) {
     x=x+y;
     y++;
   }

c/loop-zilu/benchmark30_conjunctive.c

@@ -24,7 +24,7 @@ int main() {
   int x = __VERIFIER_nondet_int();
   int y = __VERIFIER_nondet_int();
   if (!(y == x)) return 0;
-  while (1) {
+  while (__VERIFIER_nondet_bool()) {
     x++;
     y++;
   }

c/loop-zilu/benchmark32_linear.c

@@ -27,7 +27,7 @@ int main() {
   int x = __VERIFIER_nondet_int();
 
   if (!(x==1 || x==2)) return 0;
-  while (1) {
+  while (__VERIFIER_nondet_bool()) {
     if(x==1) x=2;
     else if (x==2) x=1;
   }

c/loop-zilu/benchmark36_conjunctive.c

@@ -25,7 +25,7 @@ int main() {
   int x = __VERIFIER_nondet_int();
   int y = __VERIFIER_nondet_int();
   if (!(x == y && y == 0)) return 0;
-  while (1) {
+  while (__VERIFIER_nondet_bool()) {
     x++;y++;
   }
   __VERIFIER_assert(x == y && x >= 0);

c/loop-zilu/benchmark38_conjunctive.c

@@ -25,7 +25,7 @@ int main() {
   int x = __VERIFIER_nondet_int();
   int y = __VERIFIER_nondet_int();
   if (!(x == y && y == 0)) return 0;
-  while (1) {
+  while (__VERIFIER_nondet_bool()) {
     x+=4;y++;
   }
   __VERIFIER_assert(x == 4*y && x >= 0);