Why is the run time of an $f(n)$ space decider bounded by $2^{O(f(n))}$? In the proof of Savitch's theorem from the 3rd edition of Sipser's Intro to Theory of Computation, Sipser claims that the maximum time that an $ f(n) $ space nondeterministic Turing machine that halts on all inputs may use on any branch of its computation is $2^{O(f(n))}$. However, I don't see why such a machine couldn't run for an arbitrary (but finite) number of steps in one of its branches. For instance, consider the following linear space machine for deciding SAT: on input $\phi$ rewrite the contents of the first tape cell $2^{2^{n}}$ times, then evalaute $\phi$ on every possible truth assignment. This machine runs in linear space (since it doesn't need to visit anything beyond the second tape cell for the first part of its execution), but its run time exceeds $2^{O(n)}$.

Despite the similar titles, my question is not a duplicate of this one. The confusion in the linked question is about the constants that result from using an arbitrary alphabet. The author admits that they understand the $2^{O(f(n))}$ time bound for machines that use a binary alphabet (which is precisely what I don't get), and therefore none of the answers address my question.
Because, if you only use $f(n)$ tape cells, there are at most $|\Sigma|^{f(n)}$ possible strings you can have written on the tape, at most $f(n)$ different places the tape head could be, and at most $|Q|$ different states the Turing machine could be in.  That means there are at most $|Q|\,f(n)\,|\Sigma|^{f(n)}$ different configurations for the machine.  If the machine runs for more steps than that, it must visit the same configuration twice.

For a moment, let's pretend the machine is deterministic. If it visits the same configuration twice, it will take exactly the same sequence of steps and visit a third time, and infinitely often, so it cannot terminate.  However, we know that it does terminate for all inputs.  Therefore, it runs for at most $|Q|\,f(n)\,|\Sigma|^{f(n)}=2^{O(f(n))}$ steps.

But, actually, the machine is nondeterministic. Still, if some computation path visits the same configuration twice, we know that there is a computation path in which, by making the same nondeterministic choices again, the machine reaches the configuration a third time, and so on. Since we're told that every computation path terminates, we know that no computation path visits the same configuration twice, so we're done as in the deterministic case.