update z3 to 4.14.0

[Catoverflow]

Update default z3 version to 4.13.0 and fix the runtime version check. For version check the problem is described in #1313 (comment) :

I'm using Arch Linux and shipped z3 has the version number as Z3 version 4.13.0 - 64 bit - build hashcode 3049f578a8f98a0b0992eca193afe57a73b30ca3, which happened to pass the version checks in vargo wrapper at

verus/tools/vargo/src/main.rs

Line 80 in 2776465

SmtSolverType::Z3 => Regex::new(r"Z3 version (\d+\.\d+\.\d+) - \d+ bit")

and

verus/tools/vargo/src/main.rs

Line 161 in 2776465

let version = captures.next()?;

because the hash part is skipped using the 2nd match group. But it fails at runtime even if the versions compared are the same(see the error above):

verus/source/air/src/smt_verify.rs

Line 186 in 2776465

if version != expected_version.as_str() {

error: expected z3 version 4.13.0, found 4.13.0 - build hashcode 3049f578a8f98a0b0992eca193afe57a73b30ca3

[utaal]

Hi @Catoverflow, thank you for the PR.

Just wanted to mention that we may want to do a veritas run before merging a major Z3 version bump, as that may break a number of proofs.

Regarding #1313 note that, as @tjhance mentioned, you shouldn't need to rely on your package manager's Z3. The installation steps will download the expected Z3 version when you set up verus.

[Catoverflow]

we may want to do a veritas run before merging a major Z3 version bump

I think it should be added to CI. And I have tested the PR using veritas locally and all build / test passes by github actions (workflow for this PR here requires approval to run). All passed except one from utaal/verified-nrkernel of unable to fetch page table and I think that's not related to verus.

you shouldn't need to rely on your package manager's Z3

This makes sense, so this PR is not necessary and you can close it. But it could still be more convenient. For example, Arch Linux has glibc version of 2.40 which was not included in z3's binary release. So using the version of z3 shipped by system will spare me from compiling z3 everytime it updates.

[utaal]

Can ask you a favor: can you post the result of the veritas run with this branch?

[Catoverflow]

@utaal The error related logs running ~/verus/tools/veritas (main)> bash run.sh run_configuration_small.toml are

■■■ info: verus ready ■■■
■■■ info: producing output at /root/output/2024-10-24-22-32-19-127-3704fe9cc0818cffbd8e5efc2c689255b224473d6141ac778f0b1d1d6a897d2f ■■■
■■■ info: running projects ■■■
■■■ info: running project verus-vstd ■■■
■■■ info: fetching https://github.com/verus-lang/verus.git into /root/repos-cache/verus-vstd-5fd9e8df53cb0957a9c182e2857c835acd008efa69e1633fd22e450a15921bc3 ■■■
▶▶▶ running: cd "/root/work/work/verus-vstd-0d6e4079e36703ebd37c00722f5891d28b0e2811dc114b129215123adcce3605/" && "/root/work/work/verus-0d6e4079e36703ebd37c00722f5891d28b0e2811dc114b129215123adcce3605/source/target-verus/release/verus" "source/vstd/vstd.rs" "--no-vstd" "--crate-type=lib" "-V" "use-crate-name" "--output-json" "--time" "--no-report-long-running" ◀◀◀
■■■ info: running project page-table ■■■
■■■ info: fetching https://github.com/utaal/verified-nrkernel.git into /root/repos-cache/page-table-18eaab182025129d1f4175b03abbc9bc8523332d0fa5e96e4e52f28821e24d98 ■■■
error [src/main.rs:272:26]: failed to find page-table: revspec 'page-table' not found; class=Reference (4); code=NotFound (-3)

With unmodified z3 version this error occurred too (this should not be related to the version change anyway)

[utaal]

I moved this to 4.14.0 but that introduces a timeout in div_internals/lemma_div_auto_minus.

• veritas run