Satisfiability Modulo Theories 22nd International Workshop SMT 2024 Proceedings Montreal, Canada Affiliated with CAV-36 July 22 – 23, 2024 Giles Reger1 , Yoni Zohar2 1 Amazon Web Services (AWS) 2 Bar Ilan University SMT 2024: 22st International Workshop on Satisfiability Modulo Theories July 22–23, 2024, Montreal Canada $ reggiles@amazon.com (G. Reger); yoni.zohar@biu.ac.il (Y. Zohar) € http://www.cs.man.ac.uk/~regerg/ (G. Reger); https://u.cs.biu.ac.il/~zoharyo1/ (Y. Zohar) © 2024 Copyright for the individual papers by the papers’ authors. Copyright for the volume as a collection by its editors. This volume and its papers are published under the Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings Preface The 22nd International Workshop on Satisfiability Modulo Theories was held in Montreal, Canada, on July 22nd and 23rd in association with the International Conference on Computer Aided Verification (CAV-36). The SMT workshop is an annual event dedicated to Satisfiability Modulo Theories (SMT). Determining the satisfiability of first-order formulas modulo background theories, known as the Satisfiability Modulo Theories problem, has proved to be an enabling technology for verification, synthesis, test generation, compiler optimization, scheduling, and other areas. The success of SMT techniques depends on the development of both domain-specific decision procedures for each background theory (e.g., linear arithmetic, the theory of arrays, or the theory of bit-vectors) and combination methods that allow one to obtain more versatile SMT tools, usually leveraging Boolean satisfiability (SAT) solvers. These ingredients together make SMT techniques well-suited for use in larger automated reasoning and verification efforts. The aim of the workshop is to bring together researchers and users of SMT tools and tech- niques. Relevant topics include but are not limited to: • Decision procedures and theories of interest • Combinations of decision procedures • Novel implementation techniques • Benchmarks and evaluation methodologies • Applications and case studies • Theoretical results SMT 2024 featured invited talks by Sophie Tourret from INRIA and Mathias Preiner from Stanford University, and the presentation of 12 peer-reviewed papers. The workshop received 13 submissions, out of which 12 were accepted. Each submission was reviewed by three program committee members. Of the 12 accepted submissions, seven are published in this volume: three as original papers, and four as extended abstracts. The remaining five were submitted to the workshop for presentation only. For one of them, the authors include the paper abstract in this volume. We would like to thank the program committee, the subreviewers, the authors, the invited speakers, the SMT-COMP organizers, workshop participants and the SMT Steering Committee for their contribution to the workshop. We would further like to thank the CAV organizers for hosting the workshop, EasyChair for the availability of their conference system, and CEUR for their help to publish these proceedings. SMT 2024 was sponsored by AWS, Halmos, and Ethereum Foundation. We are grateful for their generosity in supporting the workshop. Giles Reger and Yoni Zohar Co-chairs, SMT 2024 Program Committee Program Chairs Giles Reger, AWS Yoni Zohar, Bar Ilan University Program Committee Katalin Fazekas, TU Wien Viktor Kuncak, Ecole Polytechnique Fédérale de Lausanne Ahmed Irfan, SRI International Aina Niemetz, Stanford University Andrew Reynolds, University of Iowa Daniela Kaufmann, TU Wien Haniel Barbosa, Universidade Federal de Minas Gerais Nadia Labai, Amazon Clark Barrett, Stanford University Alexander Nadel, Technion and Intel Philipp Rümmer, University of Regensburg Nestan Tsiskaridze, Stanford University Guilherme Toledo, Bar Ilan University Yannick Moy, AdaCore Martin Suda, Czech Technical University in Prague Stéphane Graham-Lengrand, SRI International François Bobot, CEA Mate Soos, Ethereum Foundation Nikolaj Bjørner, Microsoft Subreviewers Enrico Lipparini, University of Genoa Thomas Hader, TU Wien Contents Invited Talks The Hows and Whys of Higher-Order SMT . . . . . . . . . . . . . . . . . . . . . . . 1 Sophie Tourret, Challenges in Bit-Vector Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 Mathias Preiner Regular Papers An SMT-LIB Theory of Finite Fields . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Thomas Hader and Alex Ozdemir Reconstruction of SMT proofs with Lambdapi . . . . . . . . . . . . . . . . . . . . . 13 Alessio Coltellacci, Stephan Merz and Gilles Dowek Arrays Reasoning in MCSat . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Ahmed Irfan and Stephane Graham-Lengrand Extended Abstracts CSB: A Counting and Sampling tool for Bit-vectors . . . . . . . . . . . . . . . . . . 36 Arijit Shaw and Kuldeep S. Meel Minimal logic detection and exporting smtlib problems with Dolmen . . . . . . . . 44 Guillaume Bury A Bit-vector to Integer Translation with bv2nat and nat2bv . . . . . . . . . . . . . . 53 Max Barth and Matthias Heizmann An SMT theory for N-Indexed Sequences . . . . . . . . . . . . . . . . . . . . . . . . 64 Hichem Rami Ait El Hara, François Bobot and Guillaume Bury Presentation-Only Papers (Abstracts) Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis . . . . . . 75 Zhengyang Lu, Stefan Siemer, Piyush Jha, Joel Day, Florin Manea and Vijay Ganesh