New release of SBV (0.9.22) is out: http://hackage.haskell.org/package/sbv Major changes in this release are: - Support for explicit quantification (including alternating existentials and universals) - Ability to use Microsoft's Z3 SMT solver (in addition to Yices). Full release notes: http://github.com/LeventErkok/sbv/blob/b75fb082c013ae9612ef09b90d5feeaec6527... Thanks, -Levent.