I do software verification. In my experience, Z3 is consistently but noticeably better than CVC5 at the kinds of problems we generate, though the two tools are close enough that you definitely want to architect your verification tool to be able to use either one (or both at once, in case you hit a problem which is pathological in one but not the other).
One place where Z3 exposes a superior interface to CVC5 is when you want to do term simplification. CVC5 does not have any real analogue to Z3's simplification tactics (like ctx-solver-simplify), so if you want to take a term and simplify it with respect to a set of assumptions, Z3 is your only choice. I think CVC5 has all the machinery you need to implement that stuff inside of it, but as a user you can't access it.
The place where CVC5 really pulls ahead of Z3 is when you want to produce proofs (eg, to integrate SMT solving into a proof assistant like Lean, HOL, or Rocq). Both tools have support for generating proofs, but CVC5's are noticeably less buggy, to the point that Lean's SMT integration uses CVC5, even though Leo de Moura (Lean's designer) was also the original designer of Z3.
There's nothing "more direct" - the different APIs for different languages call into the same underlying library, and most of them are more accessible and easier to work with than C++.
Z3 is presumably written in C++ for performance, but without data I am very confident the vast majority of programs that use Z3 consume it via one of the other APIs.
It might have more to do with the first release of Z3 being in 2012, with the first stable Rust release being in 2015. Rather than the authors of Z3 passing some kind of judgment on Rust…
Using a database or 3D Printer isn't bad because you don't learn anything about the internals.
step 1: insert the problem
step 2: ???
step 3: profit
If you're familiar with the Z3 Python API, you'll find the CVC5 one familiar.
Caveat: I mostly do logic design, maybe there are some software verification tasks where Z3 comes out ahead. I've never seen one though.
One place where Z3 exposes a superior interface to CVC5 is when you want to do term simplification. CVC5 does not have any real analogue to Z3's simplification tactics (like ctx-solver-simplify), so if you want to take a term and simplify it with respect to a set of assumptions, Z3 is your only choice. I think CVC5 has all the machinery you need to implement that stuff inside of it, but as a user you can't access it.
The place where CVC5 really pulls ahead of Z3 is when you want to produce proofs (eg, to integrate SMT solving into a proof assistant like Lean, HOL, or Rocq). Both tools have support for generating proofs, but CVC5's are noticeably less buggy, to the point that Lean's SMT integration uses CVC5, even though Leo de Moura (Lean's designer) was also the original designer of Z3.
Z3 is presumably written in C++ for performance, but without data I am very confident the vast majority of programs that use Z3 consume it via one of the other APIs.