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.
  • A minimal syntax highlighting mode for VIM.
  • 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 scripts implemented in Flex and Bison and C99
  • An OCaml parser for SMT-LIB 2.0 scripts.
  • ddSMT, a delta-debugger (input minimizer) for SMT-LIB-compliant solvers.
  • Delta SMT, another delta-debugger for SMT-LIB-compliant solvers [Webpage].
  • A Haskell library for parsing and printing SMT-LIB 2 scripts.
  • SBV, a tool to express properties of Haskell programs and prove them using SMT solvers via an SMT-LIB interface.
  • Nsolv, a front-end that allows multiple SMT-LIB compliant solvers to be executed in parallel.
  • SMT Kit, a C++11 library for many-sorted logics targeting quantifier-free SMT-LIB 2.0 formulas.
  • SMTpp, a tool operating both as a source-to-source transformer and analyzer for SMT-LIB.