Tools

» Bitwuzla

Bitwuzla is a specialized Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions.
  https://bitwuzla.github.io
  https://github.com/bitwuzla

» Boolector

Boolector is a specialized Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. It further natively handles non-recursive first-order lambda terms.
  https://boolector.github.io
  https://github.com/boolector/boolector

» CVC4

CVC4 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It supports many theories and their combinations.
  https://cvc4.stanford.edu
  https://github.com/cvc4/cvc4-archived

» cvc5

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems and is the successor of CVC4. It supports many theories and their combinations.
  https://cvc5.github.io
  https://github.com/cvc5/cvc5

» ddSMT

ddSMT serves as an input minimizer for Sat Modulo Theories (SMT) benchmarks in SMT-LIB v2 format and its dialects and extensions.
  https://ddsmt.readthedocs.io
  https://github.com/ddsmt/ddSMT

» Murxla

A modular and highly extensible model-based API Fuzzer for SMT Solvers.
  https://murxla.github.io
  https://github.com/murxla/murxla

» BTOR2Tools

A generic parser and tool package for the BTOR2 format.

  https://github.com/boolector/btor2tools

» QBFcert

QBFcert is a framework for resolution-based extraction and validation of certificates for Quantified Boolean Formulas (QBF).
  http://fmv.jku.at/qbfcert

» QBFDD

QBFDD is a delta-debugger for quantified boolean formulas (QBF) in QDIMACS format.
  http://fmv.jku.at/qbfdd
  https://github.com/aniemetz/qbfdd

» QxBF

QxBF is a preprocessor for QBFs in QDIMACS format based on failed literal detection.
  http://fmv.jku.at/qxbf