[SMT-LIB] Yices 2.4.0 released

Bruno Dutertre bruno.dutertre at sri.com
Wed Jul 29 20:05:05 EDT 2015


We are pleased to announce the latest release of Yices.

Highlights:

- This new release includes support for QF_NRA (nonlinear
   real arithmetic).

- Yices now supports all arithmetic operators in the
   Ints and Real_Ints theory (include div/mod/abs etc.)

- New solver for exists/forall problems[1].

This is the version we entered in the SMT Competition.
(Yices won 11 division in the main track and 6 in
the application track).

Please visit http://yices.csl.sri.com for download
and more information.

Bruno

[1] http://smt2015.csl.sri.com/wp-content/uploads/2015/06/2015-Dutertre-Solving-Exists-Forall-Problems-With-Yices.pdf



More information about the SMT-LIB mailing list