Hi,
I have Why3 system (version 0.84) and Z3 (version 4.3.2) installed.
My provers-detection-data.conf file contains the following entry:
[ATP z3]
name = "Z3"
exec = "z3"
exec = "z3-4.3.1"
exec = "z3-4.3.0"
exec = "z3-4.2"
exec = "z3-4.1.2"
exec = "z3-4.1.1"
exec = "z3-4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.3.1"
version_old = "4.3.0"
version_old = "4.2"
version_old = "4.1.2"
version_old = "4.1.1"
version_old = "4.0"
driver = "drivers/z3.drv"
command = "%l/why3-cpulimit %t %m -s %e -smt2 -rs:42 %f"
As expected, when I run why3 config --detect-provers, I get the following
warning:
Warning: prover Z3 version 4.3.2 is not known to be supported.
When I use Why3 ide, Z3 (4.3.2) button is added to the GUI. When I try to
use it on any theory, proof call fails, and I get the following error
message:
HighFailure (0.00s)
Prover exit status: exited with status 109
Prover output:
Error: invalid command line option: -rs
For usage information: z3 -h
why3cpulimit time : 0.000000 s
My guess is that command line option -rs was removed from Z3 version 4.3.2.
What should I do to get Z3 working with Why3 - downgrade to 4.3.1 or
install it next to 4.3.2, remove -rs option from "command" line in
provers-detection-data.conf file, or something else?
_______________________________________________
Why3-club mailing list
[email protected]
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
