3 ms·
Good video! It could have been improved by digging into why the code of Z3 and CVC4 had those bugs. It is surprising to me that they could be wrong on such si
by espadrine 6y ago
Good video!
It could have been improved by digging into why the code of Z3 and CVC4 had those bugs.
It is surprising to me that they could be wrong on such simple statements (and such a simple fuzzing procedure). I expected the faulty statements to be gigantic edge-case monstrosities, but they are just a few lines of boolean logic.
- zsu 6y agoAgreed; such an analysis/study would be nice to have. It is worth to point that the small tests were the results of test input reduction --- the original tests were often quite large. Many of the bugs were due to incorrect handling of corner/boundary cases, such as "division by zero" (which has well-defined semantics in SMT-LIB).