On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers

Dominik Winterer, Chengyu Zhang, Zhendong Su

We propose type-aware operator mutation, a simple, but unusually effective approach for testing SMT solvers. The key idea is to mutate operators of conforming types within the seed…