A fuzzing framework for SMT solvers

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction

TouIST, the IDE & Language for Logic (backed by SAT, SMT and QBF solvers)

Specify satisfiability modulo theories problems in Julia and use the SMT-LIB format to interact with SMT solvers.

A frontend for multiple SMT solvers in OCaml

The Princess Theorem Prover

A constraint solver built from scratch in OCaml

An SMT-LIB formatter.

SMTLIB benchmarks assembled by Florian Schanda

Find soundness bugs in SMT solvers through equivalent transformations

SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces

output SMT syntax from Guile

Arbitrary precision IEEE-754 implementation in Python for generating SMTLIB float benchmarks

Combinatorial and Decision Making Optimization (CDMO) project during the A.Y. 2021/2022.

A generator for Semantic Fusion

simple java API for interaction with SMT solvers using SMT-LIB

A tool to translate regular expressions to smt-lib constraints

Parse smt2 in Haskell

A translator from TPTP to SMT-LIB

SMT-LIB v2 Parser