HTTP/2 200 server: nginx/1.24.0 (Ubuntu) date: Fri, 16 Jan 2026 00:09:20 GMT content-type: text/html content-length: 1193 last-modified: Wed, 17 Sep 2025 08:43:57 GMT etag: "a7c-63efb3cc617c1-gzip" accept-ranges: bytes vary: Accept-Encoding content-encoding: gzip strict-transport-security: max-age=31536000; includeSubDomains

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.

Contents Home People Documentation Download Publications Links