If they prove a check is always false, it means you have dead code or you made a mistake.

It is very very hard to write C without mistakes.

When not-actually-dead code gets removed, the consequences of many mistakes get orders of magnitudes worse.