Inconclusive Termination of rather simple float loop

[cloerkes]

Hi, I want to prove termination of the following C function:

int main()
{
  float x = 1.4E-45;

  while (x <= 3.4028233E38) {
    x *= 2.0;
  }
  
  return x;
}

I use the command ./2ls-binary --all-functions --termination ../c_examples/main.c, where 2ls-binary is of version 0.10.0 (drawn precompiled from the last SV-COMP). 2LS answers:

** Termination:
[main]: unknown
[__CPROVER_initialize]: yes
[__CPROVER__start]: unknown
VERIFICATION INCONCLUSIVE

Is there an adaption to the command that enables a succesfull termination proof in this case? I observed that termination can be proven for smaller thresholds (e.g. 8.0E37 instead of 3.4028233E38, which is the maximal finite float value). However, this behaviour is not monotonic: For the even smaller threshold 4.0E37, termination cannot be shown.

Thanks for your help in advance!

[peterschrammel]

Hm... unless I'm missing something, I can't see why the termination of this program depends on the loop bound. I would assume that it primarily depends on whether, depending on the rounding mode, rounding causes the multiplication to saturate, which should probably be detectable after 2 iterations (can it still happen later?!). If it doesn't saturate then it will eventually reach +Inf and terminate. So, I think that 2LS reporting termination when changing the bound likely indicates a bug in the tool.

[cloerkes]

Thanks for your answer!
Yes, indeed, the program terminates for every finite positive bound, regardless of the bound's exact value. Because of the doubling in each step, the updated value is the original value with the exponent increased by one - and thus strictly greater than the original value for all values greater zero. So no saturation occurs and the loop terminates.