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")
> (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.
Why3-club mailing list