boolector ☆

« Back to VersTracker

Description:
SMT solver for fixed-size bit-vectors

Type: Formula | Latest Version: 3.2.4@0 | Tracked Since: Dec 17, 2025

Links: Homepage | formulae.brew.sh

Category: Developer tools

Tags: smt-solver bit-vector formal-verification solver c-library

Install: brew install boolector

About:
Boolector is a satisfiability modulo theories (SMT) solver for bit-vectors, arrays, and uninterpreted functions. It is designed for automated reasoning tasks with a strong focus on performance and ease of integration. The tool provides a C API and Python bindings, making it suitable for both standalone use and embedding in larger verification frameworks.

Key Features:

High-performance solving for bit-vector and array logic
Incremental solving and support for assumptions
Multiple solver backends (e.g., Lingeling, CaDiCaL)
C API and Python bindings for easy integration
Supports SMT-LIB2 and BTOR formats

Use Cases:

Hardware verification and formal validation of digital circuits
Program analysis and automated test case generation
Symbolic execution and constraint solving in security research

Alternatives:

Z3 – Z3 is a general-purpose SMT solver with broader theory support; Boolector specializes in bit-precise reasoning and often excels on bit-vector problems.
MathSAT – MathSAT offers rich theory support and industrial-grade features; Boolector is open-source and optimized for bit-vectors and arrays.

License: MIT

Bottles available for: arm64_sequoia, arm64_sonoma, arm64_ventura, arm64_monterey, sonoma, ventura, monterey, arm64_linux, x86_64_linux

Version History

Detected	Version	Rev	Change	Commit
Sep 14, 2024 7:43pm		0	VERSION_BUMP	d5dd7575