Releases Notes

Yices 2.6.5

Released June 24, 2024.

• New features:
• Arrays support in the MCSat solver.
• MCSat Thread Safety.
• New logics: QF_AUFBVLIA, QF_UFBVLIA, QF_BVLRA, QF_AUFBVNIA, QF_UFBVNIA.
• Parallel make check.
• Improved MCSat heuristics.
• New Theory-guided variable selection heuristic in the MCSat solver.
• API features:
• Set static variable order in the MCSat solver.
• Set initial variable order in the MCSat solver.
• Many bugs fixed
• See the issues on GitHub for details.
• Thanks to all people who provided feedback.

Yices 2.6.4

Released October 22, 2021.

• New features:
• Solving modulo a model in the MCSat solver
• Interpolant generation (also in MCSat)
• Support for the UF theory (uninterpreted functions with quantifiers)
• optional support for the Kissat backend SAT solver.
• Many bugs fixed
• See the issues on GitHub for details.
• Thanks to all people who provided feedback.

Yices 2.6.2

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 simplication 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 people who provided feedback.

Yices 2.6.1

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!)

Yices 2.6.0

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)

Yices 2.5.4

Released September 30, 2017.

• API Extensions: all printing and pretty-printing function now have a variant that takes a file descriptor (instead of FILE*).

Yices 2.5.3

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

Yices 2.5.2

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)

Yices 2.5.1

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 i in (bit x i) is a constant.
  • In the API: fixed bug in yices_division.
• Updates and corrections to the documentation.

Yices 2.5.0

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

Yices 2.4.2

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.

Yices 2.4.1

Released August 10, 2015.

• Fixed a bug reported by Andrew Gacek and fixed memory leaks.
• Changes to the search heuristics.

Yices 2.4.0

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.

Yices 2.3.1

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.

Yices 2.3.0

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, functions yices_bvand, yices_bvor, yices_bvxor, and yices_bvconcat now take an array of terms as argument. The binary versions of these oprerators are now called yices_bvand2, yices_bvor2, yices_bvxor2, yices_bvconcat2.

Yices 2.2.2

Released August 5, 2014.

• Fixed bugs reported by Paulo Matos and Martin Stanek.
• Preliminary support for Exists/Forall solving
• Source code available

Yices 2.2.1

Released April 1, 2014.

• Fixed a bug reported by David Cok.

Yices 2.2.0

Released February 11, 2014.

• Added support for SMT-LIB 2.0.
• More preprocessing options (including symmetry breaking for QF_UF).
• Better array solver.

Yices 2.1.0

Released August 3, 2102.

• Added support for lambda terms in definitions.
• Fixed bugs

Yices 2.0.5

Released July 26, 2012. Fixes a bug reported by Richard Uhler.

Yices 2.0.4

Released July 10, 2012.

Yices 2.0.2

Released July 5, 2102. Fixes a bug reported by Richard Uhler.

Yices 2.0.1

Released July 3, 2102. Fixes bugs reported by Richard Uhler.

Yices 2.0.0

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.