Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Support Bitwuzla #2172

Open
RyanGlScott opened this issue Jan 7, 2025 · 0 comments · May be fixed by #2173
Open

Support Bitwuzla #2172

RyanGlScott opened this issue Jan 7, 2025 · 0 comments · May be fixed by #2173
Assignees
@RyanGlScott
Labels
type: feature request Issues requesting a new feature or capability
Milestone
2025T1

Comments

@RyanGlScott
Copy link
Contributor

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 SAW relatively easily.

See GaloisInc/cryptol#1786 and GaloisInc/crucible#1269 for the corresponding Cryptol and Crucible issues.
@RyanGlScott RyanGlScott added the type: feature request Issues requesting a new feature or capability label Jan 7, 2025
@RyanGlScott RyanGlScott added this to the 2025T1 milestone Jan 7, 2025
@RyanGlScott RyanGlScott self-assigned this Jan 7, 2025
RyanGlScott added a commit that referenced this issue Jan 7, 2025
@RyanGlScott
Add Bitwuzla support
902cabf 
Bumps the following submodules to bring in Bitwuzla-related changes:

* GaloisInc/cryptol#1786
* GaloisInc/crucible#1270

Fixes #2172.
RyanGlScott added a commit that referenced this issue Jan 9, 2025
@RyanGlScott
Add Bitwuzla support
bd095a4 
Bumps the following submodules to bring in Bitwuzla-related changes:

* GaloisInc/cryptol#1786
* GaloisInc/crucible#1270

Fixes #2172.
@RyanGlScott RyanGlScott linked a pull request Jan 9, 2025 that will close this issue
Draft
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@RyanGlScott RyanGlScott

Labels
type: feature request Issues requesting a new feature or capability
Projects
None yet
Milestone
2025T1
Development

Successfully merging a pull request may close this issue.

Add Bitwuzla support GaloisInc/saw-script
1 participant
@RyanGlScott