Verus not respecting --no-solver-version-check flag

[Catoverflow]

What Happened

I have z3 of 4.13.0 installed locally and verus expected 4.12.5, according to the note:

vargo build
error: Verus expects z3 version "4.12.5", found version "4.13.0"
Run ./tools/get-z3.(sh|ps1) to update z3 first.
If you need a build with a custom z3 version, re-run with --no-solver-version-check.

I added the --no-solver-version-check because I think it's compatible with 4.12.5 API according to z3's release note, but Verus still panicked with

thread '<unnamed>' panicked at /tmp/verus/source/air/src/smt_verify.rs:192:21:
The verifier expects z3 version "4.12.5", found version "4.13.0 - build hashcode 3049f578a8f98a0b0992eca193afe57a73b30ca3"
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

I checked the code and thought this flag was not respected:

verus/source/air/src/smt_verify.rs

Lines 182 to 196 in aa8b423

	if line.starts_with(GET_VERSION_RESPONSE_PREFIX) {
	if let Some(expected_version) = &context.expected_solver_version {
	let value: &str = &line[GET_VERSION_RESPONSE_PREFIX.len()..line.len() - 1];
	let version = value.trim_matches(&[' ', '"'][..]);
	if version != expected_version.as_str() {
	diagnostics.report(
	&context
	.message_interface
	.unexpected_z3_version(&expected_version, version),
	);
	panic!(
	"The verifier expects z3 version \"{}\", found version \"{}\"",
	expected_version, version
	);
	}

What Was Expected

Verus respect --no-solver-version-check and proceed with no panic / error

[Catoverflow]

This bug still exists after this commit:

Building succeeded with

verus/source ((release/rolling/0.2024.10.22.2776465))> vargo build --no-solver-version-check --release
vargo info [0]: building rust_verify
    Finished release [optimized] target(s) in 0.04s
vargo info [0]: building builtin
    Finished release [optimized] target(s) in 0.02s
vargo info [0]: building builtin_macros
    Finished release [optimized] target(s) in 0.03s
vargo info [0]: building state_machines_macros
    Finished release [optimized] target(s) in 0.02s
vargo info [0]: building vstd_build
    Finished release [optimized] target(s) in 0.02s
vargo info [0]: building verus
    Finished release [optimized] target(s) in 0.03s
vargo info [0]: vstd fresh

But runtime panicked:

verus/source ((release/rolling/0.2024.10.22.2776465))> ./target-verus/release/verus rust_verify/example/guide/getting_started.rs

thread '<unnamed>' panicked at verus/source/air/src/smt_verify.rs:192:21:
The verifier expects z3 version "4.12.5", found version "4.13.0 - build hashcode 3049f578a8f98a0b0992eca193afe57a73b30ca3"
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
error: expected z3 version 4.12.5, found 4.13.0 - build hashcode 3049f578a8f98a0b0992eca193afe57a73b30ca3

thread '<unnamed>' panicked at rust_verify/src/verifier.rs:352:17:
dropped, expected call to `into_inner` instead
stack backtrace:
   0:     0x74620163e6f6 - std::backtrace_rs::backtrace::libunwind::trace::hbee8a7973eeb6c93
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/../../backtrace/src/backtrace/libunwind.rs:104:5
   1:     0x74620163e6f6 - std::backtrace_rs::backtrace::trace_unsynchronized::hc8ac75eea3aa6899
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x74620163e6f6 - std::sys_common::backtrace::_print_fmt::hc7f3e3b5298b1083
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/sys_common/backtrace.rs:68:5
   3:     0x74620163e6f6 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::hbb235daedd7c6190
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x746201690f40 - core::fmt::rt::Argument::fmt::h76c38a80d925a410
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/core/src/fmt/rt.rs:142:9
   5:     0x746201690f40 - core::fmt::write::h3ed6aeaa977c8e45
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/core/src/fmt/mod.rs:1120:17
   6:     0x74620163253f - std::io::Write::write_fmt::h78b18af5775fedb5
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/io/mod.rs:1810:15
   7:     0x74620163e4d4 - std::sys_common::backtrace::_print::h5d645a07e0fcfdbb
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x74620163e4d4 - std::sys_common::backtrace::print::h85035a511aafe7a8
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x746201641267 - std::panicking::default_hook::{{closure}}::hcce8cea212785a25
  10:     0x746201640fc9 - std::panicking::default_hook::hf5fcb0f213fe709a
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/panicking.rs:292:9
  11:     0x746201641828 - std::panicking::rust_panic_with_hook::h095fccf1dc9379ee
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/panicking.rs:779:13
  12:     0x5e0d80baf54d - std::panicking::begin_panic::{{closure}}::h7d943025b9aab28a
  13:     0x5e0d80bab4c6 - std::sys_common::backtrace::__rust_end_short_backtrace::hbe36db03c1754811
  14:     0x5e0d80aca66a - std::panicking::begin_panic::h7ede8bd9c91d2094
  15:     0x5e0d80bb1ee6 - core::ptr::drop_in_place<core::option::Option<rust_verify::verifier::util::PanicOnDropVec<(alloc::sync::Arc<vir::messages::MessageX>,air::messages::MessageLevel)>>>::hbd7d395a3f6460ac
  16:     0x5e0d80bd3c14 - rust_verify::verifier::Verifier::verify_bucket::hf3ebbe0a20e79754
  17:     0x5e0d80bac3e8 - std::sys_common::backtrace::__rust_begin_short_backtrace::h5bb45eaeb7d063f8
  18:     0x5e0d80b8a77b - core::ops::function::FnOnce::call_once{{vtable.shim}}::h599537c8f06ad65a
  19:     0x74620164b8e5 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h12de4fc57affb195
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/alloc/src/boxed.rs:2015:9
  20:     0x74620164b8e5 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h3c619f45059d5cf1
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/alloc/src/boxed.rs:2015:9
  21:     0x74620164b8e5 - std::sys::unix::thread::Thread::new::thread_start::hbac657605e4b7389
                               at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/library/std/src/sys/unix/thread.rs:108:17
  22:     0x7461fb6a339d - <unknown>
  23:     0x7461fb72849c - <unknown>
  24:                0x0 - <unknown>
thread '<unnamed>' panicked at library/core/src/panicking.rs:163:5:
panic in a destructor during cleanup
thread caused non-unwinding panic. aborting.
fish: Job 1, './target-verus/release/verus ru…' terminated by signal SIGABRT (Abort)

[tjhance]

You need to add --no-solver-version-check to the ./target-verus/release/verus rust_verify/example/guide/getting_started.rs line.

[tjhance]

Whoops, you actually need to add -V no-solver-version-check.

[Catoverflow]

Thanks for the timely reply @tjhance

The problem after the fixing commit is:

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

May I open a PR to update the version and fix the problem with build hash?

[tjhance]

I'm a little confused about the problem - I understand the comparison doesn't work properly, but I think the comparison should be skipped entirely if you supply -V no-solver-version-check. Is that not the case?

We like to keep up-to-date with z3, so I doubt you'll receive much pushback for updating the version -- but it's also a process that requires a bit of testing. I also want to make sure I understand the problem you're running into.

[tjhance]

By the way, if you follow the instructions here, you shouldn't need to rely on your system Z3.

[Catoverflow]

I think the comparison should be skipped entirely if you supply -V no-solver-version-check

Yes.

if you follow the instructions here, you shouldn't need to rely on your system Z3.

Yes, I moved this part of discussion in PR and I think this makes sense, though it could be more convenient to add the support

[utaal]

Do we need a no-sover-version-check for vargo too? (So one can build verus with a non-standard Z3?)

Nevermind, I believe this is already supported in vargo (and should now be functional, thanks to Travis' fix).

I'll close this as fixed, please reopen if not, and we can discuss the port to 4.13.0 in #1316