Blazing-Fast SMT-LIB Parsing for Rust and Lean

Jan Onderka, Armin Biere, Henrik Böving

SMT-LIB is a standard input format for Satisfiability Modulo Theories (SMT) solvers. However, parsing the format is non-trivial and can become a bottleneck, e.g. when retrieving benchmark metadata or normalising the input for solvers. We introduce blazing-smtlib, a Rust parsing library for SMT-LIB, and BSmtLib, its port to Lean. We outline the library API we designed for composability and extensibility (including non-standard SMT-LIB commands), and discuss our implementation decisions for fast lexing and parsing. We proved that our lexing and parsing with Lean-specific optimisations match our formalised reading of the SMT-LIB syntax. We measured performance on a representative sample from the 2025 SMT-LIB corpus and found that blazing-smtlib is more than 6 times faster on the geometric mean than previous parsing libraries and BSmtLib is faster or comparable to them.