  Theorem provers has been used extensively in software engineering for
software testing or verification. However, software is now so large and complex
that additional architecture is needed to guide theorem provers as they try to
generate test suites. The SNAP test suite generator (introduced in this paper)
combines the Z3 theorem prover with the following tactic: cluster some
candidate tests, then search for valid tests by proposing small mutations to
the cluster centroids. This technique effectively removes repeated structures
in the tests since many repeated structures can be replaced with one centroid.
In practice, SNAP is remarkably effective. For 27 real-world programs with up
to half a million variables, SNAP found test suites which were 10 to 750
smaller times than those found by the prior state-of-the-art. Also, SNAP ran
orders of magnitude faster and (unlike prior work) generated 100% valid tests.
