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 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
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
Murxla is a modular and highly extensible, model-based API Fuzzer for SMT solvers. Murxla randomly generates valid sequences of solver API calls based on a customizable API model, with full support for the semantics and features of SMT-LIB. https://murxla.github.io https://github.com/murxla/murxla