Generating Tests from Counterexamples