Introduction
Welcome 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.
|
![mathsat [AT] fbk [DOT] eu](email.png)