一句话：用 LLM 一次性地合成可复用项生成器，并以结构骨架引导填充，实现语法合法且高效的 SMT 求解器模糊测试。
SMT 求解器是符号执行与自动验证等工作的基础，其正确性至关重要，但已有测试技术难以跟上求解器快速演进的新特性；基于 LLM 的方法虽能探索高级功能，却存在近半生成公式语法非法、以及反复与 LLM 交互带来高昂开销两大障碍。本文提出 Once4All，将 LLM 的用途从直接生成公式转为合成可复用项（逻辑表达式）的生成器：先用 LLM 从文档中自动抽取各 SMT 理论（含求解器特有扩展）的上下文无关文法，再合成符合这些文法的可组合布尔项生成器；模糊测试时，从已有公式导出结构骨架，并用生成器迭代产出的项填充骨架，从而在保证语法合法的同时提升语义多样性，且仅需一次性的 LLM 交互投入，大幅降低运行时开销。作者在 Z3 与 cvc5 上评估，共发现 43 个已确认缺陷，其中 40 个已被开发者修复。
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 solverspecific 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.