Oracle-Guided SMT Solver Validation via Synthesizing Diverse Formulas with Multiple Assignments

Ensuring the correctness of Satisfiability Modulo Theory (SMT) solvers is critical, as undetected bugs in these solvers can lead to incorrect results in the many applications that depend on them. However, automatically testing SMT solvers remains challenging, largely due to the absence of reliable test oracles. To address this challenge, recent work has explored assignment-aided reassembling techniques, such as STORM and Diver, which generate satisfiable test formulas by recombining parts of existing formulas based on satisfying assignments. While these techniques have demonstrated effectiveness in practice, opportunities remain to further enhance the approaches. For example, they cannot generate unsatisfiable test formulas, which may restrict their ability to detect certain classes of soundness bugs. Therefore, this article introduces a novel fuzzing technique that enhances these methods building on the idea of assignment-aided reassembling. Specifically, our approach utilizes multiple satisfying assignments derived from seed formulas to guide the reassembly of sub-formulas, exploring divergent logical paths to synthesize new test cases. To further increase test diversity, we incorporate formula snippets generated from scratch. In addition, we extend the approach to support the generation of unsatisfiable test formulas by using unsatisfiable cores extracted from unsatisfiable seed formulas. We have implemented this approach in a practical tool, Octopus , designed to test SMT solvers more comprehensively. We applied Octopus to leading SMT solvers, including Z3 and cvc5, and reported 13 bugs to their issue trackers. Among these, 11 bugs have been confirmed by the developers, and nine have been fixed. Our experiments also show that Octopus achieves higher code coverage compared to existing SMT fuzzers.