Why OK?
	• This technique is unsound: it may not report counterexamples when they exist • However – The approach is very clear about reporting only counterexamples in the selected bound – If it does find counterexamples, they help identify problem early – The search space, while bounded, is still large – There is an unproven hypothesis that most, or at least many, problems arise in small state spaces (“small scope hypothesis”)