Utilities and Tools

The page contains a set of utilities and tools to work with the SMT-LIB 2 format.

Note: Most of the utilities tools below have been developed by third parties and are provided here as a convenience to the community. Appearance on this page does not imply an endorsement of their full conformance to the SMT-LIB standard. Please contact each utility's authors directly for questions, bug reports, or other requests.



  • An ANTLR grammar of SMT-LIB 2.6 scripts.
  • jSMTLIB, a suite of Java tools for parsing and type-checking SMT-LIB 2 scripts, and translating them to the input languages of some non-SMT-LIB-conforming solvers.
  • An open source generic lexer and parser for SMT-LIB 2.0 scripts implemented in Flex and Bison and C99.
  • A Haskell library for parsing and printing SMT-LIB 2 scripts.
  • An SWI-Prolog parser for SMT-LIB 2.6 scripts.
  • An OCaml parser for SMT-LIB 2.0 scripts (not maintained).

Language Servers

  • Dolmen, an LSP server SMT-LIB 2.6.


  • ddSMT, a delta-debugger (input minimizer) for SMT-LIB-compliant solvers.


  • Nsolv, a front-end that allows multiple SMT-LIB 2 compliant solvers to be executed in parallel.
  • rsmt2, a generic Rust library to interact with SMT-LIB 2 compliant solvers running in a separate system process.
  • SBV, a tool to express properties of Haskell programs and prove them using SMT solvers via an SMT-LIB interface.
  • SMT Kit, a C++11 library for many-sorted logics targeting quantifier-free SMT-LIB 2.0 formulas.
  • SMTpp, an OCaml tool operating both as a source-to-source transformer and analyzer for SMT-LIB 2.0.
  • pySMT, a Python library for manipulating and solving SMT formulas using SMT-LIB 2-compliant solvers.