一句话：提出 Aries，用拟态变异与生成式等式饱和探索 SMT 重写空间，验证重写系统并发现真实缺陷。
SMT 求解器广泛用于程序分析等自动推理任务，其重写系统负责简化与变换公式，对求解性能至关重要，但重写系统验证长期缺乏专门测试技术。本文提出 Aries：首先采用拟态变异，针对性地重塑输入公式，使其匹配已知重写模式，从而触发并多样化重写机会；随后利用演绎重写，借助生成式等式饱和探索重写空间，并生成语义等价的变异体用于验证。作者实现工具并在 Z3、cvc5 等主流求解器上评估，发现 27 个新问题，其中 22 个已被确认或修复，且多数涉及重写系统，表明该方法能有效探索重写空间并暴露真实缺陷。
Satisfiability Modulo Theories (SMT) solvers are widely used for program analysis and other applications that require automated reasoning. Rewrite systems, as crucial integral components of SMT solvers, are responsible for simplifying and transforming formulas to optimize the solving process. The effectiveness of an SMT solver heavily depends on the robustness of its rewrite system, making its validation crucial. Despite ongoing advancements in SMT solver testing, rewrite system validation remains largely unexplored. Our empirical analysis reveals that developers invest significant effort in ensuring the correctness and reliability of rewrite systems. However, existing testing techniques do not adequately address this aspect. In this paper, we introduce Aries , a novel technique designed to validate SMT solver rewrite systems. First, Aries employs mimetic mutation , a targeted strategy that actively reshapes input formulas to provoke and diversify rewrite opportunities. By aligning mutated terms with known rewrite patterns, Aries can conduct a thorough exploration of the rewrite space in the following phase. Second, Aries utilizes deductive rewriting , leveraging generative equality saturation to effectively explore rewrite space and produce semantically equivalent mutants for the purpose of validation. We implemented Aries as a practical validation tool and evaluated it on leading SMT solvers, including Z3 and cvc5. Our experiments demonstrate that Aries effectively identifies bugs, with 27 new issues detected, of which 22 have been confirmed or fixed by developers. Most of these issues involve the rewrite systems, highlighting Aries ’s strength in exploring the rewrite space.
@article{paperbot2974,
title = {Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation},
author = {Maolin Sun and Yibiao Yang and Jiangchang Wu and Yuming Zhou},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763093}
}