Deciding Satisfiability of Quantified Bitvector Formulae with BDDs (abstract)

Quantifier Instantiations: To Mimic or To Revolt? (abstract)

From MBQI to Enumerative Instantiation and Back (abstract)

Being polite is not enough (and other limits of theory combination) (abstract)

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

Evaluating Binary Polynomials using Subpolynomials (abstract)

Satisfiability Modulo Exponential Integer Arithmetic (abstract)

Constraint Propagation for Bit-Vectors in Alt-Ergo (abstract)

Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search (abstract)

Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2 (abstract)

Space Explanations of Neural Network Classification (abstract)

Approximate SMT Counting Beyond Discrete Domains (abstract)

Syntax-Guided Synthesis with CounterExample Guided E-graphs: A Work-In-Progress Report (abstract)

On Writing SMT-LIB Scripts: Metrics and a new Dataset (abstract)

SAT Reasoning in CDCL(T) Solvers (abstract)

An Optimization Modulo Theories-based Approach to Cumulative Scheduling with Delays (abstract)

Visualization of execution traces in Colibri 2 SMT solver (abstract)

A Conjecture Regarding SMT Instability (abstract)

A Catalog of SMT-LIB Benchmarks (abstract)

A Proposal for an OMT Extension to SMT-LIB (abstract)

Instability Track for SMT-COMP (abstract)

SMT-COMP presentation

SMT-LIB discussion

Business Meeting