[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