Good to know. At compile or verification time, it seems like you could get the same problem again, though? We want our compiles to finish promptly, and a slow, total predicate could hang.

Which is to say, a possibly-diverging function seems okay to use even by a verification tool, so long as it finishes quickly in practice. Having some notion of analysis-time-safe predicates seems useful but it doesn't seem to map cleanly to being able to prove termination?