Do bounded-visit nondeterministic linear bounded automata recognize only regular languages?
By a nondeterministic linear bounded automaton (nLBA) I mean a single-tape nondeterministic Turing machine where the input comes "padded" with endmarkers on both ends which can never be overwritten, and so that the head can never move out of the input region, "outside" the endmarkers.
The LBA is bounded-visit if there is a number $k$ such that all runs on all inputs terminate and visit every cell of the tape at most $k$ times.
Does such a machine recognize only regular languages? Hennie's result seems to say this only for deterministic machines, if I'm reading it right. Does the result hold for nondeterministic machines too? If yes, a reference would be appreciated.