Shortcuts names for provers can't be used anymore from command line?
When calling why3 prove in command line, one has to specify the "name" and "version" of the prover (s)he wants to use with the "-P" option.
It seems that we cannot use the "shortcut" of the prover anymore. Is it a feature?
For example, with cvc4, I used to write:
why3 prove -P cvc4 foo.mlw
("cvc4" is the shortcut)
But now it answers:
No prover in corresponds to "cvc4"
(it seems that the config file name/path is missing between words "in" and "corresponds")
So I got back to the manual (http://why3.lri.fr/doc/starting.html which does not seem up-to-date). It says:
the first word of each line [of the output of
why3 --list-provers
] is a unique identifier
My output is:
Known provers:
Alt-Ergo 2.0.0
CVC4 1.7
CVC4 1.7 (counterexamples)
Z3 4.8.5
Z3 4.8.5 (counterexamples)
Z3 4.8.5 (noBV)
So I tried
why3 prove -P CVC4 foo.mlw
But now, why3 answers:
More than one prover in correspond to "CVC4": CVC4 1.7, CVC4 1.7 (counterexamples)
So I figured that I had to explicit the version number of cvc4 with a comma to explicit the fact that I don't want the counterexamples alternative.
why3 prove -P CVC4,1.7 foo.mlw
I think that it would be interesting if we were able to use the "shortcut" of the prover, and/or use its name (Why3 in that case could choose the most recent version of the prover which is not an "alternative" version)