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理论（包括求解器特定扩展）的上下文无关文法（CFG）；（2）合成符合这些文法的可组合布尔项生成器。在模糊测试过程中，Once4All通过LLM合成生成器迭代产生的项来填充从现有公式推导出的结构骨架。该设计在保证语法有效性的同时促进了语义多样性。值得注意的是，Once4All仅需单次LLM交互投入，从而大幅降低运行时成本。我们在两个主流SMT求解器（Z3和cvc5）上评估了Once4All。实验结果表明，该方法已发现43个已确认缺陷，其中40个已被开发者修复。