"dove prove" does not accept z3 (nor cvc4) executable path correctly anymore

[villesundell]

Hello again! While dove prove works fine with 1.3.0-44c7e88, the --z3-exe switch seems broken in 1.3.0-9283954.

One used to be able to run dove prove --boogie-exe ~/.dotnet/tools/boogie --z3-exe ~/bin/z3 successfully, but with the current version, the output is as follows:

➜  taohe git:(master) ✗ dove prove --boogie-exe ~/.dotnet/tools/boogie --z3-exe ~/bin/z3

ERROR: z3 executable not found in PATH. Please install it from https://github.com/Z3Prover/z3

The only way I got this to work was setting up PATH correctly, and running dove prove without arguments. (With the arguments above, I would still get errors: cvc4 cannot be found, and --cvc4-exe does not seem to fix the problem.)

[RIg410]

Thank you for your feedback.

[RIg410]

You can also define the paths to the executable files in a separate config in the root of the dove project.

prover-env.toml

boogie = "~/.dotnet/tools/boogie" 
z3 =  "~/bin/z3"
cvc4 = "..../cvc4"

[villesundell]

Thanks for fixing it quickly again: your prover branch solves this issue for me :+1:

However, ~/ does not seem to work in prover-env.toml: absolute path is required.

[RIg410]

Unfortunately, dove prove only works with absolute paths. And also by default, it searches for PATH. I apologize for confusing you with my previous message.

[RIg410]

Added the ability to set paths starting with ~/.