We present a technique to automatically derive reachability information from designs to enhance Bounded Model Checking style verification. The method is well suited for typical protocol applications where the operation is controlled by a main finite state machine (FSM) interacting with a hierarchy of sub-FSMs. The algorithm traverses the global state space of the design based on single transitions of the main finite state machine. This transition-by-transition decomposition of the state space distinguishes our approach from previous ones. The experimental results clearly show the value of the new method. In our experiments, false negatives could be completely avoided and the overall verification effort was drastically reduced.