In my limited experience trying both on a couple CTF problems this last year (although having used Z3 a plenty for years before that), they're not even in the same ballpark. CVC5 is ridiculously good.

I do recall that for real number theory, CVC4 and Z3 have very different models though. I don't recall which one uses which model though, and I'm not sure if CVC5 uses the same model. I don't use either of them for real number arithmetic anyway.

The paper had a comparison table gainst the prev. version CVC4 and Z3. cvc5 found more solutions than the other 2. Their python API is the same, it's a drop-in replacement against Z3, its C++ Api is better, its solver is better.

I just miss the comparison against lingeling and others. will have to wait for next competition. most cvc4 users, like Isabelle and Ada Spark will upgrade soon.

Cvc5 will likely be better if you use strings a lot, or other exotic theories.