MC2 MC² ("Model Constructing Modular Contraption") is a modular SMT solver in OCaml, based on the MCSat calculus. Documentation https://c-cube.github.io/mc2/ COPYRIGHT This program is distributed under the Apache Software License version 2.0. See the enclosed file LICENSE.