4 ms·
Anyone have opinions on this vs z3? I started with z3 and have never had reason to look elsewhere. Minor performance differences do not concern me as much as do
by 41b696ef1113 5y ago
Anyone have opinions on this vs z3? I started with z3 and have never had reason to look elsewhere. Minor performance differences do not concern me as much as documentation, (Python) bindings, etc quality of life features.
- procedurecall 5y agoIn 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.
- c-cube 5y agoCvc5 will likely be better if you use strings a lot, or other exotic theories.
- rurban 5y agoThe 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.