Le 14/08/2018 à 18:59, Ziqing Luo a écrit :
I have another question: is it possible to let why3 automatically try different provers ? So far I use the command "why3 prove -P [prover] [filename]", with which why3 only uses one prover and there are always few goals left unproved.
I highly recommend using the graphical user interface (launched by "why3 ide [filename]"), as it lets you choose which provers (possibly several ones) you want to use on which goals, and it remembers your choices the next time you open your file.
If, for some reasons (e.g. interfacing with another tool), you cannot make use of the graphical interface, then you will have to use Why3 as a library rather than as a program, if the command line tools are not expressive enough.
Best regards, Guillaume _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
