Issues · Why3 / why3 · GitLab

--list-transform should print all transformations

#210 · created Oct 12, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 0
updated Nov 13, 2018
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
transformation ``apply`` should consider ``let`` as a premise

#185 · created Sep 20, 2018 by MARCHE Claude component: transformations feature wish
- CLOSED
- 4
updated Oct 29, 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
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
Problem with infix and val predicate in transformations

#114 · created May 04, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 2
updated Jul 18, 2018
Array access in transformations with arguments

#116 · created May 07, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated Jul 18, 2018
Transformation `split_vc` and term shapes

#128 · created Jun 01, 2018 by Guillaume Melquiond 1.0.0 component: session component: transformations priority: blocker
- CLOSED
- 1
- 0
updated Jun 13, 2018
Transformation `apply` and inductive predicates

#126 · created Jun 01, 2018 by Guillaume Melquiond component: transformations
- CLOSED
- 2
updated Jun 01, 2018
subst_all and split_intros_goal_wp do not substitute enough

#115 · created May 07, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated May 23, 2018
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
subst should remove declarations

#16 · created Oct 31, 2017 by DAILLER Sylvain component: transformations priority: medium
- CLOSED
- 4
updated May 16, 2018
eliminate_literal, range types and Eprover driver

#101 · created Mar 27, 2018 by Raphaël Rieu-Helft component: drivers component: transformations
- CLOSED
- 0
updated Mar 28, 2018
first_order_matching may instantiate matching variables using bound variables

#79 · created Jan 22, 2018 by CLOCHARD Martin component: transformations soundness
- CLOSED
- 4
updated Feb 02, 2018
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
Compute inside an hypothesis

#13 · created Oct 31, 2017 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated Jan 05, 2018
Add simpl

#14 · created Oct 31, 2017 by DAILLER Sylvain component: transformations
- CLOSED
- 2
updated Jan 05, 2018
Add a revert transformation

#23 · created Oct 31, 2017 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated Dec 20, 2017

Prev
1
2
3
Next