Issues · Why3 / why3 · GitLab

destruct/case transformations incorrectly handle polymorphic formulas

#525 · created Jan 14, 2021 by Quentin Garchery 1.4.0 component: transformations soundness
- CLOSED
- 1
- 4
updated Jul 13, 2021
Hide does not work

#405 · created Oct 31, 2019 by DAILLER Sylvain component: transformations
- CLOSED
- 1
- 0
updated Nov 04, 2019
`apply with` and `rewrite with` should give more details (e.g., quantifier names) when the number of arguments do not match

#399 · created Oct 25, 2019 by Guillaume Melquiond component: transformations
- CLOSED
- 1
- 2
updated Oct 28, 2019
List transformation with arguments and documentation

#380 · created Sep 03, 2019 by DAILLER Sylvain component: transformations
- CLOSED
- 17
updated Nov 22, 2019
Why3 should not introduce spaces in identifiers

#377 · created Aug 22, 2019 by DAILLER Sylvain component: transformations
- CLOSED
- 1
- 1
updated Aug 23, 2019
Trivial goals are not user-friendly

#367 · created Jul 15, 2019 by Guillaume Melquiond component: session component: transformations
- CLOSED
- 5
updated Dec 04, 2019
Incorrect goal location after splitting.

#366 · created Jul 11, 2019 by Guillaume Melquiond component: graphical user interface component: transformations
- CLOSED
- 1
- 11
updated Jul 16, 2019
induction_ty_arg_lex expected behavior

#280 · created Mar 01, 2019 by DAILLER Sylvain component: transformations
- CLOSED
- 1
- 0
updated Mar 26, 2019
transformation replace should replace also under the conditions of `if`

#269 · created Feb 05, 2019 by MARCHE Claude 1.3.0 component: transformations
- CLOSED
- 4
updated Feb 12, 2019
destruct improvement with if then else

#264 · created Jan 31, 2019 by DAILLER Sylvain component: transformations
- CLOSED
- 2
- 2
updated Feb 08, 2019
Removing Inline_trivial

#263 · created Jan 31, 2019 by DAILLER Sylvain component: drivers component: transformations
- CLOSED
- 1
- 0
updated Feb 12, 2019
improve destruct_alg

#259 · created Jan 28, 2019 by MARCHE Claude component: transformations
- CLOSED
- 1
- 2
updated Jan 31, 2019
Improve case transformation

#238 · created Nov 14, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated Jun 18, 2019
Avoid substituting to proxy symbols

#235 · created Nov 13, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 2
updated Nov 16, 2018
instantiate should be able to remove the general hypothesis

#232 · created Nov 07, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated Sep 24, 2019
Add a transformation destruct*

#231 · created Nov 07, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 5
updated Nov 08, 2018
Restricting behavior of rewrite_list

#226 · created Oct 29, 2018 by DAILLER Sylvain component: transformations priority: low
- CLOSED
- 2
updated Nov 07, 2018
--list-transform should print all transformations

#210 · created Oct 12, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 0
updated Nov 13, 2018
New split_vc sometimes crashes

#195 · created Oct 02, 2018 by Raphaël Rieu-Helft 1.1.0 component: transformations
- CLOSED
- 4
updated Oct 05, 2018
Modify split_vc to not use simplify_trivial_quantification

#188 · created Sep 28, 2018 by Raphaël Rieu-Helft 1.1.0 component: transformations
- CLOSED
- 1
- 0
updated Oct 04, 2018

Prev
1
2
3
Next