search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
819 stars 258 forks source link

Run CBMC regression tests with Bitwuzla #8388

Open tautschnig opened 2 months ago

tautschnig commented 2 months ago

As discussed in #8365, Bitwuzla may be superior to Z3 in some cases. #8384, however, showed that we don't always use it correctly. We should establish how Bitwuzla compares to Z3 (and CVC5) across all regression tests via a CI job.

rod-chapman commented 1 month ago

I like this idea. This will provide hard data to drive improvement of Bitwuzla and CVC5.