search

GaloisInc / what4-solvers

Multi-platform binary creation for solvers of the versions most suitable for use with What4
5 stars 1 forks source link

Boolector incompatible #19

Closed weaversa closed 2 years ago

weaversa commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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.