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

Added cli options for reinitialization and internal action loop verification; added list of internal infinite loops in output