undefined | Better HN

0 pointszsu5y ago0 comments

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.

0 comments

1 comments · 1 top-level

zsuOP5y ago

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

j / k navigate · click thread line to collapse