Le 20/03/2020 à 10:43, Julia Lawall a écrit :
> I just see a cascade of split_vc, and when I look at the alt-ergo code
> from one to the next, it is identical.
Good catch. I have opened https://gitlab.inria.fr/why3/why3/issues/462
to track the issue.
Best regards,
Guillaume
On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 22:14, Julia Lawall a écrit :
>
> >> 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 str
On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 22:14, Julia Lawall a écrit :
>
> >> 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 str
Le 18/03/2020 à 22:14, Julia Lawall a écrit :
>> 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 h
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 le
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
> * 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
Le 17/03/2020 à 14:44, Julia Lawall a écrit :
> cvc4 1.7 a l'air de me donner systematiquement un seg fault:
Oui, il a tendance à faire segfault dès qu'il est contrarié (cf
https://gitlab.inria.fr/why3/why3/issues/461 ). Je ne sais pas si c'est
évitable côté Why3. Est-ce qu'il a dit quelque chose
J'ai aussi l'impression d'avoir une boucle infinie sur un auto level 3.
Il fait des split_vc infiniement, mais a chaque etape le but est un
predicate, et il n'y a rien a splitter.
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://l
cvc4 1.7 a l'air de me donner systematiquement un seg fault:
CVC4 suffered a segfault.
Offending address is 0x7fff8
expr::ExprManager::AND, 736
expr::ExprManager::APPLY_UF, 4555
expr::ExprManager::BOUND_VARIABLE:Boolean type, 11
expr::ExprManager::BOUND_VARIABLE:integer type, 663
expr::ExprMan
We are happy to announce a new release of Why3, version 1.3.0, available
from the Web page http://why3.lri.fr/
There have been numerous changes since the last release (see below for a
list). Here are some of the most important ones.
- Module cloning now has much stricter requirements; this fixes
11 matches
Mail list logo
