Version 0.8.0 (2021-02-24)

Features

- Support for Scala 2.12.13 (epfl-lara#913)
- Support for ghost fields in GenC (epfl-lara#904, epfl-lara#907)
- Initial support for unsigned integers in GenC (epfl-lara#888)

Bug fixes

- Fix issues watch mode (and add support for Enter key to reload) (epfl-lara#906)
- Better support for refinement types in type-checker
- Various bug fixes in extraction phases

Tag noxt-0.7.6-67-g533f5d5

Stainless Noxt 0.7.1-21-g381fb00

Stainless Noxt 0.7.1-17-ga897e90

After this commit, the counter encoding of allocation was dropped

Version 0.7.6 (2021-01-18)

Features

- Add GenC component from Leon (epfl-lara#885)
- Add frontend for more bitvector types and operations (epfl-lara#879)

Improvements

- Inox dependency is now directly on GitHub

Bug fixes

- Fix some issues in imperative phase (epfl-lara#874) and type encoding (epfl-lara#884)

Version 0.7.5 (2020-11-27)

Features

- Add `admit-vcs` option to generate VCs without sending them to the solver
- Add support for indexed types in scalac frontend

Improvements

- Generalize specification helpers (epfl-lara#828)

Bug fixes

- Remove unsound type-checking rule for function types, and add subtying rules instead

Version 0.7.4 (2020-10-02)

Bug fixes

- Fix unapplyAccessor not instantiating with refinement type (epfl-lara#841)
- Remove duplicate serializations

Version 0.7.3 (2020-09-08)

Improvements

- Remove check that measure has good type at call site (this was making arguments of recursive functions being type-checked twice, and thus duplicating VCs)
- Instead, add check that mutually recursive functions have the same measure type
- `SplitCallBack` now processes mutually recursive functions together
- Improve HTML output for type-checking derivation

Version 0.7.2 (29-08-2020)

Features

- Add `ListMap` implementation (associative list) (epfl-lara#794)

Improvements

- Remove type-checking tuple rule that was duplicating VCs (epfl-lara#792)
- Improve documentation on check/assert (epfl-lara#815)
- Add documentation for contracts on abstract functions (epfl-lara#825)

Bug fixes

- Fix `@induct` transformation for bounded-size integers (epfl-lara#804)
- Add checks to reject programs not supported by Stainless (epfl-lara#810, epfl-lara#814)
- Fix type encoding translation error (epfl-lara#818)
- Fix issues on `@inlineInvariant` feature (epfl-lara#820)
- Fix bug where Stainless could make an infinite loop in `isMutableClassType` (epfl-lara#824)
- Fix "missing field" error in watch mode (epfl-lara#829)
- Fix bug in watch mode where errors from previous runs kept getting reported (epfl-lara#830)
- Fix bug in watch mode that made the verification report incomplete (epfl-lara#831)