The key difference between a property-specific heuristic and a structural heuristic can be seen in the dining philosophers’ example where we search for the well-known deadlock scenario. When increasing the number of philosophers high enough it becomes impossible for an explicit-state model checker to try all the possible combinations of actions to get to the deadlock, and heuristics (or luck) are required. A property-specific heuristic applicable here is to try and maximize the number of blocked threads, since if all threads are blocked we have a deadlock (most-blocked heuristic). Whereas a structural heuristic may be to observe that we are dealing here with a highly concurrent program—hence it may be argued that any error in it may well be related to an unexpected interleaving —we use the heuristic to favor increased interleaving during the search (interleaving heuristic). Although experimental results are by no means conclusive, it is still worth noting that for the dining philosophers’ example the structural heuristic performs much better than the property-specific heuristic. Another interesting observation is that turning the state storage off with the interleaving heuristic mentioned above for both the dining philosophers’ example and the Remote Agent example does not seem to change the results significantly—we found only minor variations in the length of counterexamples and number of states searched. In contrast, turning the state storage off for the most-blocked heuristic seems to cause previously successful searches to become unsuccessful.