A Catalog of SMT-LIB Benchmarks

Hans-Jörg Schurr, Mathias Preiner, Aina Niemetz, Clark Barrett, Pascal Fontaine and Cesare Tinelli

Visualization of Execution Traces in Colibri 2 SMT Solver

Christophe Junke and François Bobot

Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2

Marcel Barlik and Martin Brain

Quantifier Instantiations: To Mimic or To Revolt?

Jan Jakubův and Mikoláš Janota

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

Guilherme Toledo, Benjamin Przybocki and Yoni Zohar

A Proposal for an OMT Extension to SMT-LIB

Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli and Clark Barrett

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

Ellen Dasnois and Pascal Fontaine

Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search

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

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

Soaibuzzaman and Jan Oliver Ringert

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

Deciding Satisfiability of Quantified Bitvector Formulae with BDDs

Jan Strejček and Jochen Hoenicke

From MBQI to Enumerative Instantiation and Back

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