On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 21:31, Julia Lawall a écrit :
> >> * default proof strategies "Auto level 1" and "Auto level 2"
> >> have been respectively renamed "Auto level 2" and "Auto level 3";
> >> "Auto level 1" now behaves similarly to "Auto level 0" but with a
> >> longer
> >> time limit; more details in the manual, Section 10.6 "Proof
> >> Strategies" :x:
> >
> > This means that there is no more of the old Auto Level 3?
>
> This is the first release with "Auto level 3". (Why3 1.2 provided levels
> 0, 1, 2 only.) If you were already using "Auto level 3", that is because
> you were using a git version of Why3.
Yes, that is the case.
>
> As far as I know, the strategies have not changed since they were
> renamed, so I have no idea why you are experiencing a change of behavior
> in "Auto level 3".
Where are the strategies defined? I found strategies.conf, but that seems
to have only level 0 and level 1. Previously, the auto strategies were
in the why.conf file, but that doesn't seem to be the case any more.
julia
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
