Hello,
I’m happy to announce the initial release 0.1 of mc2, a SMT solver in pure OCaml based on the mcSAT framework. It can handle the QF_UFLRA fragment (functions and linear rational arithmetic). It is more of a research project than a production ready solver, but has pretty acceptable performance (see for examples benchmarks on QF_UFLRA and QF_LRA with timeout=10s).
The solver is Apache licensed and weights around 7kloc (+ a few basic dependencies). Questions or comments welcome 