Repository navigation
Fuzzing cvc5
We are very committed to making sure that the core usage model of cvc5 (i.e., its usage without experimental/research options enabled) is extremely robust. At the same time, we are a small team and have to set priorities, including prioritizing user bugs over fuzzer bugs.
For fuzzing bugs, we have the following guidelines:
- Each fuzzer team may submit up to 3 bugs per week on the cvc5 issue tracker.
- Please follow the guidelines below regarding the cvc5 configurations and options that can be used for fuzzing.
- Suggestions for prioritizing bug reports:
- refutational soundness bugs (unsat instead of sat);
- solution soundness bugs (sat instead of unsat);
- model bugs (i.e. bad models);
- all other bugs.
- Please make sure that submitted SMT-LIB files are as small as possible. We recommend using a delta-debugger (such as ddSMT) if possible.
- Please do your best to not submit duplicates and also double-check that bugs fail on the latest nightly build of cvc5 before submitting.
This may take some effort on the fuzzing team's part in order to curate, retest, and submit the weekly bugs. Issues take significant effort to investigate and fix, so this is a way that fuzzing efforts can help without overwhelming our developers.
In general, all cvc5 configurations can be used for fuzzing purposes. To achieve good throughput, a production build with assertions (./configure.sh production --assertions) is a good start. This configuration enables compiler optimizations but keeps all debug assertions. Configuring cvc5 with ASan/UBSan support (--asan/--ubsan) is a good way to find bugs related to memory management/undefined behavior.
Note: Before reporting performance bugs, please make sure that the problems persist with a production build. Non-production builds are not optimized for performance, so performance rarely matters except in particularly egregious cases. If you found such a bug, please explain why you think this should be fixed.
While cvc5 is used in production environments, it is also a research project. As such, we have several experimental options, with various limitations (especially when combined together), making them unsuitable for fuzzing at this point in time. Given our small team size, we do not have the capacity to address fuzzed bugs from experimental options in the foreseeable future, though we are working on improving the situation. Thus we will only address bug reports that combine an arbitrary number of common options with at most one regular option. We list the common and the regular options below. For example we would accept --check-models --incremental --finite-model-find (two common options and a regular option) but would consider --check-models --simplification=none --finite-model-find (one common option and two regular options) out of scope. Please note that not all of those combinations make sense but we would expect cvc5 to produce a meaningful error message in such cases.
--check-models--check-proofs--check-unsat-cores--condense-function-values--copyright--dag-thresh--debug-check-models--decision--decision-mode--default-function-value-mode--enum-inst--expr-depth--filename--force-logic--full-saturate-quant--help--help-regular--incremental--input-language--interactive--lang--output--output-lang--output-language--parse-only--preprocess-only--print-inst--print-success--produce-models--produce-proofs--produce-unsat-cores--proof-check--proof-granularity--proof-print-conclusion--proof-print-reference--quiet--random-seed--reproducible-resource-limit--rlimit--rlimit-per--seed--show-config--stats--stats-all--stats-internal--strict-parsing--tlimit--tlimit-per--verbose--verbosity--version
--arith-brab--arith-rewrite-equalities--arith-static-learning--arrays-eager-index--bitblast--bitwise-eq--bool-to-bv--bv-eager-eval--bv-print-consts-as-indexed-symbols--bv-sat-solver--bv-solver--bv-to-bool--cbqi--cbqi-all-conflict--cbqi-mode--cegis-sample--cegqi--cegqi-bv--cegqi-innermost--check-abducts--check-interpolants--check-synth-sol--dump-difficulty--dump-instantiations--dump-models--dump-proofs--dump-unsat-cores--dump-unsat-cores-lemmas--e-matching--eager-arith-bv-conv--ee-mode--elim-taut-quant--enum-inst-interleave--enum-inst-sum--ext-rewrite-quant--finite-model-find--fmf-bound--fmf-type-completion-thresh--fresh-declarations--global-declarations--ho-elim--ho-elim-store-ax--ieval--inst-max-rounds--inst-no-entail--inst-when--interactive-mode--interpolants-mode--ite-lift-quant--learned-rewrite--macros-quant-mode--mbqi--mbqi-enum--mbqi-one-inst-per-round--miniscope-quant--miniscope-quant-user--model-cores--model-u-print--multi-trigger-cache--multi-trigger-linear--multi-trigger-priority--multi-trigger-when-single--nl-ext--nl-ext-factor--nl-ext-rewrite--nl-ext-tf-tplanes--nl-ext-tplanes--nl-ext-tplanes-interleave--opt-res-reconstruction-size--pre-skolem-quant--prenex-quant-user--preregister-mode--print-cores-full--print-inst-full--produce-abducts--produce-assertions--produce-assignments--produce-difficulty--produce-interpolants--produce-learned-literals--produce-unsat-assumptions--proof-rewrite-rcons-rec-limit--proof-rewrite-rcons-step-limit--prop-proof-mode--quant-alpha-equiv--quant-dsplit--relevant-triggers--sat-random-seed--simplification--simplification-mode--solve-bv-as-int--solve-int-as-bv--solve-real-as-int--static-learning--stats-every-query--strings-check-entail-len--strings-deq-ext--strings-eager-eval--strings-eager-len-re--strings-eager-solver--strings-exp--strings-fmf--strings-mbr--strings-process-loop-mode--strings-regexp-inclusion--sygus--sygus-abort-size--sygus-add-const-grammar--sygus-core-connective--sygus-enum--sygus-eval-unfold--sygus-fair--sygus-grammar-cons--sygus-inst--sygus-inv-templ--sygus-min-grammar--sygus-out--sygus-pbe--sygus-repair-const--sygus-rewriter--sygus-si--sygus-si-abort--sygus-si-rcons--sygus-simple-sym-break--sygus-stream--sygus-sym-break-pbe--sygus-unif-pi--sygus-verify-timeout--term-db-mode--trigger-sel--uf-lazy-ll--uf-ss--uf-ss-abort-card--uf-ss-fair--user-pat--var-elim-quant--var-ineq-elim-quant