search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
243 stars 34 forks source link

Use int2bv if available #561

Closed LeventErkok closed 4 years ago

LeventErkok commented 4 years ago

@MrChico

CVC4 and z3 support int2bv out-of-the box.

Yices and mathsat require manual translation.

dReal doesn't support bit-vectors, and abc doesn't support unbounded integers; so no support at all for those two.

We should do this via a solver-capability, picking the correct translation.

LeventErkok commented 4 years ago

@MrChico

Just pushed some changes which should use the native version if available. Give it a shot and let me know if it works as expected. Thanks!

MrChico commented 4 years ago

Thanks @LeventErkok , this seems to work well!

LeventErkok commented 4 years ago

Great. Thanks!