Skip to content

Add support for Bitwuzla SMT solver #2669

@dguido

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

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