yices2 ☆

« Back to VersTracker

Description:
Yices SMT Solver

Type: Formula | Tracked Since: Dec 28, 2025

Links: Homepage | formulae.brew.sh

Category: Developer tools

Tags: smt solver verification formal-methods logic

Install: brew install yices2

About:
Yices2 is a high-performance SMT solver developed by SRI International. It determines the satisfiability of logical formulas expressed in various theories, including bit-vectors, arrays, and uninterpreted functions. The tool is widely used in formal verification to check the correctness of hardware and software systems.

Key Features:

Supports SMT-LIB 2.x input format
High-performance solving engine
Supports multiple theories (QF_AUFBV, etc.)
Provides a C API for integration
Command-line interface for interactive use

Use Cases:

Formal verification of software and hardware systems
Automated theorem proving
Constraint solving for program analysis

Alternatives:

Z3 – Z3 is another popular SMT solver with broader language bindings and a wider range of supported theories out of the box.
CVC5 – CVC5 is a modern solver that often competes with Yices2, offering strong performance on standard benchmarks.

Version History

Detected	Version	Rev	Change	Commit
Sep 11, 2025 8:54am		0	VERSION_BUMP	1b2b84e0