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

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/termination-crafted/Collatz_unknown-termination_false-no-overflow.c https://github.com/sosy-lab/sv-benchmarks/blob/svcomp17/c/te...