Skip to content

Support Bitwuzla #1786

@RyanGlScott

Description

@RyanGlScott

We should add support for the Bitwuzla SMT solver in Cryptol, which offers efficient reasoning over bit-vectors, floating-points, arrays and uninterpreted functions. Both What4 and SBV now support Bitwuzla, so we should be able to add Bitwuzla support in Cryptol relatively easily.

Metadata

Metadata

Assignees

No one assigned

    Labels

    feature requestAsking for new or improved functionality

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions