This release adds incremental solving capabilities to SBV: Users can now interact with the underlying solver using a typed API capturing the SMTLib language, issuing commands, getting model values, and asserting further constraints on-the-fly. The possibility of issuing multiple check-sat commands allows incremental assertion of facts, a key feature of modern constraint solving systems.

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

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

  Release notes: https://github.com/LeventErkok/sbv/blob/master/CHANGES.md

  SMTLib initiative: http://smtlib.cs.uiowa.edu/

Feedback and bug reports are most welcome!

-Levent.