Not really usable as a fully fledged SMT solver right now. Mainly just a collection of various algorithms used in SMT solvers, implemented in Haskell: SAT solving Davis–Putnam–Logemann–Loveland (DPLL) Conflict Driven Clause Learning (CDCL) Uninterpreted Functions Congruence Closure Linear Arithmatic Simplex Method Fourier-Motzkin Branch and Bound Non-Linear Arithmatic Interval Constraint Propagation Subtropical Satisfiability Cylindtrical Algebraic Decomposition Virtual Substitution