Z3 Version Parsing Error: EasyCrypt interprets "4.8.12" as "4.12"

[MaryamAmiriTehrani]

When using EasyCrypt/Why3 on Ubuntu/WSL, Z3 version 4.8.12 is sometimes parsed as 4.12, causing EasyCrypt to complain about an "unknown prover Z3@4.12." This happens even though the recognized versions are 4.8.12 and 4.8.14, and Z3 is correctly installed.

Steps to Reproduce:
Install EasyCrypt (commit r2025.02-1-g3300445) on Ubuntu 24.04.2 LTS (WSL2).
Install Z3 versions 4.8.12 and 4.8.14 (via apt or any other method).
Run ./ec.native why3config to detect provers.
Attempt to compile a trivial EasyCrypt file:
bash
Copy
./ec.native compile test.ec
Observe the error: unknown prover Z3@4.12.
Expected Behavior
EasyCrypt should recognize Z3@4.8.12 (or Z3@4.8.14) and compile the file without error.

Actual Behavior
EasyCrypt attempts to invoke Z3@4.12, resulting in the error:
[critical] unknown prover Z3@4.12

Environment:
OS: Ubuntu 24.04.2 LTS on WSL2 (Windows 11)
EasyCrypt commit: r2025.02-1-g3300445
Installed Z3 versions: 4.8.12, 4.8.14
Additional provers: CVC4, CVC5, Yices

Configuration File (~/.config/easycrypt/why3.conf)
`
ini
Copy
[main]
default_editor = "xdg-open %f"
magic = 14
memlimit = 1000
running_provers_max = 2
timelimit = 5.000000

[partial_prover]
name = "CVC4"
path = "/.../cryptol-3.2.0/bin/cvc4.exe"
version = "1.8"

[partial_prover]
name = "CVC5"
path = "/.../cryptol-3.2.0/bin/cvc5.exe"
version = "1.1.1"

[partial_prover]
name = "Yices"
path = "/.../cryptol-3.2.0/bin/yices.exe"
version = "Yices"

[partial_prover]
name = "Yices"
path = "/.../cryptol-3.2.0/bin/yices-smt2.exe"
version = "2.6.2\r"

[partial_prover]
name = "Z3"
path = "/usr/bin/z3"
version = "4.8.12"
`
(Originally also had a Windows-based Z3@4.8.14 entry, which I removed, but the error persisted.)

Additional Context:
I removed ~/.config/easycrypt/why3.conf and re-ran ./ec.native why3config, but EasyCrypt still references Z3@4.12.
Specifying -p Z3@4.8.14 at compile time does not fix the issue.
Confirmed no environment variables are forcing a default of 4.12.
Removing the Windows-based Z3 entry also did not help.

[fdupress]

Hiya @MaryamAmiriTehrani! Can you check if there is an easycrypt.project in the proof repo you are trying to run, and if it refers to 4.12?

This error message would be emitted when the project you are verifying specifies "I need z3 version at least 4.12" and you do not have it installed.