A new release of SBV is out (v4.1): http://hackage.haskell.org/package/sbv-4.1 The main change in this release is the connection to Berkeley's ABC http://www.eecs.berkeley.edu/~alanmi/abc/ system, which is an industrial strength synthesis and verification system. SBV can now generate proof goals that are discharged by ABC, using state-of-the-art SAT based techniques. ABC is especially extremely well-tuned for dealing with problems in the bit-vector theory, and is heavily used in the hardware industry as a backend verification tool. Also included in this release is better support for IEEE-floats, and a reworked implementation of the connection to the Boolector http://fmv.jku.at/boolector/ solver. Thanks to Adam Foltzer of Galois for contributing the connection to ABC, and Alan Mischenko from Berkeley to add the necessary infrastructure to ABC to allow for this bridge to be built. Full release notes: https://github.com/LeventErkok/sbv/blob/master/CHANGES.md SBV web page: http://leventerkok.github.io/sbv/ -Levent.