SlackBuilds Repository

15.0 > Academic > yices2 (2.6.4)

  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.

Yices 2 can process input written in the SMT-LIB notation (both
versions 2.0 and 1.2 are supported). Alternatively, you can write
specifications using Yices 2's own specification language, which
includes tuples and scalar types. You can also use Yices 2 as a
library in your software.

If you want to enable non-linear real and integer arithmetic
set MCSAT=yes, this requires libpoly and libcudd.

Maintained by: William PC
Keywords: satisfiability modulo theories solver,SMT solver
ChangeLog: yices2


Source Downloads:
yices-2.6.4-src.tar.gz (6863fb6c44345e4b72490d16a7ee9f27)

Download SlackBuild:
yices2.tar.gz.asc (FAQ)

(the SlackBuild does not include the source)

Individual Files:

Validated for Slackware 15.0

See our HOWTO for instructions on how to use the contents of this repository.

Access to the repository is available via:
ftp git cgit http rsync

© 2006-2023 Project. All rights reserved.
Slackware® is a registered trademark of Patrick Volkerding
Linux® is a registered trademark of Linus Torvalds