- Optimize IC3/PDR engine, add experimental IC3 with implicit abstraction
- Add two modular versions of the graph-based invariant generation from PKind.
- Add path compression in k-induction
- Support Yices 1 and 2 as SMT solvers
- Optimize Lustre translation and internal term data structures
- Optimize queries to SMT solvers with check-sat with assumption instead of push/pop
- Return Lustre counterexamples faithful to input by undoing optimizations in translation
- Improve output and logging
- Many bug and performance fixes
- Web service to accept jobs from remote clients
Refer to the user documentation for more details.