[Qian-Cheng-nju]

WhichToSplit computes AtMaxOccupancy(ParentOf(node)) even when node is the root. The root has no parent, so this value is unspecified. If it is true, both of these CASE guards hold:

CASE node = root -> toSplit
  [] splitParent -> <<parent>> \o toSplit

TLA+ does not give the first matching arm priority. Taking the second arm can push a value outside Nodes onto toSplit, violating TypeOk. TLC normally takes the first arm and hides the overlap.

Set splitParent to FALSE at the root. Non-root splitting keeps the same condition.

I checked a 10-state witness after inserting keys 1 and 2 and starting an insertion of 3. Giving the empty parent choice the value NIL, giving keysOf[NIL] a full occupancy, and selecting the parent arm reproduces the violation. These are explicit interpretations of unspecified values, not a counterexample from TLC's default evaluation. With the fix, the same witness keeps the root on the stack and enters SPLIT_ROOT_LEAF. The existing MCbtree.cfg passes with unchanged state counts.

[lemmy]

/cc ^^ @lorin