Once4All: Skeleton-Guided SMT Solver Fuzzing with LLM-Synthesized Generators

ArXi:2508.20340v3 Announce Type: replace-cross Satisfiability Modulo Theory (SMT) solvers are foundational to modern systems and programming languages research, providing the foundation for tasks like symbolic execution and automated verification. Because these solvers sit on the critical path, their correctness is essential, and high-quality test formulas are key to uncovering bugs. However, while prior testing techniques performed well on earlier solver versions, they struggle to keep pace with rapidly evolving features.