CProver analyses permits idle action even if transition(s) could be performed.
Due to injecting nodeterministic choice behavior for which traversable transition to perform, CBMC might find traces which perform a states idle action instead of possible outgoing transitions.
(from redmine: issue id 1599, created on 2013-08-08, closed on 2013-09-01)