Choose-free Heuristic: With the choose-free heuristic, the model checker first searches the part of state space that does not contain any non-deterministic choices. This is particularly useful when abstractions based on over-approximations of the system behavior are used for reducing the size of the state space to allow more efficient model checking. A variation of this heuristic gives the best heuristic values to the states with the fewest nondeterministic choice statements enabled, allowing the choose-free state space to be searched first but continuing to the rest of the state space otherwise (this also allows choose-free to be combined with other heuristics).