How to call why3, from the command line, to access a prover with alternatives?

Question

My configuration file includes alternative entries for different provers. When I execute why3 prove with that prover, then the output of why3 is a message informing that I have more than one prover in my configuration file with the given name, the list of these provers.

/home/xyz> why3 prove --prover Z3 afile.why
More than one prover in /home/xyz/.why3.conf correspond to "Z3":
Z3 (4.4.1), Z3 (4.4.1 noBV)

I would like to know how to call why3 on a specific alternative of that prover, if this is possible.

Answer 1

Eventually I peeked at the source code of Why3 to get an answer. It is to be found in why3/src/driver/whyconf.mli and why3/src/driver/whyconf.ml.

A solution is to use the version and alternative fields of the prover entry in Why3's configuration file. For instance, if this file contains the following two entries for Z3:

[prover]
alternative = "noBV"
command = "%l/why3-cpulimit %t %m -s z3 -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%l/why3-cpulimit %U %m -s z3 -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
driver = "/home/ddeharbe/.opam/system/share/why3/drivers/z3_432.drv"
editor = ""
in_place = false
interactive = false
name = "Z3"
version = "4.4.1"

[prover]
command = "%l/why3-cpulimit %t %m -s z3 -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%l/why3-cpulimit %U %m -s z3 -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
driver = "/home/ddeharbe/.opam/system/share/why3/drivers/z3_440.drv"
editor = ""
in_place = false
interactive = false
name = "Z3"
shortcut = "z3"
version = "4.4.1"

The "alternative" field differs between entries. So to call the first entry, the command is:

why3 prove afile.why --prover Z3,4.4.1, 

To call the second entry, the command is:

why3 prove afile.why --prover Z3,4.4.1,noBV