Satisfiability Modulo Theories 20th International Workshop SMT 2022 Proceedings Haifa, Israel Affiliated with IJCAR 2022 Part of FLoC 2022 August 11 – 12, 2022 David Déharbe, Antti E. J. Hyvärinen (editors) SMT 2022: Satisfiability Modulo Theories, August 11–12, 2022, Haifa, Israel © 2022 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) Preface The International Workshop on Satisfiability Modulo Theories is an annual event dedicated to Satisfiability Modulo Theories (SMT). The 20th edition of the SMT workshop was held in Haifa, Israel, on August 11th and 12th in association with the International Joint Conference on Automated Reasoning 2022 (IJCAR 2022), as part of the 8th Federated Logic Conference (FLoC 2022). 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 2022 featured an invited talk by Aina Niemetz from Stanford University, a panel dis- cussion, and the presentation of 14 peer-reviewed papers, along with a discussion on SMT proofs and a competitive event. The workshop received 15 paper submissions, out of which 14 were accepted. Each submission was reviewed by three program committee members. Of the 14 accepted submissions, four were accepted as regular papers, and six as extended abstracts. The remaining five contributions were submitted to the workshop for presentation only. The authors of one of these presentations agreed to include the abstract of their talk into these proceedings. We would like to thank the program committee, the subreviewers, the authors, the invited speaker, the panelists, the SMT competition organisers and participants, and the SMT Steering Committee for their contributions to the workshop. We thank Alexander Nadel and Aina Niemetz, the chairs of SMT 2021 for their valuable advice in organising the workshop. We would further like to thank the IJCAR and FLoC organizers for hosting the workshop, EasyChair for the availability of their conference system, and CEUR for their help to publish these proceedings. SMT 2022 was sponsored by AdaCore, Ethereum Foundation, Informal Systems, and Runtime Verification. We are grateful for their generosity in supporting the workshop. David Déharbe and Antti Hyvärinen Co-chairs, SMT 2022 Program Committee David Déharbe, CLEARSY Antti Hyvärinen, Università della Svizzera italiana Leonardo Alt, Ethereum Foundation Haniel Barbosa, Universidade Federal de Minas Gerais Nikolaj Bjørner, Microsoft Research Maria Paola Bonacina, Università degli Studi di Verona Martin Bromberger, Max-Planck Institut für Informatik Rayna Dimitrova, CISPA Helmholtz Center for Information Security Pascal Fontaine, Université de Liège Stéphane Graham-Lengrand, SRI International Liana Hadarean, Amazon Web Services Jochen Hoenicke, University of Freiburg Chantal Keller, Université Paris-Saclay Igor Konnov, Informal Systems Austria Matteo Marescotti, Meta Platforms, UK Aina Niemetz, Stanford University Elizabeth Polgreen, University of Edinburgh Mathias Preiner, Stanford University Andrew Reynolds, University of Iowa Tanja Schindler, University of Freiburg Sophie Tourret, Inria and MPI for Informatics Yoni Zohar, Bar Ilan University Subreviewers Hans-Jörg Schurr, Université de Lorraine Alex Ozdemir, Stanford University Contents Invited Talks Invited Talk: Local Search for Bit-Precise Reasoning and Beyond 1 Aina Niemetz Regular Papers Trail Saving in SMT 2 Milan Banković, David Šćepanović CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length 18 Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar An SMT-LIB Theory of Heaps 38 Zafer Esen, Philipp Rümmer A Simple Proof Format for SMT 54 Jochen Hoenicke, Tanja Schindler Extended Abstracts User-Propagators for Custom Theories in SMT Solving 71 Nikolaj Bjorner, Clemens Eisenhofer, Laura Kovács The VMT-LIB Language and Tools (Extended Abstract) 80 Alessandro Cimatti, Alberto Griggio, Stefano Tonetta An SMT Approach for Solving Polynomials over Finite Fields 90 Thomas Hader, Laura Kovács Goose: A Meta-Solver for Deep Neural Network Verification 99 Joseph Scott, Guanting Pan, Elias B. Khalil, Vijay Ganesh On Satisfiability of Polynomial Equations over Large Prime Fields 114 Joseph Scott, Guanting Pan, Elias B. Khalil, Vijay Ganesh Presentation-Only Papers (Abstracts) Abstract: Challenges and Solutions for Higher-Order SMT Proofs 128 Chad E. Brown, Mikoláš Janota, Cezary Kaliszyk