The 23rd International Workshop on Satisfiability Modulo Theory (SMT 2025) and the 16th International Workshop on Pragmatics of SAT (PoS 2025) were held in Glasgow, UK, on August 10th and 11th in association with the 28th International Conference on Theory and Application of Satisfiability Testing (SAT), the 31st International Conference on Principles and Practice of Constraint Programming (CP), and the 18th International Symposium on Combinatorial Search (SoCS). 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 eforts. The aim of the 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
SMT 2025 featured invited talks by Jan Strejček from Masaryk University and Katalin Fazekas from TU Wien. There were 19 presentations of peer-reviewed papers. The workshop received 24 submissions, out of which 19 were accepted. Each submission was reviewed by three program committee members. Of the 19 accepted submissions, 13 are published in this volume: three as original papers, and ten as extended abstracts. The remaining six were submitted to the workshop for presentation only.
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 CP/SAT/SoCS organizers for hosting the workshop, EasyChair for the availability of their conference system, and CEUR for their help to publish these proceedings.
SMT 2025 was sponsored by Certora and the Ethereum Foundation. We are grateful for their generosity in supporting the workshop.
PoS 2025 The Pragmatics of SAT (PoS) workshop is an annual event dedicated to providing a forum for discussion and presentation of the design and application of SAT solver and related solver technologies. This includes (but is not restricted to) Satisfiability Modulo Theories (SMT), Answer Set Programming (ASP), Constraint Programming (CP).
The success of solver technologies for declarative languages such as Boolean satisfiability (SAT) over the last two decades is mainly due to both the availability of eficient solver implementations and the growing number of problems that can eficiently be solved through the declarative approach. Designing eficient solvers requires both the understanding of fundamental underlying algorithms and expertise in how to implement such algorithms as eficient and robust solvers.
The PoS workshop series is organized together with the International Conferences on Theory and Applications of Satisfiability Testing (SAT). The year 2025 constituted the 16th edition of the workshop.
PoS 2025 received a total of 11 submissions, out of which 10 were accepted. Each submission was reviewed by three program committee members. Out of the 10 accepted submissions, 4 are published in this volume as original papers and the remaining 6 were submitted for presentation only.
During the workshop, we honored the memory of Allen Van Gelder, one of the founding members, with a short tribute following his passing on April 25, 2025.
We would like to thank the program committee, the authors, the workshop participants and the PoS Steering Committee for their contributions to the workshop. We would further like to thank the CP/SAT/SoCS organizers for hosting the workshop, EasyChair for the availability of their conference system, and CEUR for their help to publish these proceedings.
Peer Reviewers
Sophie Tourret, Inria, France
Nikolaj Bjørner, Microsoft, US Maria Paola Bonacina, Università degli Studi di Verona, Italy Guillaume Bury, OCamlPro, France Bruno Dutertre, Amazon Web Services, US Katalin Fazekas, TU Wien, Austria Pascal Fontaine, Université de Liège, Belgium Florian Frohn, RWTH Aachen University, Germany Alessandro Gianola, Lisbon University, Portugal Stéphane Graham-Lengrand, SRI International, US Alberto Griggio, Fondazione Bruno Kessler, Italy Martin Jonáš, Masaryk University, Czechia Alexander Nadel, Technion & NVIDIA, Israel Aina Niemetz, Stanford University, US Mathias Preiner, Stanford University, US Philipp Rümmer, University of Regensburg, Germany Hans-Jörg Schurr, University of Iowa, US Natasha Sharygina, University of Lugano, Switzerland Cesare Tinelli, The University of Iowa, US Yoni Zohar, Bar-Ilan University, Israel
SMT
Deciding Satisfiability of Quantified Bitvector Formulae with BDDs . . . . . . . . . . . . . . 1
Jan Strejček SAT Reasoning in CDCL(T) Solvers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
Katalin Fazekas
Evaluating Binary Polynomials using Subpolynomials . . . . . . . . . . . . . . . . . . . . . . 3
Jacob M. Howe, Martin Brain, Arnau Gàmez-Montolio An Optimization Modulo Theories-Based Approach to Cumulative Scheduling with Delays . 16
Antton Kasslin, Jeremias Berg A Proposal for an OMT Extension to SMT-LIB . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark Barrett