MathSAT 5

An SMT Solver for Formal Verification & More


Input Formats

The default input format for MathSAT is SMT-LIB v2. The solver accepts also SMT-LIBv1.2 and DIMACS. The input format can be selected with the -input command-line argument. In all cases, the input problem must be given on standard input.

Configurations and command-line options

MathSAT supports several options for controlling its behaviour and features in various ways. The complete list of options can be obtained with the -help command-line switch.

References and Examples

Linking the MathSAT binary against different GMP and/or libc versions

The MathSAT 5 binary is linked with the Gnu Multiprecision Library (GMP) and (on Linux) the GNU C library (glibc), both covered by the GNU LGPL license. The executable provided in the distribution is linked statically, so as to avoid potential issues with library versions. However, a MathSAT executable linked against a different version of GMP and/or libc can be obtained easily, by creating a main.c C file with the following content:

extern int msat_main(int argc, const char **argv);
int main(int argc, const char **argv) { return msat_main(argc, argv); }

and linking it against libmathsat.a, GMP and glibc. For example, using GCC this can be done as follows:

gcc main.c -o mathsat lib/libmathsat.a -lgmpxx -lgmp
Contents Home
mathsat [AT] fbk [DOT] eu
mathsat-announce mailing list