`RangeError: Invalid string length` error when running large simulations with `--mbt`

[crodriguezvega]

Running quint run with --mbt and a large number of samples and steps (--max-samples 2000 --n-traces 2000 --max-steps 500) causes a RangeError: Invalid string length crash in Node.js after all samples complete successfully.

Environment

• quint: 0.32.0
• Node.js: v25.8.2
• OS: macOS Darwin 24.2.0

Observed behavior

Quint completes all 2000/2000 samples successfully, then crashes:

Running... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 100% | ETA: 0s | 2000/2000 samples | 258 2
        this[kLine_buffer] += string;
                              ^

RangeError: Invalid string length
    at [_normalWrite] [as _normalWrite] (node:internal/readline/interface:652:31)
    at Socket.ondata (node:internal/readline/interface:263:23)
    at Socket.emit (node:events:508:28)
    at addChunk (node:internal/streams/readable:563:12)
    at readableAddChunkPushByteMode (node:internal/streams/readable:514:3)
    at Readable.push (node:internal/streams/readable:394:5)
    at Pipe.onStreamRead (node:internal/stream_base_commons:189:23)

Node.js v25.8.2

Exit code is non-zero.

Expected behavior

The command completes successfully (exit code 0) since all 2000 samples finished without error. At minimum, the error message should clearly indicate that the output buffer limit was exceeded rather than crashing with an internal Node.js error.

Root cause hypothesis

With --mbt and a large number of samples/steps, Quint accumulates output before flushing. At this scale the accumulated string hits V8's hard limit on maximum string length, causing RangeError: Invalid string length to be thrown.