Issues · Why3 / why3 · GitLab

Allow "use ghost Foo"

#246 · opened Nov 30, 2018 by Guillaume Melquiond To be discussed component: core component: extraction component: syntax feature wish
- 0
updated May 21, 2019
Division and comparison in SMT and Alt-ergo

#242 · opened Nov 26, 2018 by François Bobot
- 1
updated Nov 26, 2018
Improve apply

#233 · opened Nov 07, 2018 by DAILLER Sylvain component: transformations
- 0
updated Nov 07, 2018
Add warning to anonymous function without ensures

#230 · opened Nov 07, 2018 by DAILLER Sylvain
- 0
updated Nov 07, 2018
Adding location to SP generated variables

#229 · opened Nov 06, 2018 by DAILLER Sylvain component: wp
- 2
updated Nov 07, 2018
ieee_float library

#228 · opened Oct 30, 2018 by DAILLER Sylvain priority: low
- 3
updated Oct 30, 2018
syntax function in extraction drivers

#222 · opened Oct 24, 2018 by Jean-Christophe Filliâtre Hackathon
- 1
updated May 21, 2019
IDE: should display the right source file in case of syntax or typing error

#218 · opened Oct 23, 2018 by MARCHE Claude 1.3.0
- 0
updated Feb 11, 2019
Extraction des foncteurs 0 of 3 tasks completed

#215 · opened Oct 19, 2018 by François Bobot
- 2
updated Oct 19, 2018
Imprecise error for record with invariant

#213 · opened Oct 18, 2018 by DAILLER Sylvain
- 4
updated Jul 15, 2019
Questions on labels

#211 · opened Oct 15, 2018 by DAILLER Sylvain
- 9
updated Dec 17, 2018
Syntax of drivers is not documented

#204 · opened Oct 10, 2018 by DAILLER Sylvain documentation
- 0
updated Oct 10, 2018
Document syntax of clone

#202 · opened Oct 10, 2018 by DAILLER Sylvain documentation
- 0
updated Nov 13, 2018
Document extraction of clonable/cloned modules

#201 · opened Oct 09, 2018 by MARCHE Claude
- 2
updated Jan 28, 2019
Interaction of smt encoding with meta

#196 · opened Oct 03, 2018 by DAILLER Sylvain component: transformations feature wish priority: low
- 2
updated Oct 04, 2018
usage of array.Array should not enforce polymorphic VCs

#193 · opened Oct 02, 2018 by MARCHE Claude
- 0
updated Oct 02, 2018
Miscellaneous feature wishes for discussion

#176 · opened Aug 29, 2018 by BECKER Benedikt feature wish
- 10
updated Aug 31, 2018
Extraction of absurd

#171 · opened Aug 29, 2018 by MARCHE Claude Hackathon feature wish
- 4
updated May 21, 2019
Cloning function with bad ghost status raises Invalid_argument("Expr.let_rec")

#168 · opened Aug 24, 2018 by PARREIRA PEREIRA Mário José 1.3.0
- 6
updated Feb 08, 2019
"use" in drivers is done too late

#156 · opened Jul 04, 2018 by Andrei Paskevich
- 11
updated Jul 23, 2018