Issues · Why3 / why3 · GitLab

Machine integers and range types

#29 · created Nov 09, 2017 by Guillaume Melquiond 1.0.0 component: theories component: wp
- CLOSED
- 1
updated Feb 02, 2018
No default order for range types

#56 · created Dec 14, 2017 by Guillaume Melquiond component: wp
- CLOSED
- 0
updated Sep 14, 2018
Variants and soundness guarantees

#57 · created Dec 15, 2017 by Guillaume Melquiond component: wp soundness
- CLOSED
- 0
updated Jun 13, 2018
Make `any ... ensures` less error-prone

#136 · created Jun 15, 2018 by Guillaume Melquiond 1.0.0 component: wp
- CLOSED
- 2
updated Jun 22, 2018
Cloning part of mutable structure

#258 · created Jan 28, 2019 by François Bobot component: theories component: wp
- CLOSED
- 1
updated Jan 28, 2019
Extend witness grammar for type invariant

#286 · created Mar 26, 2019 by François Bobot component: wp
- CLOSED
- 1
- 9
updated Apr 24, 2021
Add `(e at label)` as acceptable ghost code

#307 · created Apr 19, 2019 by François Bobot component: wp feature wish
- CLOSED
- 6
updated Apr 20, 2019
Lost location for function argument

#344 · created Jun 11, 2019 by DAILLER Sylvain component: wp
- CLOSED
- 4
updated Mar 14, 2022
Location of `variant` clause

#348 · created Jun 18, 2019 by DAILLER Sylvain component: counterexample component: wp
- CLOSED
- 1
updated Jun 19, 2019
Clone problem when type has nested regions

#468 · created Mar 25, 2020 by Mário Pereira component: wp
- CLOSED
- 5
updated Mar 27, 2020