TLC crashes with "File too large" IOException while writing MC.st file

[Nipun sehrawat <nipunse...@xxxxxxxxx>]

Hello,

I am running into TLC crashes, especially when checking for some liveness properties.  The error reported by TLC is:

TLC threw an unexpected exception.

This was probably caused by an error in the spec or model.

See the User Output or TLC Console for clues to what happened.

The exception was a java.io.IOException

: File too large

The error occurred when TLC was evaluating the nested

expressions at the following positions:

    The error call stack is empty.

TLC threw an unexpected exception.

This was probably caused by an error in the spec or model.

See the User Output or TLC Console for clues to what happened.

The exception was a java.io.IOException

: File too large

I debugged a bit and found that TLC crashes right after MC.st file crosses 512MB in size.  I have disabled checkpoints and snapshots but that didn't help.  Any ideas how to fix/avoid these crashes?

Thanks,

Nipun