An Optimization Modulo Theories (OMT) tool

SMT-LIBv2 Extensions

Note: OptiMathSAT now requires -optimization=true to be set in order to use the optimization interface. If that option is not set, OptiMathSAT behaves as MathSAT.

OptiMathSAT (>= 1.7.0) accepts a modified version of SMT-LIBv2 input format, extended as follows: The input problem must be given to OptiMathSAT on standard input:
~$ ./optimathsat < FILENAME.smt2