SMT 2025: 23RD INTERNATIONAL WORKSHOP ON SATISFIABILITY MODULO THEORIES
SLIDES

A Proposal for an OMT Extension to SMT-LIB

Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli and Clark Barrett

Being Polite is Not Enough (and Other Limits of Theory Combination)

Guilherme Toledo, Benjamin Przybocki and Yoni Zohar

Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search

Enrico Lipparini, Thomas Hader, Ahmed Irfan and Stéphane Graham-Lengrand

A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints

Ellen Dasnois and Pascal Fontaine

Deciding Satisfiability of Quantified Bitvector Formulae with BDDs

Jan Strejček and Jochen Hoenicke

Evaluating Binary Polynomials using Subpolynomials

Jacob M. Howe, Martin Brain and Arnau Gàmez-Montolio

Space Explanations of Neural Network Classification

Faezeh Labbaf, Tomáš Kolárik, Martin Blicha, Grigory Fedyukovich, Michael Wand and Natasha Sharygina

From MBQI to Enumerative Instantiation and Back

Marek Dančo, Petra Hozzová and Mikoláš Janota

On Writing SMT-LIB Scripts: Metrics and a New Dataset

Soaibuzzaman and Jan Oliver Ringert
Total: 9 presentations.