{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T10:37:55Z","timestamp":1790937475955,"version":"4.1.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>We introduce ET, a grammar-based enumerator for validating SMT solver correctness and performance. By compiling grammars of the SMT theories to algebraic datatypes, ET leverages the functional enumerator FEAT. ET is highly effective at bug finding and has many complimentary benefits. Despite the extensive and continuous testing of the state-of-the-art SMT solvers Z3 and cvc5, ET found 102 bugs, out of which 84 were confirmed and 40 were fixed. Moreover, ET can be used to understand the evolution of solvers. We derive eight grammars realizing all major SMT theories including the booleans, integers, reals, realints, bit-vectors, arrays, floating points, and strings. Using ET, we test all consecutive releases of the SMT solvers Z3 and CVC4\/cvc5 from the last six years (61 versions) on 8 million formulas, and 488 million solver calls. Our results suggest improved correctness in recent versions of both solvers but decreased performance in newer releases of Z3 on small timeouts (since z3-4.8.11) and regressions in early cvc5 releases on larger timeouts. Due to its systematic testing and efficiency, we further advocate ET\u2019s use for continuous integration.<\/jats:p>","DOI":"10.1145\/3689795","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"2378-2401","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Validating SMT Solvers for Correctness and Performance via Grammar-Based Enumeration"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4122-5981","authenticated-orcid":false,"given":"Dominik","family":"Winterer","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2970-1391","authenticated-orcid":false,"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"AdaCore. 2021. SPARK. Retrieved 2023-10-23 from https:\/\/github.com\/AdaCore\/spark2014"},{"key":"e_1_3_1_3_2","unstructured":"Alexandr Andoni Dumitru Daniliuc Sarfraz Khurshid and Darko Marinov. 2003. Evaluating the \u201cSmall Scope Hypothesis\u201d. In POPL \u201903. 1\u201312."},{"key":"e_1_3_1_4_2","doi-asserted-by":"crossref","unstructured":"John Backes Pauline Bolignano Byron Cook Catherine Dodge Andrew Gacek Kasper S\u00f8e Luckow Neha Rungta Oksana Tkachuk and Carsten Varming. 2018. Semantic-based Automated Reasoning for AWS Access Policies using SMT. In FMCAD \u201918. 1\u20139.","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"e_1_3_1_5_2","doi-asserted-by":"crossref","unstructured":"Clark Barrett Christopher L. Conway Morgan Deters Liana Hadarean Dejan Jovanovic Tim King Andrew Reynolds and Cesare Tinelli. 2011. CVC4. In CAV \u201911. 171\u2013177. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14 10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_1_6_2","doi-asserted-by":"crossref","unstructured":"Clark Barrett Leonardo de Moura and Aaron Stump. 2005. SMT-COMP: Satisfiability Modulo Theories Competition. In CAV \u201905. 20\u201323.","DOI":"10.1007\/11513988_4"},{"key":"e_1_3_1_7_2","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2019. The Satisfiability Modulo Theories Library (SMT-LIB). Retrieved 2023-10-2023 from www.SMT-LIB.org"},{"key":"e_1_3_1_8_2","unstructured":"Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The SMT-LIB Standard: Version 2.0. In SMT \u201910."},{"key":"e_1_3_1_9_2","doi-asserted-by":"crossref","unstructured":"S. M. Blackburn R. Garner C. Hoffman A. M. Khan K. S. McKinley R. Bentzur A. Diwan D. Feinberg D. Frampton S. Z. Guyer M. Hirzel A. Hosking M. Jump H. Lee J. E. B. Moss A. Phansalkar D. Stefanovic T. VanDrunen D. von Dincklage and B. Wiedermann. 2006. The DaCapo Benchmarks: Java Benchmarking Development and Analysis. In OOPSLA \u201906. 169\u2013190. https:\/\/doi.org\/10.1145\/1167473.1167488 10.1145\/1167473.1167488","DOI":"10.1145\/1167515.1167488"},{"key":"e_1_3_1_10_2","doi-asserted-by":"crossref","unstructured":"Dmitry Blotsky Federico Mora Murphy Berzish Yunhui Zheng Ifaz Kabir and Vijay Ganesh. 2018. StringFuzz: A Fuzzer for String Solvers. In CAV \u201918. 45\u201351. https:\/\/doi.org\/10.1007\/978-3-642-00768-2_16 10.1007\/978-3-642-00768-2_16","DOI":"10.1007\/978-3-319-96142-2_6"},{"key":"e_1_3_1_11_2","doi-asserted-by":"crossref","unstructured":"Robert Brummayer and Armin Biere. 2009. Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In TACAS \u201909. 174\u2013177.","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"e_1_3_1_12_2","doi-asserted-by":"crossref","unstructured":"Robert Brummayer and Armin Biere. 2009. Fuzzing and delta-debugging SMT solvers. In SMT \u201909. 1\u20135. https:\/\/doi.org\/10.1145\/1670412.1670413 10.1145\/1670412.1670413","DOI":"10.1145\/1670412.1670413"},{"key":"e_1_3_1_13_2","doi-asserted-by":"crossref","unstructured":"Alexandra Bugariu and Peter M\u00fcller. 2020. Automatically Testing String Solvers. In ICSE \u201920. 1459\u20131470. https:\/\/doi.org\/10.1145\/3377811.3380398 10.1145\/3377811.3380398","DOI":"10.1145\/3377811.3380398"},{"key":"e_1_3_1_14_2","doi-asserted-by":"crossref","unstructured":"W.H. Burkhardt. 1967. Generating test programs from syntax. In Computing. 53\u201373.","DOI":"10.1007\/BF02235512"},{"key":"e_1_3_1_15_2","unstructured":"Cristian Cadar Daniel Dunbar and Dawson R. Engler. 2008. KLEE: Unassisted and Automatic Generation of High- Coverage Tests for Complex Systems Programs. In OSDI \u201908. 209\u2013224."},{"key":"e_1_3_1_16_2","doi-asserted-by":"crossref","unstructured":"Koen Claessen and John Hughes. 2000. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In ICFP \u201900. 268\u2013279. https:\/\/doi.org\/10.1145\/351240.351266 10.1145\/351240.351266","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_1_17_2","unstructured":"SAT Competition. 2023. The International SAT Competition Web Page. Retrieved 2023-10-23 from https:\/\/github.com\/AdaCore\/spark2014"},{"key":"e_1_3_1_18_2","doi-asserted-by":"crossref","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS \u201908. 337\u2013340. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24 10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_19_2","doi-asserted-by":"crossref","unstructured":"David Detlefs Greg Nelson and James B. Saxe. 2005. Simplify: A Theorem Prover for Program Checking. JACM (2005) 365\u2013473. https:\/\/doi.org\/10.1145\/1066100.1066102 10.1145\/1066100.1066102","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_1_20_2","doi-asserted-by":"crossref","unstructured":"Jonas Duregard Patrick Jansson and Meng Wang. 2012. FEAT: Functional Enumeration of Algebraic Types. In Haskell \u201912. 61\u201372. https:\/\/doi.org\/10.1145\/2430532.2364515 10.1145\/2430532.2364515","DOI":"10.1145\/2430532.2364515"},{"key":"e_1_3_1_21_2","doi-asserted-by":"crossref","unstructured":"Ambros Gleixner Gregor Hendel Gerald Gamrath Tobias Achterberg Michael Bastubbe Timo Berthold Philipp M. Christophel Kati Jarck Thorsten Koch Jeff Linderoth Marco L\u00fcbbecke Hans D. Mittelmann Derya Ozyurt Ted K. Ralphs Domenico Salvagnin and Yuji Shinano. 2021. MIPLIB 2017: Data-Driven Compilation of the 6th Mixed-Integer Programming Library. Mathematical Programming Computation (2021). https:\/\/doi.org\/10.1007\/s12532-020-00194-3 10.1007\/s12532-020-00194-3","DOI":"10.1007\/s12532-020-00194-3"},{"key":"e_1_3_1_22_2","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid Nils Klarlund and Koushik Sen. 2005. DART: directed automated random testing. In PLDI \u201905. 213\u2013223. https:\/\/doi.org\/10.1145\/1064978.1065036 10.1145\/1064978.1065036","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_1_23_2","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid Michael Y. Levin and David Molnar. 2012. SAGE: Whitebox Fuzzing for Security Testing: SAGE Has Had a Remarkable Impact at Microsoft. Queue (2012) 20\u201327.","DOI":"10.1145\/2090147.2094081"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1147\/sj.94.0242"},{"key":"e_1_3_1_25_2","unstructured":"Christian Holler Kim Herzig and Andreas Zeller. 2012. Fuzzing with Code Fragments. In USENIX Security Symposium. https:\/\/doi.org\/10.5555\/2362793.2362831 10.5555\/2362793.2362831"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_3_1_27_2","doi-asserted-by":"crossref","unstructured":"D. Jackson and C.A. Damon. 1996. Elements of style: analyzing a software design feature with a counterexample detector. TSE \u201996 (1996) 484\u2013495. https:\/\/doi.org\/10.1109\/32.538605 10.1109\/32.538605","DOI":"10.1109\/32.538605"},{"key":"e_1_3_1_28_2","doi-asserted-by":"crossref","unstructured":"Muhammad Numair Mansur Maria Christakis Valentin W\u00fcstholz and Fuyuan Zhang. 2020. Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing. In FSE \u201920. 701\u2013712. https:\/\/doi.org\/10.1145\/3368089.3409763 10.1145\/3368089.3409763","DOI":"10.1145\/3368089.3409763"},{"key":"e_1_3_1_29_2","volume-title":"Tools for Discovery, Refinement and Generalization of Functional Properties by Enumerative Testing","author":"Braquehais Rudy Matela","year":"2017","unstructured":"Rudy Matela Braquehais. 2017. Tools for Discovery, Refinement and Generalization of Functional Properties by Enumerative Testing. Ph. D. Dissertation. University of York."},{"key":"e_1_3_1_30_2","doi-asserted-by":"crossref","unstructured":"Aina Niemetz Mathias Preiner and Clark Barrett. 2022. Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. In CAV \u201922. 92\u2013106. https:\/\/doi.org\/10.1007\/978-3-031-13188-2_5 10.1007\/978-3-031-13188-2_5","DOI":"10.1007\/978-3-031-13188-2_5"},{"key":"e_1_3_1_31_2","article-title":"Model-based API testing for SMT solvers","volume":"10","author":"Niemetz Aina","year":"2017","unstructured":"Aina Niemetz, Mathias Preiner, and Armin Biere. 2017. Model-based API testing for SMT solvers. In SMT \u201917. 10.","journal-title":"SMT \u201917"},{"key":"e_1_3_1_32_2","doi-asserted-by":"crossref","unstructured":"Jiwon Park Dominik Winterer Chengyu Zhang and Zhendong Su. 2021. Generative Type-Aware Mutation for Testing SMT Solvers. In OOPSLA \u201921. 1\u201319. https:\/\/doi.org\/10.1145\/3485529 10.1145\/3485529","DOI":"10.1145\/3485529"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jvlc.2018.10.004"},{"issue":"1","key":"e_1_3_1_34_2","article-title":"A Lightweight Formalism for Reference Lifetimes and Borrowing in Rust","volume":"43","author":"Pearce David J.","year":"2021","unstructured":"David J. Pearce. 2021. A Lightweight Formalism for Reference Lifetimes and Borrowing in Rust. ACM Trans. Program. Lang. Syst. 43, 1 (2021). https:\/\/doi.org\/10.1145\/3443420 10.1145\/3443420","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"e_1_3_1_35_2","doi-asserted-by":"crossref","unstructured":"Colin Runciman Matthew Naylor and Fredrik Lindblad. 2008. Smallcheck and Lazy Smallcheck: Automatic Exhaustive Testing for Small Values. In Haskell \u201908. 37\u201348. https:\/\/doi.org\/10.1145\/1411286.1411292 10.1145\/1411286.1411292","DOI":"10.1145\/1411286.1411292"},{"key":"e_1_3_1_36_2","doi-asserted-by":"crossref","unstructured":"Neha Rungta. 2022. A Billion SMT Queries a Day (Invited Paper). In CAV \u201922. 3\u201318. https:\/\/doi.org\/10.1007\/978-3-031-13185-1_1 10.1007\/978-3-031-13185-1_1","DOI":"10.1007\/978-3-031-13185-1_1"},{"key":"e_1_3_1_37_2","doi-asserted-by":"crossref","unstructured":"Joseph Scott Federico Mora and Vijay Ganesh. 2020. BanditFuzz: Fuzzing SMT Solvers with Reinforcement Learning. In CAV \u201920. 68\u201386. https:\/\/doi.org\/10.1007\/978-3-030-63618-0_5 10.1007\/978-3-030-63618-0_5","DOI":"10.1007\/978-3-030-63618-0_5"},{"key":"e_1_3_1_38_2","volume-title":"Program Synthesis by Sketching","author":"Solar-Lezama Armando","year":"2008","unstructured":"Armando Solar-Lezama. 2008. Program Synthesis by Sketching. Ph. D. Dissertation. University of California at Berkeley. https:\/\/doi.org\/10.1007\/978-3-642-10672-9_3 10.1007\/978-3-642-10672-9_3"},{"key":"e_1_3_1_39_2","unstructured":"SPEC. 2023. SPEC\u2019s Benchmarks and Tools. Retrieved 2023-10-23 from https:\/\/www.spec.org\/benchmarks.html"},{"key":"e_1_3_1_40_2","doi-asserted-by":"crossref","unstructured":"Kevin Sullivan Jinlin Yang David Coppit Sarfraz Khurshid and Daniel Jackson. 2004. Software Assurance by Bounded Exhaustive Testing. In ISSTA \u201904. 133\u2013142. https:\/\/doi.org\/10.1145\/1013886.1007531 10.1145\/1013886.1007531","DOI":"10.1145\/1007512.1007531"},{"key":"e_1_3_1_41_2","doi-asserted-by":"crossref","unstructured":"Geoff Sutcliffe. 2016. The CADE ATP System Competition \u2014 CASC. AI Magazine (Jul. 2016) 99\u2013101. https: \/\/ojs.aaai.org\/index.php\/aimagazine\/article\/view\/2620","DOI":"10.1609\/aimag.v37i2.2620"},{"key":"e_1_3_1_42_2","doi-asserted-by":"crossref","unstructured":"Emina Torlak and Rastislav Bodik. 2014. A lightweight symbolic virtual machine for solver-aided host languages. In PLDI \u201914. 530\u2013541. https:\/\/doi.org\/10.1145\/2594291.2594340 10.1145\/2594291.2594340","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_1_43_2","doi-asserted-by":"crossref","unstructured":"Dominik Winterer Chengyu Zhang and Zhendong Su. 2020. On the Unusal Effectiveness of Type-Aware Operator Mutation. OOPSLA \u201920 1\u201325. https:\/\/doi.org\/10.1145\/3428261 10.1145\/3428261","DOI":"10.1145\/3428261"},{"key":"e_1_3_1_44_2","doi-asserted-by":"crossref","unstructured":"Dominik Winterer Chengyu Zhang and Zhendong Su. 2020. Validating SMT Solvers via Semantic Fusion. PLDI \u201920 718\u2013\u2013730. https:\/\/doi.org\/10.1145\/3385412.3385985 10.1145\/3385412.3385985","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_1_45_2","doi-asserted-by":"crossref","unstructured":"Xuejun Yang Yang Chen Eric Eide and John Regehr. 2011. Finding and Understanding Bugs in C Compilers. In PLDI \u201911. 283\u2013294. https:\/\/doi.org\/10.1145\/1993316.1993532 10.1145\/1993316.1993532","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_1_46_2","doi-asserted-by":"crossref","unstructured":"Peisen Yao Heqing Huang Wensheng Tang Qingkai Shi Rongxin Wu and Charles Zhang. 2021. Fuzzing SMT Solvers via Two-Dimensional Input Space Exploration. In ISSTA \u201921. 322\u2013335. https:\/\/doi.org\/10.1145\/3460319.3464803 10.1145\/3460319.3464803","DOI":"10.1145\/3460319.3464803"},{"key":"e_1_3_1_47_2","doi-asserted-by":"crossref","unstructured":"Peisen Yao Heqing Huang Wensheng Tang Qingkai Shi Rongxin Wu and Charles Zhang. 2021. Skeletal Approximation Enumeration for SMT Solver Testing. In FSE \u201921. 1141\u20131153. https:\/\/doi.org\/10.1145\/3468264.3468540 10.1145\/3468264.3468540","DOI":"10.1145\/3468264.3468540"},{"key":"e_1_3_1_48_2","doi-asserted-by":"crossref","unstructured":"Qirun Zhang Chengnian Sun and Zhendong Su. 2017. Skeletal program enumeration for rigorous compiler testing. In PLDI \u201917. 347\u2013361. https:\/\/doi.org\/10.1145\/3140587.3062379 10.1145\/3140587.3062379","DOI":"10.1145\/3062341.3062379"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689795","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689795","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:14:07Z","timestamp":1770196447000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689795"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":47,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689795"],"URL":"https:\/\/doi.org\/10.1145\/3689795","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}