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

Researchers developed Once4All, an LLM-assisted fuzzing framework for testing SMT solvers that addresses syntax validity issues and computational overhead. The system found 43 confirmed bugs in leading solvers Z3 and cvc5, with 40 already fixed by developers.

• →Once4All uses LLMs to synthesize reusable term generators rather than directly generating test formulas, improving efficiency.
• →The framework automatically extracts context-free grammars from SMT solver documentation to ensure syntactic validity.
• →The system requires only one-time LLM interaction, dramatically reducing computational costs compared to iterative approaches.
• →Testing on Z3 and cvc5 solvers resulted in 43 confirmed bugs, demonstrating the framework's effectiveness.
• →The approach addresses key limitations of previous LLM-based testing methods that generated syntactically invalid formulas.