This is a release with many new features. Some highlights:

   * Support for symbolic sum-types: Maybe/Either. (Thanks to Joel Burget for initiating these.)

   * Support for symbolic sets.

   * Support for uninterpreted-function values in models.

   * Support for validation of models coming from SMT-solvers for high-assurance.

   * An implementation of Dijkstra's weakest-precondition logic and a toy language for showing how to do Hoare style total-correctness proofs in SBV.

   * A new and better interface to the optimization engine supporting arbitrary metric spaces.

    * A bunch of other fixes, improvements, and examples.

Full release notes are here: https://github.com/LeventErkok/sbv/blob/master/CHANGES.md

  Hackage: https://hackage.haskell.org/package/sbv

  Homepage: http://leventerkok.github.io/sbv/

Feedback and bug reports are most welcome. Happy proving!

-Levent.