I'm pleased to announce v3.1 release of SBV, a library for integrating SMT solvers into Haskell. This release coincides with GHC 7.8.3: A a prior bug in the 7.8 series caused SBV to crash under heavy load. GHC 7.8.3 fixes this bug; so if you're an SBV user, please upgrade to both GHC 7.8.3 and your version of SBV. Also new in this release are two oft-requested features: - Parallel solving capabilities: Using multiple SMT solvers at the same time to get the fastest result (speed), or get all results (to make sure they all behave the same way, safety). - A variant of symbolic if-then-else (called sBranch) that can call the external solver during simulation before it symbolically simulates "then" and "else" branches. This is useful for programming with recursive functions where termination depends on symbolic values. Full release notes: https://github.com/LeventErkok/sbv/blob/master/CHANGES.md SBV web page: http://leventerkok.github.io/sbv/ As usual, bug reports and feedback are most welcome! -Levent.