Understanding Property Violations: When a property violation is detected by the model checker, the model checker typically generates a counterexample trace. The trace points to the location where the violation was detected, but quite often what is reported is only a symptom of a bug which occurred much earlier in the execution trace. At this stage, you need to localize the root cause of the property violation.
Quite often one bug may cause the code to fail in many different ways. Selection of suitable search strategies allows us to find the shortest paths to the problem, thereby minimizing the distance between the detected property violation and the root cause.
One common technique for localizing the root cause of the violation is to let the model checker generate multiple counterexamples, and use these counterexamples collectively to find the root cause.