Somewhat related: a similar program [1] is part of the benchmarks used in the annual Software Verification Competition (SV-COMP). Specifically, in the termination analysis suite.

Maybe they secretly hope that some tool, someday, will spit out a correct proof? :)

[1] https://github.com/sosy-lab/sv-benchmarks/blob/svcomp17/c/te...