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