diagnostics: Explain why programs might run OOM in GenMC mode

GenMC's allocator can currently only allocate up to 4GB per thread.

Authored-by: Ralf Jung