mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-10-12 22:25:48 +00:00
Code Activity

Add fuzz bug filing policy to README

Browse source 
Added a policy for filing fuzz bugs to clarify expectations for bug reports.
This commit is contained in:
Nikolaj Bjorner 2026-08-22 15:13:23 -07:00 • committed by GitHub
parent 8fd4b73ab5
commit a66f69dd86
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
README.md
View file

@ -294,3 +294,12 @@ to Z3's C API. For more information, see [MachineArithmetic/README.md](https://g
## Power Tools
* The [Axiom Profiler](https://github.com/viperproject/axiom-profiler-2) currently developed by ETH Zurich
# Policy for filing fuzz bugs
Z3 is a popular target for fuzzers. Many (best) papers have been published on finding bugs in z3 and SMT solvers and
without doubt the bug file/fix ratio plays an important role establishing evidence in the publications for the value of fuzz tools.
Unfortunately, addressing fuzz bugs doesn't necessarily advance uses of z3 where it matters most to users,
and efforts to address them takes time away from such activities.
With rapidly increasing quality of coding agents for diagnostics and fixes
it is now a reasonable ask that fuzz bug reports make a solid effort on diagnostics and fix.
To help focus efforts on what matters, fuzz bugs without further analysis than a repro may be closed without further consideration.