One can provide labels to pause stmts for refering to them in the LTL properties to be verified. These labels will be used in the generated code. Note that labels can only be put on pause stmts