SMTFuzz is a fuzzing framework for testing SMT solvers and first-order theorem provers.
Here we list the bugs bound by SMTFuzz.
Contact: rainoftime.github.io
(NOTE: Many new bugs have not been added here.)
Summary
CVC4:326 (total)
Z3: 805 (total)
Dreal: 25 (total)
Boolector: 40 (total)
Yices2: 121 (total)
OpenSMT: 69 (total)
SMTInterpol: 64 (total)
SMT-RAT: 51 (total)
ArgoSMT: 6 (total)
Eldarica: 18 (total)
Ostrich: 18 (total)
Vampire: 7 (total)
STP: 2 (total)
Alt-Ergo: 1 (total)
Bitwuzla: 1 soundness (total)
VeriT: 2 soundness (total)
MathSAT (4 soundness, 2 crash)
OptiMathSAT (1 crash)
SPASS (1 crash)
Bitwualz, VeriT, MathSAT, OptiMathSAT, and SPASS have no public bug tracking systems