[ANN] release of mc2 0.1, a SMT solver

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 :slight_smile:

9 Likes