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.
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.