PV4 Yicesproduces a satisfiability result for a formula

Application domain/field

Type of tool

SMT solver

Expected input

SMT formula


SMT-LIB(version 1.2 and 2.0), or its own specification language. It also has a C API and bindings for Java, Python, Go and OCaml.

Expected output

sat if the problem is satisfiable, unsat if it is not satisfiable or unknown if the solver does not terminate within a fixed number of iterations. If the formula can be satisfied, then you can ask Yices for a satisfying model.


License: GPLv3


Related papers

Interpolation and Model Checking for Nonlinear Arithmetic (CAV '21)

Last publication date

15 July 2021

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.