3 ms·

Good question, gugagore! We have treated Z3 and CVC4 exactly equal, i.e. every formula on which Z3 was tested, CVC4 got also tested. It is thus striking that w

Good question, gugagore! We have treated Z3 and CVC4 exactly equal, i.e. every formula on which Z3 was tested, CVC4 got also tested. It is thus striking that we found almost twice as many bugs in Z3 as compared to CVC4. The solvers have different development models. Whereas Z3 relies on a single main developer and a couple of assisting developers, CVC4 is more of a community effort. CVC4 requires code reviews, Z3 usually not. On the other hand, issues in Z3 get usually fixed faster and Z3 has the larger codebase (Z3: ~400k LoC vs CVC4: ~200k LoC). The fuzzing practices of CVC4 did not play a role, though. As soon as they were in place (since August 2020), we applied their rules to both solvers. Our earlier work "Validating SMT Solvers via Semantic Fusion" published at PLDI 2020 (bug hunting from July 2019 - November 2019) showed the same trend. To the best of our knowledge, all SMT solver bug hunting campaigns prior to ours, found no bugs in CVC4 at all. CVC4 simply seems to be harder to crack.

zsu 6y ago
To add a quick follow-up to dwinterer's nice reply, note please Z3's current support for nonlinear arithmetic and string logics is more advanced than CVC4's, where many of the detected bugs in Z3 occurred.
- zsu 6y ago
  Figure 8 in the OOPSLA paper (https://arxiv.org/pdf/2004.08799.pdf https://arxiv.org/pdf/2004.08799.pdf) provides a breakdown of the bugs found in different logics for Z3 and CVC4.
ahelwer 6y ago
I really wish Microsoft would hire some developers to help Nikolaj. I've done some simple volunteer dev work for Z3 (just creating a nuget package & improving their build/release pipeline mostly) but my impression is there is a ton of work that could be done if one were to really sink their teeth into the codebase. Really tricky, interesting, applied-theory type work too. I'm biased but if I had any purse string authority at Microsoft, RiSE's budget would be a multiple of what it currently is.

zsu 6y ago

To add a quick follow-up to dwinterer's nice reply, note please Z3's current support for nonlinear arithmetic and string logics is more advanced than CVC4's, where many of the detected bugs in Z3 occurred.

zsu 6y ago
Figure 8 in the OOPSLA paper (https://arxiv.org/pdf/2004.08799.pdf https://arxiv.org/pdf/2004.08799.pdf) provides a breakdown of the bugs found in different logics for Z3 and CVC4.

ahelwer 6y ago

I really wish Microsoft would hire some developers to help Nikolaj. I've done some simple volunteer dev work for Z3 (just creating a nuget package & improving their build/release pipeline mostly) but my impression is there is a ton of work that could be done if one were to really sink their teeth into the codebase. Really tricky, interesting, applied-theory type work too. I'm biased but if I had any purse string authority at Microsoft, RiSE's budget would be a multiple of what it currently is.