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. Recent approaches based on Large Language Models (LLMs) show promise in exploring advanced solver capabilities, but two obstacles remain: nearly half of the generated formulas are syntactically invalid, and iterative interactions with LLMs introduce substantial computational overhead. In this study, we present Once4All, a novel LLM-assisted fuzzing framework that addresses both issues by shifting from direct formula generation to the synthesis of generators for reusable terms (i.e., logical expressions). Specifically, Once4All uses LLMs to (1) automatically extract context-free grammars (CFGs) for SMT theories, including solver-specific extensions, from documentation, and (2) synthesize composable Boolean term generators that adhere to these grammars. During fuzzing, Once4All populates structural skeletons derived from existing formulas with the terms iteratively produced by the LLM-synthesized generators. This design ensures syntactic validity while promoting semantic diversity. Notably, Once4All requires only one-time LLM interaction investment, dramatically reducing runtime cost. We evaluated Once4All on two leading SMT solvers: Z3 and cvc5. Our experiments show that Once4All has identified 43 confirmed bugs, 40 of which have already been fixed by developers.

翻译：可满足性模理论（SMT）求解器是现代系统和编程语言研究的基石，为符号执行、自动验证等任务提供基础支撑。由于这些求解器处于关键路径上，其正确性至关重要，而高质量的测试公式是发现缺陷的关键。然而，尽管先前的测试技术在早期求解器版本上表现良好，但难以跟上快速演化的特性。基于大型语言模型（LLM）的最新方法在探索高级求解器能力方面展现出潜力，但仍存在两大障碍：近半数生成的公式存在语法无效问题，且与LLM的迭代交互会引入大量计算开销。本研究提出Once4All——一种新型LLM辅助模糊测试框架，通过将直接生成公式转变为合成可复用项（即逻辑表达式）的生成器，同时解决上述两个问题。具体而言，Once4All利用LLM实现：（1）从文档中自动提取面向SMT理论（包括求解器特有扩展）的上下文无关文法；（2）合成遵循这些文法的可组合布尔项生成器。在模糊测试过程中，Once4All利用LLM合成生成器迭代产生的项，填充由现有公式推导出的结构骨架。该设计在确保语法有效性的同时促进语义多样性。值得注意的是，Once4All仅需一次性与LLM交互投入，大幅降低运行时开销。我们在两个主流SMT求解器——Z3和cvc5上对Once4All进行了评估。实验表明，Once4All已发现43个经确认的缺陷，其中40个已被开发者修复。