Documentation

The on-line documentation includes the Yices manual and the API Reference

The manual describes the Yices language and type system. It explains how to download and install Yices, and how to use the different solvers included in the distributions. More documentation and many examples are also included in all the distributions.

Technical Background

Tool paper:

The basics of SMT solving:

Simplex-based arithmetic solver used by Yices:

A more advanced linear-arithmetic solver for SMT:

A technique for learning lemmas used in Yices as a preprocessing step to learn implied equalities.

Exists/forall solving with Yices and applications: