Evaluating the use of a general-purpose benchmark suite for domain-specific SMT-solving

Benchmark suites are an important resource in validating performance requirements for software. However, generalpurpose suites may be unsuitable for domain-specific purposes, and may provide an incorrect indication of the software performance. This paper uses SMT-solvers (Satisfiability Modulo Theories) as a case-study. Taking deductive software verification as a specific application domain for SMT-solvers, we present an approach to quantifying the difference between generalpurpose and domain-specific benchmark suites. We show that workload-based clustering of benchmark programs increases the specificity of features tested by the suite compared to the inherent hierarchy of a general-purpose suite