I'm pleased to announce v7.0 release of SBV, a library for integrating SMT solvers into Haskell. 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.