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.

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

Boolector incompatible #19

Closed
weaversa opened this issue Apr 9, 2022 · 4 comments
Closed

Boolector incompatible #19

weaversa opened this issue Apr 9, 2022 · 4 comments

Comments

@weaversa
Copy link
Contributor

weaversa commented Apr 9, 2022

The version of boolector provided here does not work with Cryptol-2.12.

Cryptol> :s prover=boolector
Warning: boolector installation not found
Cryptol> :s prover=w4-boolector
:s prover=w4-boolector
Warning: solver interaction failed with w4-boolector
    fd:16: hFlush: resource vanished (Broken pipe)
@RyanGlScott
Copy link
Contributor

This is almost certainly because boolector-3.2.2 (the version shipped with what4-solvers) removed its --smt2-model flag, which is a flag that what4 and sbv previously passed to boolector to determine if it was configured correctly. There have been issues opened on both the sbv issue tracker and the what4 issue tracker about this, both of which have been fixed upstream. The sbv fix is now available on Hackage in sbv-8.15 or later, so if you use a nightly version of Cryptol, then setting prover=sbv-boolector will work. The what4 fix has not yet appeared in a Hackage release, however.

If you'd prefer, I could downgrade the version of boolector used in what4-solvers to 3.2.1. That version still has the --smt2-model flag and will therefore work with old versions of what4 and sbv. Alternatively, one could wait until new versions of what4 and cryptol have been released with the appropriate fix, although that will likely take a bit longer.

@weaversa
Copy link
Contributor Author

Thanks @RyanGlScott! I'm happy to locally use the older boolector for a while. I'll watch here for when things should start working normally again.

@RyanGlScott
Copy link
Contributor

After GaloisInc/cryptol#1346, the master branch of cryptol should now support boolector-3.2.2. We'll work on making a new Cryptol release with these changes in the coming month or so.

@RyanGlScott
Copy link
Contributor

The Cryptol 2.13.0 release should work out of the box with Boolector 3.2.2. I'll close this issue under the optimistic assumption that this has been fixed, but do reopen this if you continue to experience issues.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants