HomeDocsDownloadFM Tools
Yices

Yices 1 is no longer maintained. You can still download it and use it, but we do not provide support for Yices 1.

Our more recent Yices 2 solver is here


Yices 1 Examples

These examples are not benchmarks. Their purpose is to illustrate Yices. If you are intererested in benchmarks, you should go to SMT-LIB.

Trivial

Scalars

Uninterpreted Types

Linear Arithmetic

Subtypes & Dependent Types

Booleans as Terms

Function Updates (i.e., "Array Theory")

Integer Completeness

Lambda Expressions

Tuples

Records

Bit-vectors

Inductive datatypes

Quantifiers

HomeDocsDownloadFM Tools