Yices-2.6.5

Yices 2.6.5

New Features:

• Arrays support in the MCSat solver
• MCSat Thread Safety
• New logics: QF_AUFBVLIA, QF_UFBVLIA, QF_BVLRA, QF_AUFBVNIA, QF_UFBVNIA
• Set static variable order in the MCSat solver
• Set initial var order in the MCSat solver
• Parallel make check
• Plugin decision hint queue in the MCSat solver

Many fixes

Yices-2.6.4

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

Yices-2.6.3

This is a release candidate for 2.6.4. It reports itself as 2.6.4, so once we are happy with it we can just call it 2.6.4 without further futzing with the code.

2021-02-19

Merge pull request #348 from kquick/yices_abort

Adds --abort-on-int cmdline flag to yices executable.

Yices-2.6.2

New features

• support for bit-vectors in MCSAT
• optional use of CaDiCaL or CryptoMiniSAT as backend SAT solvers
• more flexibility in displaying models (for yices-smt2)
• new command in the yices-language frontend to reduce models
• export SMT-LIB2 bit-vector problems to DIMACS
• API improvements

Many bug fixed

Yices-2.6.1

New features:

• Bug fixes.
• Unsat core supported by the Yices front end.
• The python bindings are now a git submodule, and have been updated and improved.

Yices-2.6.0

New features:

• unsat cores
• push/pop now supported by the MC-SAT solver
• improved support for SMT-LIB 2.5
• various fixes

Yices-2.5.4

This release will be used to upload new packages to the our ppa

Yices-2.5.3

Released August 9, 2017.

This is to synchronize with our debian packages.

Yices-2.5.2

Released February 3, 2017.