Released April 6, 2020.
- Improvements for bit-vector problems
- Support for third-party backend SAT solvers CaDiCal and CryptoMiniSat
- Support for exporting from SMT-LIB2 QF_BV problems for CNF in DIMACS format
- More rewriting and simplification rules
- The MCSAT solver can now be used for bit-vector problems.
- Improvements to the SMT-LIB2 frontend (yices-smt2)
- Support for displaying models in the SMT-LIB2 format
- Option for displaying bit-vector values in the SMT-LIB2 decimal format (e.g., (_ QF bv10 4) instead of 0b1010).
- Improvements to the Yices frontend (yices)
- New command to display reduced models
- API Improvements
- Added support to export to DIMACS and solving with third-party SAT solvers
- More functions to reduce and display models
- Option to build the library for multi-threated operations
- Many bugs fixed
- See the issues on GitHub for details.
- Thanks to all the people who provided feedback.
Released October 26, 2018.
- Unsat cores are now supported by the Yices frontend.
- Python bindings improved and moved to a git submodule
- Fixed bugs reported by Rod Dockins, Marc Roig Vilamala, Iavor Diatchki, Ian Mason
- Another bug was fixed by Aman Goel (Thanks!)
Released June 30, 2018.
- Added support for unsat cores.
- MC-SAT solver now supports push/pop.
- Support more of SMT-LIB 2.5.
- Python bindings to the API.
- Fixed bugs reported by Sorav Bansal, Iavor Diatchki, Martin Bromberger, Clifford Wolf (thanks to them)
Released September 30, 2017.
- API Extensions: all printing and pretty-printing function now have a variant
that takes a file descriptor (instead of FILE*).
Released August 9, 2017.
- Fixes several bugs, included one reported by Clifford Wolf
- Fixed the Sphinx documentation to work with Sphinx 1.6
- Added an API function to check whether MC-SAT (and nonlinear arithmetic) is supported
Released February 3, 2017.
- Fixes bugs reported by Enric Carbonell and Hoang Le
- Improvements to model construction in nonlinear arithmetic
(in the presence of division by zero)
Released August 23, 2016.
- Bug fixes:
- Prints a warning when attempting to use the MCSat solver in incremental mode.
- In the Yices frontend: checks that the index
(bit x i) is a constant.
- In the API: fixed bug in
- Updates and corrections to the documentation.
Released July 28, 2016.
- Supports new logics: QF_NIA, QF_NIRA, QF_UFNRA, QF_UFNIA, QF_UFNIRA
- New command-line option to the SMT-LIB 2 frontend to give a timeout
- API updates to support division by non-constant
- Improvements to the pretty printer
Released December 11, 2015.
- Fixed a bug reported by Lifan Su.
- Fixed an issue with prompts when the stdin is not a terminal.
- Added API support to catch out-of-memory errors.
Released August 10, 2015.
- Fixed a bug reported by Andrew Gacek and fixed memory leaks.
- Changes to the search heuristics.
Released July 29, 2015.
- Added support for nonlinear arithmetic (QF_NRA).
- New arithmetic operations: abs, ceil, floor, div, mod, divides, is_int.
The SMT-LIB 2 front end now fully supports the theories Ints and Real_Ints.
- Improvements to the exists/forall solver.
- More preprocessing and various performance improvements.
Released March 30, 2015.
- Fixed bugs and other issues reported by Robert Dockins, Liana Hadarean, and David Cok.
- Updated the Mac OS X binary distribution to be compatible with Mac OS X Yosemite (Darwin 14.1.0).
- Better error reports.
Released February 10, 2015.
- Fixed bugs reported by Andrew Gacek, Heinz Riener, and Dorus Peelen.
- Better exists/forall solver
- API Changes:
- New functions to print types, terms. and models to strings.
- New functions to explore types and terms.
- More term constructors.
- More operations on models, including implicant construction and generalization.
- Changes to function names:
In an attempt to use a more consistent naming
convention for the associative operators,
yices_bvconcat now take an array of
terms as argument. The binary versions of these
oprerators are now
Released August 5, 2014.
- Fixed bugs reported by Paulo Matos and Martin Stanek.
- Preliminary support for Exists/Forall solving
- Source code available
Released April 1, 2014.
- Fixed a bug reported by David Cok.
Released February 11, 2014.
- Added support for SMT-LIB 2.0.
- More preprocessing options (including symmetry breaking for QF_UF).
- Better array solver.
Released August 3, 2102.
- Added support for lambda terms in definitions.
- Fixed bugs
Released July 26, 2012. Fixes a bug reported by Richard Uhler.
Released July 10, 2012.
Released July 5, 2102. Fixes a bug reported by Richard Uhler.
Released July 3, 2102. Fixes bugs reported by Richard Uhler.
First official Yices 2 release (May 26, 2012).
Yices 2 SMT-COMP 2009
This is an early Yices 2 prototype that participated in the SMT Solver Competition in 2009. Released October 6, 2009.