Skip to content
This repository was archived by the owner on Jun 24, 2026. It is now read-only.
This repository was archived by the owner on Jun 24, 2026. It is now read-only.

Add support for Bitwuzla SMT solver #2669

Description

@dguido

Summary

Boolector has been archived and is no longer maintained. It has been succeeded by Bitwuzla, which is actively developed and provides improved performance and features.

Motivation

  • Boolector is no longer maintained (final release was 3.2.4)
  • Building Boolector from source in CI takes significant time (~2-3 minutes per job)
  • Bitwuzla is the official successor with active development
  • Bitwuzla provides prebuilt binaries, making CI installation much faster

Proposed Changes

  1. Add Bitwuzla as a supported solver option in manticore/core/smtlib/solver.py
  2. Add configuration options for Bitwuzla binary path
  3. Update documentation to mention Bitwuzla as an alternative to Boolector
  4. Consider deprecating Boolector support in a future release

Implementation Notes

  • Bitwuzla supports the same SMT-LIB2 interface as Boolector
  • Prebuilt binaries are available from: https://github.com/bitwuzla/bitwuzla/releases
  • The solver integration should be similar to the existing Boolector implementation

References

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions