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. Best regards, Guillaume _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
