IntroductionWelcome to the home page of MathSAT 5, an efficient Satisfiability modulo theories (SMT) solver. MathSAT 5 is the successor of MathSAT 4, supporting a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, and arrays) and functionalities (including e.g. computation of Craig interpolants, extraction of unsatisfiable cores, generation of models and proofs, and the ability of working incrementally). MathSAT 5 is a joint project of Fondazione Bruno Kessler and DISI-University of Trento. |