{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T09:16:06Z","timestamp":1768900566961,"version":"3.49.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>Satisfiability Modulo Theories (SMT) solvers are widely used for program analysis and other applications that require automated reasoning.  \nRewrite systems, as crucial integral components of SMT solvers, are responsible for simplifying and transforming formulas to optimize the solving process.  \nThe effectiveness of an SMT solver heavily depends on the robustness of its rewrite system, making its validation crucial.  \nDespite ongoing advancements in SMT solver testing, rewrite system validation remains largely unexplored.  \nOur empirical analysis reveals that developers invest significant effort in ensuring the correctness and reliability of rewrite systems.  \nHowever, existing testing techniques do not adequately address this aspect.  \nIn this paper, we introduce Aries, a novel technique designed to validate SMT solver rewrite systems.  \nFirst, Aries employs mimetic mutation, a targeted strategy that actively reshapes input formulas to provoke and diversify rewrite opportunities.  \nBy aligning mutated terms with known rewrite patterns, Aries can conduct a thorough exploration of the rewrite space in the following phase.  \nSecond, Aries utilizes deductive rewriting, leveraging generative equality saturation to effectively explore rewrite space and produce semantically equivalent mutants for the purpose of validation.  \nWe implemented Aries as a practical validation tool and evaluated it on leading SMT solvers, including Z3 and cvc5.  \nOur experiments demonstrate that Aries effectively identifies bugs, with 27 new issues detected, of which 22 have been confirmed or fixed by developers.  \nMost of these issues involve the rewrite systems, highlighting Aries's strength in exploring the rewrite space.<\/jats:p>","DOI":"10.1145\/3763093","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"1205-1231","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5617-2205","authenticated-orcid":false,"given":"Maolin","family":"Sun","sequence":"first","affiliation":[{"name":"Nanjing University, Nanjing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1153-2013","authenticated-orcid":false,"given":"Yibiao","family":"Yang","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9932-7315","authenticated-orcid":false,"given":"Jiangchang","family":"Wu","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4645-2526","authenticated-orcid":false,"given":"Yuming","family":"Zhou","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2024. cvc5. https:\/\/github.com\/cvc5\/cvc5"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632928"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_1_4_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2022. The satisfiability modulo theories library (SMT-LIB). http:\/\/smtlib.cs.uiowa.edu\/"},{"key":"e_1_2_1_5_1","volume-title":"Handbook of model checking","author":"Barrett Clark","unstructured":"Clark Barrett and Cesare Tinelli. 2018. Satisfiability modulo theories. In Handbook of model checking. Springer, 305\u2013343."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597208"},{"key":"e_1_2_1_7_1","unstructured":"Martin Brain. 2024. How to know the implemented rewrite rules in cvc5? https:\/\/github.com\/cvc5\/cvc5\/discussions\/10275#discussioncomment-8159588"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1670412.1670413"},{"key":"e_1_2_1_9_1","volume-title":"Engler","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings, Richard Draves and Robbert van Renesse (Eds.). USENIX Association, 209\u2013224. http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571207"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620666.3651330"},{"key":"e_1_2_1_12_1","volume-title":"TVM: An Automated End-to-End Optimizing Compiler for Deep Learning. In 13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018","author":"Chen Tianqi","year":"2018","unstructured":"Tianqi Chen, Thierry Moreau, Ziheng Jiang, Lianmin Zheng, Eddie Q. Yan, Haichen Shen, Meghan Cowan, Leyuan Wang, Yuwei Hu, Luis Ceze, Carlos Guestrin, and Arvind Krishnamurthy. 2018. TVM: An Automated End-to-End Optimizing Compiler for Deep Learning. In 13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018, Carlsbad, CA, USA, October 8-10, 2018, Andrea C. Arpaci-Dusseau and Geoff Voelker (Eds.). USENIX Association, 578\u2013594. https:\/\/www.usenix.org\/conference\/osdi18\/presentation\/chen"},{"key":"e_1_2_1_13_1","volume-title":"Metamorphic Testing: A New Approach for Generating Next Test Cases. CoRR, abs\/2002.12543","author":"Chen Tsong Yueh","year":"2020","unstructured":"Tsong Yueh Chen, S. C. Cheung, and Siu-Ming Yiu. 2020. Metamorphic Testing: A New Approach for Generating Next Test Cases. CoRR, abs\/2002.12543 (2020), arXiv:2002.12543. arxiv:2002.12543"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620665.3640392"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_16_1","volume-title":"VLSI: Systems on a Chip, IFIP TC10\/WG10.5 Tenth International Conference on Very Large Scale Integration (VLSI \u201999)","author":"Hoe James C.","year":"1999","unstructured":"James C. Hoe and Arvind. 1999. Hardware Synthesis from Term Rewriting Systems. In VLSI: Systems on a Chip, IFIP TC10\/WG10.5 Tenth International Conference on Very Large Scale Integration (VLSI \u201999), December 1-4, 1999, Lisbon, Portugal, L. Miguel Silveira, Srinivas Devadas, and Ricardo Augusto da Luz Reis (Eds.) (IFIP Conference Proceedings, Vol. 162). Kluwer, 595\u2013619."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","unstructured":"Aaron Hurst Adam Lerer Adam P. Goucher Adam Perelman Aditya Ramesh Aidan Clark AJ Ostrow Akila Welihinda Alan Hayes Alec Radford Aleksander Madry Alex Baker-Whitcomb Alex Beutel Alex Borzunov Alex Carney Alex Chow Alex Kirillov Alex Nichol Alex Paino Alex Renzin Alex Tachard Passos Alexander Kirillov Alexi Christakis Alexis Conneau Ali Kamali Allan Jabri Allison Moyer Allison Tam Amadou Crookes Amin Tootoonchian Ananya Kumar Andrea Vallone Andrej Karpathy Andrew Braunstein Andrew Cann Andrew Codispoti Andrew Galu Andrew Kondrich Andrew Tulloch Andrey Mishchenko Angela Baek Angela Jiang Antoine Pelisse Antonia Woodford Anuj Gosalia Arka Dhar Ashley Pantuliano Avi Nayak Avital Oliver Barret Zoph Behrooz Ghorbani Ben Leimberger Ben Rossen Ben Sokolowsky Ben Wang Benjamin Zweig Beth Hoover Blake Samic Bob McGrew Bobby Spero Bogo Giertler Bowen Cheng Brad Lightcap Brandon Walkin Brendan Quinn Brian Guarraci Brian Hsu Bright Kellogg Brydon Eastman Camillo Lugaresi Carroll L. Wainwright Cary Bassin Cary Hudson Casey Chu Chad Nelson Chak Li Chan Jun Shern Channing Conger Charlotte Barette Chelsea Voss Chen Ding Cheng Lu Chong Zhang Chris Beaumont Chris Hallacy Chris Koch Christian Gibson Christina Kim Christine Choi Christine McLeavey Christopher Hesse Claudia Fischer Clemens Winter Coley Czarnecki Colin Jarvis Colin Wei Constantin Koumouzelis and Dane Sherburn. 2024. GPT-4o System Card. CoRR abs\/2410.21276 (2024) https:\/\/doi.org\/10.48550\/ARXIV.2410.21276 arXiv:2410.21276. 10.48550\/ARXIV.2410.21276","DOI":"10.48550\/ARXIV.2410.21276"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_35"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE56229.2023.00088"},{"key":"e_1_2_1_20_1","volume-title":"18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024","author":"Jiang Zu-Ming","year":"2024","unstructured":"Zu-Ming Jiang and Zhendong Su. 2024. Detecting Logic Bugs in Database Engines via Equivalent Expression Transformation. In 18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024, Santa Clara, CA, USA, July 10-12, 2024, Ada Gavrilovska and Douglas B. Terry (Eds.). USENIX Association, 821\u2013835. https:\/\/www.usenix.org\/conference\/osdi24\/presentation\/jiang"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632900"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_11"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57246-3_17"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming Artificial Intelligence and Reasoning - 16th International Conference LPAR-16 Dakar Senegal April 25-May 1 2010 Revised Selected Papers Edmund M. Clarke and Andrei Voronkov (Eds.) (Lecture Notes in Computer Science Vol. 6355). Springer 348\u2013370. https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20 10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613140"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409763"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_44"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485496"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_5"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_12"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_20"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622834"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00202"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485529"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254104"},{"key":"e_1_2_1_38_1","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. 2016. Push-Button Verification of File Systems via Crash Refinement. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016, Kimberly Keeton and Timothy Roscoe (Eds.). USENIX Association, 1\u201316. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/sigurbjarnarson"},{"key":"e_1_2_1_39_1","unstructured":"SMT-COMP. 2023. The International SMT Competition. https:\/\/smt-comp.github.io\/2023\/"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00018"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","unstructured":"Maolin Sun Yibiao Yang Jiangchang Wu and Yuming Zhou. 2025. Artifact for OOPSLA\u201925 paper \"Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation\". https:\/\/doi.org\/10.5281\/zenodo.15754886 10.5281\/zenodo.15754886","DOI":"10.5281\/zenodo.15754886"},{"key":"e_1_2_1_42_1","volume-title":"Anvil: Verifying Liveness of Cluster Management Controllers. In 18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024","author":"Sun Xudong","year":"2024","unstructured":"Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu. 2024. Anvil: Verifying Liveness of Cluster Management Controllers. In 18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024, Santa Clara, CA, USA, July 10-12, 2024, Ada Gavrilovska and Douglas B. Terry (Eds.). USENIX Association, 649\u2013666. https:\/\/www.usenix.org\/conference\/osdi24\/presentation\/sun-xudong"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446707"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2023.3321381"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3514221.3526125"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689795"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428261"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00018"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3669940.3707271"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656400"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616275"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591239"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498696"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763093","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:41:28Z","timestamp":1760031688000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763093"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":56,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763093"],"URL":"https:\/\/doi.org\/10.1145\/3763093","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}