MathSAT 5

Version 5.1.6 (Apr 19, 2012)

This version adds new API functions msat_named_list_from_smtlib2 and msat_named_list_to_smtlib2 which can be used to read/write a list of terms from/to SMT-LIBv2 data.

Version 5.1.5 (Apr 4, 2012)

This version fixes a bug in computing interpolants in the combined theory QF_UFLRA, and a bug in preprocessing bit-vector formulas.

Version 5.1.4 (Mar 23, 2012)

This version fixes several bugs and adds a couple of new features.

Main bug fixes:

• Fixed bug in printing of interpolants in the SMT-LIBv2 front-end;
• Fixed bugs in inlining toplevel equalities in incremental mode;
• Fixed bug in the generation of interpolants for LA;
• Fixed several bugs in model generation, especially in conjunction with free input propagation;
• Fixed crash in the EUF solver in incremental mode;
• Fixed bugs related to theory combination in the Lazy BV solver.

New features:

• Added API functions for retrieving and examining proofs of unsatisfiability generated by MathSAT;
• Added support for interfacing MathSAT with an external Boolean unsat-core extraction tool for computing unsatisfiable cores of SMT formulas;
• Added (optional) new AIG to CNF conversion algorithm based on technology mapping;
• Added support for specifying config settings of MathSAT in SMT-LIBv2 files;
• Improved accuracy of generated debug traces;
• Significantly improved performance of model generation for large problems.

Version 5.1.3 (Dec 29, 2011)

This version fixes a couple of bugs in the SMT-LIBv2 front-end:

• Fixed bug in the get-value command with quoted symbols;
• Fixed bug in the get-interpolant command when the list of groups is empty or the produced interpolant is a single Boolean constant.

Version 5.1.2 (Dec 19, 2011)

This is identical to version 5.1.1, except that the MathSAT library has been extended to include the object code for the main function msat_main, in order to make it possible to relink the solver against a different version of the GMP and/or glibc library. (See the documentation page for more details).

Version 5.1.1 (Dec 16, 2011)

This is the first official release of MathSAT 5. It is a cleaned-up version of the solver entering SMT-COMP 2011, with some bug fixes.