The widening operator causes termination issues

[Maxime-Derri]

I encountered a case where the widening operator returns an empty abstract state (bottom), leading the verifier to loop indefinitely.

A test is provided ex_widening.zip:

• section: xdp
• function: crossing_64_bit_signed_boundary_1

Note that in previous versions, probably before the introduction of the separated type domain, the test was accepted.

[Maxime-Derri]

For debugging, you can add a print before and after the extrapolate() function to check that the invariant is bottom.

[elazarg]

Do you know if this is distinct from #783?

[Maxime-Derri]

Hmm I didn't tested this issue

[Maxime-Derri]

In the issue you mentionned, Alan Jowett said that the verifier hang for 10min and assertions where checked after the invariant computation meaning that the verifier found an invariant? Here the abstract state is bottom.