Why is one often requiring space constructibility in Savitch's theorem?

When Savitch's famous theorem is stated, one often sees the requirement that $S(n)$ be space constructible (interestingly, it is omitted in Wikipedia). My simple question is: Why do we need this? I understand the requirement for $S(n)$ being in $\Omega(\log n)$, which is clear from the proof. But no proof I have seen so far explicitly uses that $S(n)$ is space constructable.

My explanation: in order to call the procedure REACH (or PATH or whatever you like to call it), the last parameter needs to be "spelled out", and in order not to leave our space bounds of S(n) for one call, we must not need more than $S(n)$ space to write it down.

This is elaborated nicely in Dexter Kozen's Theory of Computation textbook, in chapter 2.

Savitch's Theorem (Theorem 1 in his paper) says: if $S(n) \ge \log n$, then $\text{NSPACE}(S(n)) \subseteq \text{DSPACE}(S(n)^2)$. Space-constructibility often seems to be assumed in a proof, but this requirement can be removed by restarting the search with a fixed space bound that is allowed to increase with each attempt.

The confusion perhaps arises because the original Savitch paper is largely about investigating whether $\text{NSPACE}(S(n)) \not\subseteq \text{DSPACE}(S(n))$. It therefore spends a lot of effort on space-constructible functions, due to the following observation from the paper:


It is natural to ask if there is any storage function whose deterministic and nondeterministic complexity classes are equal. The answer was given by Manuel Blum and is "yes". Blum showed that there are arbitrarily large storage functions L(n) such that a set is accepted within deterministic storage L(n) if, and only if, it is accepted
within nondeterministic storage L(n). These functions L(n) are not, however, "well-behaved" and Theorem 3 does not apply to them.

(Here "well-behaved" refers to the space-constructible functions, called measurable by Savitch.)

StackExchange Computer Science Q#11168, answer score: 8