General Guidelines

We are very committed to making sure that the core use model of CVC4 (i.e. 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:

1. Each fuzzer team may submit up to 3 bugs per week on the CVC4 issue tracker.
2. Please follow the guidelines below regarding the CVC4 configurations and options that can be used for fuzzing.
3. Suggestions for prioritizing bug reports:
   1. refutational soundness bugs (unsat instead of sat);
   2. solution soundness bugs (sat instead of unsat);
   3. model bugs (i.e. bad models);
   4. all other bugs.
4. Please make sure that submitted SMT-LIB files are as small as possible. We recommend using a delta-debugger (such as ddSMT) if possible.
5. Please do your best to not submit duplicates and also double-check that bugs fail on the latest nightly build of CVC4 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.

Configurations

In general, all CVC4 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 CVC4 with ASan/UBSan support (--asan/--ubsan) is a good way to find bugs related to memory management/undefined behavior.

Note: When using ASan, the build currently must be configured with --no-proofs because there are known memory leaks when enabling proofs (tracked here).

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.

Options

While CVC4 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 --ext-rew-prep (two common options and a regular option) but would consider --check-models --ackermann --ext-rew-prep (one common option and two regular options) out of scope. Please note that not all of those combinations make sense but we would expect CVC4 to produce a meaningful error message in such cases.

Common Options

• --check-models
• --default-dag-thresh=N
• --dump-models
• --dump-unsat-cores
• --dump-unsat-cores-full
• --force-logic=LOGIC
• --help
• --incremental
• --lang=LANG
• --output-lang=LANG
• --parse-only
• --preprocess-only
• --print-success
• --produce-models
• --quiet
• --seed=N
• --show-config
• --stats
• --strict-parsing
• --tlimit-per=MS
• --tlimit=MS
• --statistics
• --verbose
• --version
• --copyright
• --interactive

Regular Options

• --ackermann
• --arrays-eager-index
• --bitblast=MODE
• --bitwise-eq
• --block-models=MODE
• --bool-to-bv=MODE
• --bv-alg-extf
• --bv-eq-slicer=MODE
• --bv-eq-solver
• --bv-inequality-solver
• --bv-print-consts-in-binary
• --bv-sat-solver=MODE
• --bv-to-bool
• --cegqi
• --cegqi-bv
• --cegqi-bv-ineq=MODE
• --cegqi-innermost
• --cegqi-midpoint
• --cegqi-nested-qe
• --cegis-sample=MODE
• --sygus-si-abort
• --sygus-si-rcons=MODE
• --sygus-si=MODE
• --check-synth-sol
• --check-unsat-cores
• --decision=MODE
• --dump-instantiations
• --dump-synth
• --e-matching
• --ext-rew-prep
• --ext-rewrite-quant
• --finite-model-find
• --fmf-bound
• --fmf-bound-int
• --fmf-fun
• --fmf-fun-rlv
• --fmf-inst-engine
• --fmf-type-completion-thresh=N
• --fs-interleave
• --full-saturate-quant
• --full-saturate-quant-limit=N
• --ho-elim
• --ho-elim-store-ax
• --inst-format=MODE
• --inst-no-entail
• --inst-when=MODE
• --macros-quant
• --macros-quant-mode=MODE
• --mbqi-one-inst-per-round
• --miniscope-quant
• --miniscope-quant-fv
• --model-cores=MODE
• --model-witness-choice
• --multi-trigger-cache
• --multi-trigger-linear
• --multi-trigger-priority
• --multi-trigger-when-single
• --new-prop
• --nl-ext-tf-tplanes
• --nl-ext-tplanes
• --nl-ext-tplanes-interleave
• --pre-skolem-quant
• --prenex-quant=MODE
• --produce-assertions
• --produce-assignments
• --produce-unsat-assumptions
• --produce-unsat-cores
• --qcf-all-conflict
• --quant-alpha-equiv
• --quant-cf
• --quant-cf-mode=MODE
• --re-elim
• --re-elim-agg
• --re-inter-mode=MODE
• --relevant-triggers
• --rewrite-divk
• --sets-ext
• --simplification=MODE
• --smtlib-strict
• --solve-bv-as-int=N
• --solve-int-as-bv=N
• --solve-real-as-int
• --sort-inference
• --static-learning
• --statistics-every-query
• --stats-every-query
• --stats-hide-zeros
• --strict-triggers
• --strings-exp
• --strings-fmf
• --strings-lazy-pp
• --strings-process-loop-mode=MODE
• --sygus-abort-size=N
• --sygus-active-gen=MODE
• --sygus-add-const-grammar
• --sygus-fair=MODE
• --sygus-grammar-cons=MODE
• --sygus-inv-templ=MODE
• --sygus-out=MODE
• --sygus-pbe
• --sygus-unif-pi=MODE
• --tear-down-incremental=N
• --term-db-mode=MODE
• --trigger-sel=MODE
• --uf-ho
• --uf-ss-abort-card=N
• --uf-ss-fair
• --uf-ss-totality
• --uf-ss=MODE
• --unconstrained-simp
• --user-pat=MODE