  The regression test suite, a key resource for managing program evolution,
needs to achieve 100% coverage, or very close, to be useful. Devising a test
suite manually is unacceptably tedious, but existing automated methods are
often inefficient. The method described in this article, ``Seeding
Contradiction'', inserts incorrect instructions into every basic block of the
program, enabling an SMT-based Hoare-style prover to generate a counterexample
for every branch of the program and, from the collection of all such
counterexamples, a test suite. The method is static, works fast, and achieves
excellent coverage.
