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.
Happy confinement to all,
- Claude
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
