Features
- Support for type members in local classes (#633)
- Report functions with missing positions in PositionChecker (#639)
- Add AmortizedQueue data structure to Stainless library (#635)
- Add debug section to show the full VC before simplification (#637)
- Add script to run tests on stainless-actors and bolts (#623)
- Ignore @library flag on typeclasses which have non-library subclasses (#595)
- Enable -feature and -unchecked scalac flags in embedded compiler (#610)
- Enforce sound equality tests (#605, #609)
- Port partial specification feature from Leon (#438)
- Add BoundedQuantifiers module to the library (#596)
Improvements
- Propagate @ghost annotation to variables introduced by calls to default copy getter (#643)
- Do not lift refinement into pre-/post-conditions when
--type-checkeris enabled (#620) - Follow symbolic links when searching for base directory (#621)
- Check that methods are only overriden by methods with the same ghostiness (#615)
- Check that required tools are installed before packaging (#599)
- Add readability check for jars in script (#600)
Bug fixes
- Add missing serializer for LocalThis (#631)
- Fix malformed case object constructor method (#641)
- Use triple quotes and escape \u for extraClasspath and extraCompilerArguments (#626)
- Fix bug in AssertionInjector where unary minus was lost in strict arithmetic mode (#630)
- Fix DottyVerificationSuite not being run (non-initialized folder) (#627)
- Fix bug where anonymous inner classes would have same identifier (#619)
- Fix handling of super calls in case objects (#618)
- Fix a bunch of issues with type members (#580)