Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation

Watch a 15-minute conference presentation introducing Aries, a novel technique for validating SMT solver rewrite systems through targeted rewrite space exploration. Learn how researchers from Nanjing University developed a practical validation tool that addresses the largely unexplored area of rewrite system validation in Satisfiability Modulo Theories (SMT) solvers. Discover the two-phase approach: mimetic mutation that actively reshapes input formulas to provoke diverse rewrite opportunities, followed by deductive rewriting using generative equality saturation to explore rewrite space and produce semantically equivalent mutants for validation purposes. Examine the experimental results demonstrating Aries's effectiveness on leading SMT solvers Z3 and cvc5, where it successfully identified 27 new issues with 22 confirmed or fixed by developers, primarily involving rewrite systems. Understand the significance of this work in improving the robustness and reliability of SMT solvers, which are crucial components in program analysis and automated reasoning applications, presented at the OOPSLA2 2025 conference with accompanying research artifacts available for replication.