Issues · Why3 / why3 · GitLab

improve destruct_alg

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

#88 · created Feb 14, 2018 by Guillaume Melquiond component: graphical user interface component: transformations feature wish
- CLOSED
- 5
updated Aug 29, 2018
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
Incorrect ident parsing in transformations

#71 · created Jan 08, 2018 by Raphaël Rieu-Helft component: transformations priority: high
- CLOSED
- 3
updated Feb 02, 2018
induction_pr with arguments

#22 · created Oct 31, 2017 by DAILLER Sylvain component: transformations priority: low
- CLOSED
- 1
- 3
updated Mar 27, 2019
induction_ty_arg_lex expected behavior

#280 · created Mar 01, 2019 by DAILLER Sylvain component: transformations
- CLOSED
- 1
- 0
updated Mar 26, 2019
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
Interaction of smt encoding with meta

#196 · created Oct 03, 2018 by DAILLER Sylvain component: transformations feature wish priority: low
- 3
updated Mar 12, 2021
List transformation with arguments and documentation

#380 · created Sep 03, 2019 by DAILLER Sylvain component: transformations
- CLOSED
- 17
updated Nov 22, 2019
--list-transform should print all transformations

#210 · created Oct 12, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 0
updated Nov 13, 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
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
Problem with infix and val predicate in transformations

#114 · created May 04, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 2
updated Jul 18, 2018
Record transformation time

#574 · created Apr 29, 2021 by Quentin Garchery To be discussed component: session component: transformations feature wish
- 11
updated May 05, 2021
recursive destruct

#20 · created Oct 31, 2017 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated Apr 29, 2019
Removing Inline_trivial

#263 · created Jan 31, 2019 by DAILLER Sylvain component: drivers component: transformations
- CLOSED
- 1
- 0
updated Feb 12, 2019
Restricting behavior of rewrite_list

#226 · created Oct 29, 2018 by DAILLER Sylvain component: transformations priority: low
- CLOSED
- 2
updated Nov 07, 2018
Simplification of array initializer for generated Why3 code

#99 · created Mar 14, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated Jun 18, 2019
simplify_trivial_quantification kills some goals

#120 · created May 22, 2018 by Raphaël Rieu-Helft component: transformations priority: high
- CLOSED
- 4
updated May 22, 2018
split_all_full raises out of memory on float theory

#285 · created Mar 24, 2019 by DAILLER Sylvain component: transformations
- 0
updated Mar 22, 2022

Prev
1
2
3
Next