On Wed, 25 Mar 2020, Claude Marche wrote:
>
>
> Le 24/03/2020 à 21:47, Guillaume Melquiond a écrit :
> > Le 24/03/2020 à 21:42, Julia Lawall a écrit :
> >
> >>> * fixed conflicting symbols for CVC4 1.7
> >>
> >> I'm not sure what this change is, but after doing a pull of the latest
> >> version, I still have to remove the --strings-exp option to get cvc4 to
> >> work.
> >
> > Yes, this is a different issue. The one that was fixed is that CVC4 1.7
> > has a lot of new predefined symbols, so Why3 has to rename user
> > identifiers so that they do not confuse CVC4.
> >
> > The issue with --strings-exp still needs to be investigated.
>
> The problem was not that CVC4 1.7 has "a lot of new predefined symbols",
> it was that we switched from
>
> (set-logic "AUFDTNIRA")
>
> to
>
> (set-logic "ALL_SUPPORTED")
>
> which by side effect seems to "activate" a lot more predefined symbols
> in CVC4.
>
> So far I assumed that the problem with -strings-exp was the same. If it
> isn't then I need a reproducer. Please consider creating a ticket.
OK, I'll try to make something small. For me, everything I do with cvc4
crashes almost immediately.
julia
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
