Yices

Yices 2 is an SMT solver that decides the satisfiability of formulas containing uninterpreted function symbols with equality, real and integer arithmetic, bitvectors, scalar types, and tuples. Yices 2 supports both linear and nonlinear arithmetic.

More Information

For more information visit the Yices website.

Available Versions

These versions of Yices are available on the BEAR systems (BlueBEAR and BEAR Cloud VMs). These will be retained in accordance with our Applications Support and Retention Policy.

Version	BEAR Apps Version
2.6.4-GCCcore-12.2.0	2022b
2.6.2-GCCcore-10.2.0	2020b