Re:Cvc5: Versatile and Industrial-Strength SMT Solver [pdf]
by procedurecall on Saturday March 05, 2022 @04:03PM
(#30571844)
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.