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.
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.
ddSMT
ddSMT serves as an input minimizer for Sat Modulo Theories (SMT) benchmarks in SMT-LIB v2 format and its dialects and extensions.
Murxla
A modular and highly extensible model-based API Fuzzer for SMT Solvers.
BTOR2Tools
A generic parser and tool package for the BTOR2 format.
QBFcert
QBFcert is a framework for resolution-based extraction and validation of certificates for Quantified Boolean Formulas (QBF).