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
Aug 24, 2024 2:48pm 0 VERSION_BUMP 1b95ecda
Sep 30, 2023 7:03am 0 VERSION_BUMP f6190e1a
Sep 12, 2023 1:36am 0 VERSION_BUMP 8e7994af
May 23, 2023 6:21pm 0 VERSION_BUMP dfd1cd9b
May 21, 2023 11:56am 0 VERSION_BUMP e9c65467
May 21, 2023 11:33am 0 NEW e1096caa
« Back to VersTracker  |  Browse Packages  |  About