Exponential bounded model-checking for leadsTo pragmas to prove liveness properties as soon as available. It allows to prove false properties in infinite graphs. Added stop and resume state space exploration methods