Klever

Core and Scheduler contribute considerably to reduce the overall time of verification job solution by speculatively shrinking a memory limit for verification tasks. AFAIK, they reschedule verification tasks with CPU timeouts (indeed, too much time may be necessary, say, for the garbage collector to hit within the reduced memory limit). It looks that this is not the case for out of memory cases. For instance, you can look here (this the internally available link, please, request for rights).