Java Stack Overflow with bounded forall (\A i \in 1..10000: TRUE)

The spec below with InitSOF or NextSOF causes TLC to run into a stack overflow (SOF). This goes at least back to TLC 2.05 as of 23 July 2013 (Toolbox 1.4.8). Init2, and Next2 do not exhibit the SOF. The workaround is thus to assign all variables a value first. In other words, to push the all quantifier down as done in Init2 or Next2.

------ MODULE JSO ------
EXTENDS Integers

VARIABLES x
S == 1..10000

InitSOF == /\ \A j \in S: TRUE
           /\ x = 1

Init2 == /\ x = 1
         /\ \A j \in S: TRUE

NextSOF ==  /\ \A j \in S: TRUE
            /\ x' = 1

Next2 == /\ x' = 1
         /\ \A j \in S: TRUE
====================

NextSOF is interpreted by recursively following the (linked) list of context instances one created for each element in the set: https://github.com/tlaplus/tlaplus/blob/dc4c3bc4570591599609b9b705f806f138a8c5b1/tlatools/src/tlc2/tool/Tool.java#L1000-L1016

Reversing the order of init or next prevents the SOF because Tool stops recursive evaluation when all variable values are assigned (thus adding one or more conjuncts to e.g. Init2 will again result in SOF): https://github.com/tlaplus/tlaplus/blob/dc4c3bc4570591599609b9b705f806f138a8c5b1/tlatools/src/tlc2/tool/Tool.java#L831-L869

Next2 are interpreted non-recursively a different chunk of code: https://github.com/tlaplus/tlaplus/blob/dc4c3bc4570591599609b9b705f806f138a8c5b1/tlatools/src/tlc2/tool/Tool.java#L1686-L1700

Note that the modified spec below also does not run into the stack overflow. This is obvious as ASSUMEs do not generate states.

------ MODULE JSO ------
EXTENDS Integers

ASSUME(\A j \in 1..10000: 1 > 0)
====================

Reproduce the JSO specification in TLC, then read the referenced evaluation paths in tlatools/src/tlc2/tool/Tool.java around lines 831-869, 1000-1016, and 1686-1700. Compare InitSOF and NextSOF with Init2 and Next2; done means the bounded forall cases no longer cause a stack overflow while retaining correct state evaluation.