Yices 2 is a solver for
Satisfiability Modulo Theories
(SMT) problems. Yices 2 can process input written in the SMT-LIB language, or
in Yices' own specification language. The package provides a
C API.
Separately, bindings for Java,
Python,
Go, and
OCaml are available.