OptiMathSAT: a tool for optimization modulo theories. Welcome to the home page of OptiMathSAT, an efficient Optimization Modulo Theories (OMT) tool. OptiMathSAT is an extension of MathSAT 5 and is available at the same licence conditions as MathSAT 5. OptiMathSAT allows for incremental multi-objective optimization over linear arithmetic objective functions, it supports a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, arrays). Like MathSAT 5, OptiMathSAT is a joint project of Fondazione Bruno Kessler and DISI-University of Trento.