# Install yices2 with Homebrew, apk, dnf, MacPorts, Nix, pacman Yices SMT Solver. Version 2.7.0 via Homebrew; verified 2026-06-24. ## Install ```sh sudo av install brew:yices2 ``` Additional install commands: ### macOS - Homebrew (100%): ```sh brew install yices2 ``` Evidence: local Homebrew formula metadata - MacPorts (94%): ```sh sudo port install yices ``` Evidence: MacPorts ports tree: math/yices/Portfile from https://api.github.com/repos/macports/macports-ports/git/trees/master?recursive=1 ### Linux - apk (92%): ```sh sudo apk add yices2 ``` Evidence: Alpine Linux edge package indexes: yices2 from https://dl-cdn.alpinelinux.org/alpine/edge/testing/x86_64/APKINDEX.tar.gz - dnf (92%): ```sh sudo dnf install yices ``` Evidence: Fedora Rawhide package metadata: yices from https://dl.fedoraproject.org/pub/fedora/linux/development/rawhide/Everything/x86_64/os/repodata/e5ca8ce900cd68f5419e1c39ae517343100b306336cbaeb70a3c153121d95094-primary.xml.zst - Nix (92%): ```sh nix profile install nixpkgs#yices ``` Evidence: nixpkgs package indexes: pkgs/by-name/yi/yices/package.nix from https://api.github.com/repos/NixOS/nixpkgs/git/trees/master?recursive=1 - pacman (92%): ```sh sudo pacman -S yices ``` Evidence: Arch Linux sync databases: yices from https://geo.mirror.pkgbuild.com/extra/os/x86_64/extra.db.tar.gz ## Package facts - **Package key:** brew:yices2 - **Package manager:** Homebrew - **Package manager page:** - **Version:** 2.7.0 - **Source summary:** Yices SMT Solver - **Homepage:** - **Repository:** - **Upstream docs:** - **License:** GPL-3.0-or-later - **Source archive:** - **Last updated:** 2026-06-24T17:21:57-04:00 - **Generated:** 2026-07-08T07:18:31+00:00 ## Executables - yices (cli) - yices-sat (cli) - yices-smt (cli) - yices-smt2 (cli) - yices (alias) - yices-sat (alias) - yices-smt (alias) - yices-smt2 (alias) ## Dependencies - gmp ## Build dependencies - autoconf ## Install behavior - Post-install hook: not defined - Bottle: available on arm64_linux, arm64_sequoia, arm64_sonoma, arm64_tahoe, arm64_ventura, sonoma, ventura, x86_64_linux ## Freshness - Page generated: 2026-07-08 - Package-manager version: 2.7.0 - Package-manager updated: 2026-06-24 - Local data: ok - Upstream repository: https://github.com/SRI-CSL/yices2 - info: No cached GitHub release or tag data was available. ## Project history and usage Yices 2 is SRI International's open-source SMT solver for satisfiability modulo theories. It supports SMT-LIB input, its own Yices language, a C API, and language bindings for Java, Python, Go, and OCaml. ### Project history Yices comes from SRI International's Computer Science Laboratory and the formal-methods lineage around Bruno Dutertre and collaborators. The Yices web site says Yices 2 decides formulas over uninterpreted functions with equality, real and integer arithmetic, bitvectors, scalar types, and tuples, including linear and nonlinear arithmetic. The documentation page anchors Yices 2 in the SMT research literature: the Yices 2.2 tool paper was presented at CAV 2014, while related technical background includes SMT tutorials, arithmetic-solver papers, MCSAT work, and applications to exists/forall problems and synthesis. The GitHub repository was created in November 2014 and contains source, documentation, tests, and examples. Later release notes show continuing solver work: unsat cores and SMT-LIB 2.5 support in 2.6.0, bit-vector support and optional SAT backends in 2.6.2, interpolation and Kissat backend support in 2.6.4, arrays and thread-safety work in 2.6.5, and finite-field support in 2.7.0. ### Adoption history Yices 2 is adopted in the formal-methods and verification world rather than as an end-user desktop CLI. Its official site documents installation with Homebrew on macOS and apt on Debian/Ubuntu via SRI's formal-methods PPA, and the repository provides examples plus multiple language bindings for embedding. For package managers, Yices 2 matters because it is both a command suite and a native library. The README distinguishes executables, dynamic library, headers, source builds, optional MC-SAT support, and optional thread-safety builds. ### How it is used Typical CLI usage feeds SMT-LIB files to yices-smt2 and asks for satisfiability and models. The README includes examples for linear real arithmetic, bit-vectors, and nonlinear real arithmetic, all producing sat models. Advanced users can embed the C API or use language bindings, build documentation, enable MC-SAT for nonlinear arithmetic and theory combination, run a portfolio script over hard SMT2 problems, or build a thread-safe library configuration when separate contexts are used per thread. ### Why package nerds care Yices 2 is a heavyweight scientific package with a deceptively small command-line surface. Package maintainers care about it because optional solver backends, headers, libraries, bindings, documentation, and platform binaries all affect whether downstream verification tools can rely on the installed package. It also illustrates a common formal-methods packaging pattern: research-grade solver, command-line frontends, C library, SMT-LIB compatibility, and cross-language bindings all distributed from one upstream. ### Timeline - 2006: SRI-related linear-arithmetic solver papers form part of the technical background documented by Yices. - 2014: Yices 2.2 tool paper presented at CAV and the public yices2 GitHub repository created. - 2017-08: Yices 2.5.3 release synchronized with Debian packages. - 2018-06: Yices 2.6.0 adds unsat cores and improved SMT-LIB 2.5 support. - 2020-04: Yices 2.6.2 adds bit-vector support in MCSAT and optional SAT backends. - 2021-10: Yices 2.6.4 stable release published. - 2024-06: Yices 2.6.5 adds arrays support in MCSAT and thread-safety work. - 2025-07: Yices 2.7.0 adds finite-field support and MCSAT improvements. ### Related projects - SMT-LIB: standard input language supported by Yices 2. - libpoly and CUDD: optional dependencies documented for MC-SAT builds. - CaDiCaL, CryptoMiniSAT, and Kissat: optional SAT backend families mentioned in release notes. - SRI formal-methods tools: adjacent tools distributed by SRI's Computer Science Laboratory. ### Sources - - - - - ## Security Notes narrow executable package without higher-risk signals. - **Geiger risk:** green / low - narrow executable package without higher-risk signals ## Source Database Details - **Source Database:** Homebrew formula API - **Tap:** homebrew/core - **Full Name:** yices2 - **Version Scheme:** 0 - **Revision:** 0 - **Head Version:** HEAD - **Bottle Stable Root URL:** - **Deprecated:** no - **Disabled:** no - **Keg Only:** no - **URL Keys:** head, stable ## Other Package-Manager Records - apk - yices2 - 2.6.5-r0: normalized package name match | Alpine Linux edge package indexes: yices2 from https://dl-cdn.alpinelinux.org/alpine/edge/testing/x86_64/APKINDEX.tar.gz | Solver for Satisfiability Modulo Theories (SMT) problems | https://github.com/SRI-CSL/yices2 - apk - yices2-dev - 2.6.5-r0: normalized package name match | Alpine Linux edge package indexes: yices2-dev from https://dl-cdn.alpinelinux.org/alpine/edge/testing/x86_64/APKINDEX.tar.gz | Solver for Satisfiability Modulo Theories (SMT) problems (development files) | https://github.com/SRI-CSL/yices2 - apk - yices2-libs - 2.6.5-r0: normalized package name match | Alpine Linux edge package indexes: yices2-libs from https://dl-cdn.alpinelinux.org/alpine/edge/testing/x86_64/APKINDEX.tar.gz | Solver for Satisfiability Modulo Theories (SMT) problems (libraries) | https://github.com/SRI-CSL/yices2 - MacPorts - yices: installed executable or alias match | MacPorts ports tree: math/yices/Portfile from https://api.github.com/repos/macports/macports-ports/git/trees/master?recursive=1 - Nix - yices: installed executable or alias match | nixpkgs package indexes: pkgs/by-name/yi/yices/package.nix from https://api.github.com/repos/NixOS/nixpkgs/git/trees/master?recursive=1 - dnf - yices - 2.7.0-8.fc45: installed executable or alias match | Fedora Rawhide package metadata: yices from https://dl.fedoraproject.org/pub/fedora/linux/development/rawhide/Everything/x86_64/os/repodata/e5ca8ce900cd68f5419e1c39ae517343100b306336cbaeb70a3c153121d95094-primary.xml.zst | SMT solver | http://yices.csl.sri.com/ - dnf - yices-devel - 2.7.0-8.fc45: installed executable or alias match | Fedora Rawhide package metadata: yices-devel from https://dl.fedoraproject.org/pub/fedora/linux/development/rawhide/Everything/x86_64/os/repodata/e5ca8ce900cd68f5419e1c39ae517343100b306336cbaeb70a3c153121d95094-primary.xml.zst | Development files for yices | http://yices.csl.sri.com/ - dnf - yices-doc - 2.7.0-8.fc45: installed executable or alias match | Fedora Rawhide package metadata: yices-doc from https://dl.fedoraproject.org/pub/fedora/linux/development/rawhide/Everything/x86_64/os/repodata/e5ca8ce900cd68f5419e1c39ae517343100b306336cbaeb70a3c153121d95094-primary.xml.zst | Documentation for yices | http://yices.csl.sri.com/ - dnf - yices-tools - 2.7.0-8.fc45: installed executable or alias match | Fedora Rawhide package metadata: yices-tools from https://dl.fedoraproject.org/pub/fedora/linux/development/rawhide/Everything/x86_64/os/repodata/e5ca8ce900cd68f5419e1c39ae517343100b306336cbaeb70a3c153121d95094-primary.xml.zst | Command line tools that use the yices library | http://yices.csl.sri.com/ - pacman - yices - 2.7.0-1: installed executable or alias match | Arch Linux sync databases: yices from https://geo.mirror.pkgbuild.com/extra/os/x86_64/extra.db.tar.gz | A solver for Satisfiability Modulo Theories (SMT) problems | https://yices.csl.sri.com/ ## Related links - [Terminal utility packages](https://www.automicvault.com/pkg/terminal-utilities/) - Matched terminal and command-line workflow metadata. - [Networking and protocol packages](https://www.automicvault.com/pkg/networking-protocol-tools/) - Matched network, protocol, or remote-service metadata. - [Scientific computing packages](https://www.automicvault.com/pkg/scientific-computing-tools/) - Matched scientific computing metadata. - [Homebrew utility packages](https://www.automicvault.com/pkg/brew-utility-packages/) - Matched Homebrew package provider. - [autoconf](https://www.automicvault.com/pkg/brew/autoconf/) - Build dependency declared by Homebrew. - [z3](https://www.automicvault.com/pkg/brew/z3/) - Shares av.db curated category or tags: cli, formal-methods, science, smt-solver. - [acl2](https://www.automicvault.com/pkg/brew/acl2/) - Shares av.db curated category or tags: cli, formal-methods, science. - [depqbf](https://www.automicvault.com/pkg/brew/depqbf/) - Shares av.db curated category or tags: cli, formal-methods, science. - [ltl2ba](https://www.automicvault.com/pkg/brew/ltl2ba/) - Shares av.db curated category or tags: cli, formal-methods, science. - [ott](https://www.automicvault.com/pkg/brew/ott/) - Shares av.db curated category or tags: cli, formal-methods, science. - [rocq](https://www.automicvault.com/pkg/brew/rocq/) - Shares av.db curated category or tags: cli, formal-methods, science. - [rocq-elpi](https://www.automicvault.com/pkg/brew/rocq-elpi/) - Shares av.db curated category or tags: cli, formal-methods, science. - [cadical](https://www.automicvault.com/pkg/brew/cadical/) - Shares av.db curated category or tags: cli, formal-methods, science. ## Combined YAML source View the package source record on GitHub. [combined/yices2.yml](https://github.com/automic-vault/db/blob/main/combined/yices2.yml) ## Sources - Nucleus package database - Geiger risk classifier - package-page enrichment - curated package history - package version freshness - av.db category and tag curation - package relationship graph - external package-manager database matches - cross-ecosystem install command graph