Fix incorrect verdict for prodbin-ll_unwindbound50.yml and prodbin-ll_unwindbound100.yml

The two benchmarks nla-digbench-scaling/prodbin-ll_unwindbound50.yml and nla-digbench-scaling/prodbin-ll_unwindbound100.yml have an incorrect verdict. They should be labeled as correct. There is why:

• The first assertion z + x * y == (long long) a * b is a loop invariant, so it can never be violated.
• Therefore a possible counterexample has to violate the assertion __VERIFIER_assert(z == (long long) a * b); after the loop.
• To violate this assertion we cannot execute the break, since the loop invariant together with the if-condition implies the assertion.
  • Therefore we need to execute the loop completely, i.e. N times (given in the filename).
  • Therefore y must always be greater than zero.
• Since y is divided by two in every iteration (the subtraction is irrelevant), it has the value \lfloor b / 2^i \rfloor in the i-th iteration.
• This means that \lfloor b / 2^{N-1} \rfloor \gt 0 (y is allowed to be 0 only in the very last iteration) and therefore b \geq 2^{N-1}.
• On the other hand b is an int (32bit), therefore b \leq 2^{31}-1.
• This concludes that there only exists a counterexample for N \leq 31, i.e. the program is correct for N \gt 31.