{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:58:20Z","timestamp":1790927900042,"version":"4.1.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>\n                    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\n                    <jats:sc>Aries<\/jats:sc>\n                    , a novel technique designed to validate SMT solver rewrite systems. First,\n                    <jats:sc>Aries<\/jats:sc>\n                    employs\n                    <jats:italic toggle=\"yes\">\n                      <jats:bold>mimetic mutation<\/jats:bold>\n                    <\/jats:italic>\n                    , a targeted strategy that actively reshapes input formulas to provoke and diversify rewrite opportunities. By aligning mutated terms with known rewrite patterns,\n                    <jats:sc>Aries<\/jats:sc>\n                    can conduct a thorough exploration of the rewrite space in the following phase. Second,\n                    <jats:sc>Aries<\/jats:sc>\n                    utilizes\n                    <jats:italic toggle=\"yes\">\n                      <jats:bold>deductive rewriting<\/jats:bold>\n                    <\/jats:italic>\n                    , leveraging generative equality saturation to effectively explore rewrite space and produce semantically equivalent mutants for the purpose of validation. We implemented\n                    <jats:sc>Aries<\/jats:sc>\n                    as a practical validation tool and evaluated it on leading SMT solvers, including Z3 and cvc5. Our experiments demonstrate that\n                    <jats:sc>Aries<\/jats:sc>\n                    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\n                    <jats:sc>Aries<\/jats:sc>\n                    \u2019s strength in exploring the rewrite space.\n                  <\/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":5,"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1153-2013","authenticated-orcid":false,"given":"Yibiao","family":"Yang","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9932-7315","authenticated-orcid":false,"given":"Jiangchang","family":"Wu","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4645-2526","authenticated-orcid":false,"given":"Yuming","family":"Zhou","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"2024cvc5. https:\/\/github.com\/cvc5\/cvc5."},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632928"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_5_1","unstructured":"ClarkBarrett PascalFontaine and CesareTinelli. 2022. The satisfiability modulo theories library (SMT-LIB). Retrieved 2022-08-18 fromhttp:\/\/smtlib.cs.uiowa.edu\/"},{"key":"e_1_3_1_6_1","doi-asserted-by":"crossref","unstructured":"ClarkBarrettand CesareTinelli. 2018. Satisfiability modulo theories. In Handbook of model checking. Springer 305\u2013343.","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597208"},{"key":"e_1_3_1_8_1","unstructured":"MartinBrain. 2024. How to know the implemented rewrite rules in cvc5?https:\/\/github.com\/cvc5\/cvc5\/discussions\/10275#discussioncomment-8159588."},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1670412.1670413"},{"key":"e_1_3_1_10_1","first-page":"209","volume-title":"8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings","author":"Cadar Cristian","year":"2008","unstructured":"CristianCadar, DanielDunbar, 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, RichardDravesand Robbertvan Renesse(Eds.). USENIX Association, 209\u2013224. http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571207"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620666.3651330"},{"key":"e_1_3_1_13_1","first-page":"578","volume-title":"13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018, Carlsbad, CA, USA, October 8-10, 2018","author":"Chen Tianqi","year":"2018","unstructured":"TianqiChen, ThierryMoreau, ZihengJiang, LianminZheng, Eddie Q.Yan, HaichenShen, MeghanCowan, LeyuanWang, YuweiHu, LuisCeze, CarlosGuestrin, and ArvindKrishnamurthy. 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-Dusseauand GeoffVoelker(Eds.). USENIX Association, 578\u2013594. https:\/\/www.usenix.org\/conference\/osdi18\/presentation\/chen"},{"key":"e_1_3_1_14_1","unstructured":"Tsong YuehChen S. C.Cheung and Siu-MingYiu. 2020. Metamorphic Testing: A New Approach for Generating Next Test Cases. CoRR abs\/2002.12543 (2020). arXiv:2002.12543https:\/\/arxiv.org\/abs\/2002.12543"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620665.3640392"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_17_1","first-page":"595","volume-title":"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 (IFIP Conference Proceedings, Vol. 162)","author":"Hoe James C.","year":"1999","unstructured":"James C.Hoeand 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 (IFIP Conference Proceedings, Vol. 162), L. MiguelSilveira, SrinivasDevadas, and Ricardo Augustoda Luz Reis(Eds.). Kluwer, 595\u2013619."},{"key":"e_1_3_1_18_1","unstructured":"AaronHurst AdamLerer Adam P.Goucher AdamPerelman AdityaRamesh AidanClark AJOstrow AkilaWelihinda AlanHayes AlecRadford AleksanderMadry AlexBaker-Whitcomb AlexBeutel AlexBorzunov AlexCarney AlexChow AlexKirillov AlexNichol AlexPaino AlexRenzin Alex TachardPassos AlexanderKirillov AlexiChristakis AlexisConneau AliKamali AllanJabri AllisonMoyer AllisonTam AmadouCrookes AminTootoonchian AnanyaKumar AndreaVallone AndrejKarpathy AndrewBraunstein AndrewCann AndrewCodispoti AndrewGalu AndrewKondrich AndrewTulloch AndreyMishchenko AngelaBaek AngelaJiang AntoinePelisse AntoniaWoodford AnujGosalia ArkaDhar AshleyPantuliano AviNayak AvitalOliver BarretZoph BehroozGhorbani BenLeimberger BenRossen BenSokolowsky BenWang BenjaminZweig BethHoover BlakeSamic BobMcGrew BobbySpero BogoGiertler BowenCheng BradLightcap BrandonWalkin BrendanQuinn BrianGuarraci BrianHsu BrightKellogg BrydonEastman CamilloLugaresi Carroll L.Wainwright CaryBassin CaryHudson CaseyChu ChadNelson ChakLi Chan JunShern ChanningConger CharlotteBarette ChelseaVoss ChenDing ChengLu ChongZhang ChrisBeaumont ChrisHallacy ChrisKoch ChristianGibson ChristinaKim ChristineChoi ChristineMcLeavey ChristopherHesse ClaudiaFischer ClemensWinter ColeyCzarnecki ColinJarvis ColinWei ConstantinKoumouzelis and DaneSherburn. 2024. GPT-4o System Card. CoRR abs\/2410.21276 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2410.21276arXiv:2410.21276"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_35"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE56229"},{"key":"e_1_3_1_21_1","first-page":"821","volume-title":"18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024, Santa Clara, CA, USA, July 10-12, 2024","author":"Jiang Zu-Ming","year":"2024","unstructured":"Zu-MingJiangand ZhendongSu. 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, AdaGavrilovskaand Douglas B.Terry(Eds.). USENIX Association, 821\u2013835. https:\/\/www.usenix.org\/conference\/osdi24\/presentation\/jiang"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632900"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_11"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57246-3_17"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613140"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","unstructured":"Muhammad NumairMansur MariaChristakis ValentinW\u00fcstholz and FuyuanZhang. 2020. Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 701\u2013712. https:\/\/doi.org\/10.1145\/3368089.3409763 10.1145\/3368089.3409763","DOI":"10.1145\/3368089.3409763"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_44"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485496"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_5"},{"key":"e_1_3_1_33_1","first-page":"65","volume-title":"22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022","author":"N\u00f6tzli Andres","year":"2022","unstructured":"AndresN\u00f6tzli, HanielBarbosa, AinaNiemetz, MathiasPreiner, AndrewReynolds, Clark W.Barrett, and CesareTinelli. 2022. Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. In 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022, AlbertoGriggioand NehaRungta(Eds.). IEEE, 65\u201374. https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_12"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_20"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622834"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00202"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485529"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254104"},{"key":"e_1_3_1_39_1","first-page":"1","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"HelgiSigurbjarnarson, JamesBornholt, EminaTorlak, and XiWang. 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, KimberlyKeetonand TimothyRoscoe(Eds.). USENIX Association, 1\u201316. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/sigurbjarnarson"},{"key":"e_1_3_1_40_1","unstructured":"SMT-COMP. 2023. The International SMT Competition. Retrieved 2023-12-1 fromhttps:\/\/smt-comp.github.io\/2023\/"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00018"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","unstructured":"MaolinSun YibiaoYang JiangchangWu and YumingZhou. 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_3_1_43_1","first-page":"649","volume-title":"18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024, Santa Clara, CA, USA, July 10-12, 2024","author":"Sun Xudong","year":"2024","unstructured":"XudongSun, WenjieMa, Jiawei TylerGu, ZichengMa, TejChajed, JonHowell, AndreaLattuada, OdedPadon, LalithSuresh, AdrianaSzekeres, and TianyinXu. 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, AdaGavrilovskaand Douglas B.Terry(Eds.). USENIX Association, 649\u2013666. https:\/\/www.usenix.org\/conference\/osdi24\/presentation\/sun-xudong"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446707"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2023.3321381"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3514221.3526125"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689795"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428261"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00018"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3669940.3707271"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656400"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616275"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591239"},{"key":"e_1_3_1_57_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":[[2026,7,16]],"date-time":"2026-07-16T10:13:50Z","timestamp":1784196830000},"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"}}]}}