Satisfiability Modulo Theories — 18th International Workshop, SMT 2020 Online (initially located in Paris, France) July 5–6, 2020 Proceedings Edited by François Bobot and Tjark Weber Copyright c 2020 for the individual papers by the papers’ authors. Copyright c 2020 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). Preface SMT 2020, the 18th International Workshop on Satisfiability Modulo Theories, was held as a satellite event of IJCAR 2020 and FSCD 2020 on July 5–6, 2020. The workshop was originally scheduled to take place in Paris, France, but was eventually held online as a virtual meeting because of the COVID-19 pandemic. For background on Satisfiability Modulo Theories and the SMT workshop series, we quote the following description from its website:1 Determining the satisfiability of first-order formulas modulo background theories, known as the Satisfiability Modulo Theories (SMT) problem, has proved to be an enabling technology for verification, synthesis, test generation, compiler optimiza- tion, scheduling, and other areas. The success of SMT techniques depends on the development of both domain-specific decision procedures for each background the- ory (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 SMT Workshop is to bring together researchers and users of SMT tools and techniques. 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 Papers on pragmatic aspects of implementing and using SMT tools, as well as novel applications of SMT, are especially encouraged. SMT 2020 featured invited talks by Philipp Rümmer and Mooly Sagiv, a joint session with the 5th International Workshop on Satisfiability Checking and Symbolic Computation (SC2 2020), and presentations of nine peer-reviewed papers. Of these, five papers are published in this volume, two as regular papers and three as short papers. The other four papers were submitted to the workshop for presentation only; we are only including their abstracts. We would like to thank the SMT Steering Committee, the IJCAR/FSCD organisers, the SMT Program Committee, the authors and speakers, and everyone else who, by supporting and adapting to the online format of the event, contributed to the workshop’s success in the midst of a global pandemic. François Bobot and Tjark Weber Co-chairs, SMT 2020 1 https://smt-workshop.cs.uiowa.edu/2020/ Program Committee Haniel Barbosa, Universidade Federal de Minas Gerais Clark Barrett, Stanford University Nikolaj Bjorner, Microsoft Research Simon Cruanes, Aesthetic Integration Pascal Fontaine, Université de Lorraine Stéphane Graham-Lengrand, SRI International Alberto Griggio, Fondazione Bruno Kessler Antti Hyvärinen, Università della Svizzera italiana Mohamed Iguernelala, OcamlPro Dejan Jovanović, SRI International Chantal Keller, LRI, Université Paris-Sud Yannick Moy, AdaCore Aina Niemetz, Stanford University Marie Pelleau, Université Nice Sophia Antipolis Mathias Preiner, Stanford University Giles Reger, University of Manchester Andrew Reynolds, University of Iowa Natasha Sharygina, Università della Svizzera italiana Peter J. Stuckey, Monash University Cesare Tinelli, University of Iowa François Bobot, CEA List Tjark Weber, Uppsala University Contents Invited Talks Solving String Constraints, Starting from the Beginning and from the End . . . . . . . . . . . . . . . . 1 Philipp Rümmer Harnessing SMT Solvers for Verifying Low Level Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 Mooly Sagiv Contributed Papers Lifting congruence closure with free variables to λ-free higher-order logic via SAT encoding 3 Sophie Tourret, Pascal Fontaine, Daniel El-Ouraoui and Haniel Barbosa An Empirical Evaluation of SAT Solvers on Bit-vector Problems . . . . . . . . . . . . . . . . . . . . . . . . . 15 Bruno Dutertre Structural Bit-vector Model Counting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Seonmo Kim and Stephen McCamant Bayesian Optimisation of Solver Parameters in CBMC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Chaitanya Mangla, Sean Holden and Lawrence Paulson Smt-Switch: a solver-agnostic C++ API for SMT solving . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Makai Mann, Amalee Wilson, Cesare Tinelli and Clark Barrett Presentation-only Papers (Abstracts) Abstract: SMT-Friendly Formalization of the Solidity Memory Model . . . . . . . . . . . . . . . . . . . . 59 Ákos Hajdu and Dejan Jovanović Abstract: Towards an SMT-LIB Theory of Heap . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 Zafer Esen and Philipp Rümmer Abstract: BanditFuzz: A Reinforcement-Learning based Performance Fuzzer for SMT Solvers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 Joseph Scott, Federico Mora and Vijay Ganesh Abstract: MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers . . . . 62 Joseph Scott, Aina Niemetz, Mathias Preiner and Vijay Ganesh