Resolve "Wrong verdict for ite-tasks"

By turning

SORT_4 state_6;
for (unsigned char i = 0; i < (1 << 8); ++i) state_6[i] = __VERIFIER_nondet_uint() & mask_SORT_2;

into

for (unsigned char i = 0; ; ++i) {
  state_6[i] = __VERIFIER_nondet_uint() & mask_SORT_2;
  if (i == mask_SORT_3) break;
}

we avoid creating infinite loops in the translated task. See this thread.

Closes #35 (closed)