Limited state explosion during concurrent pragma verification. To a better predictable behaviour in the model-checker. To correct concurrent pragma results in normal mode