MathSAT（http://mathsat.fbk.eu）是一款高效的SMT约束求解器，目前由Fondazione Bruno Kessler和DISI-University of Trento联合开发和维护。