The TChecker versions of the following benchmarks do not contain a label to be checked for safety:
arbiter_tree, csmacd, fddi, fischer, mutex, schedulability, sts
It is preferable that the generated benchmarks are ready to be checked immediately with TChecker, without manually adding a safety monitor.