cvc4(1) on Linux
The text e01c2bd3938e, as Debian 10 (Buster) shipped it.
an automated theorem prover
Flags it lists
-
--abstract-values -
--ag-miniscope-quant -
--aggressive-core-min -
--allow-empty-dependencies -
--approx-branch-depth -
--arith-no-partial-fun -
--arith-prop -
--arith-prop-clauses -
--arith-rewrite-equalities -
--arrays-config -
--arrays-eager-index -
--arrays-eager-lemmas -
--arrays-lazy-rintro1 -
--arrays-model-based -
--arrays-optimize-linear -
--arrays-prop -
--arrays-reduce-sharing -
--arrays-weak-equiv -
--assign-function-values -
--bitblast -
--bitblast-aig -
--bitblast-step -
--bool-to-bv -
--bv-abstraction -
--bv-aig-simp -
--bv-alg-extf -
--bv-algebraic-budget -
--bv-algebraic-solver -
--bv-div-zero-const -
--bv-eager-explanations -
--bv-eq-slicer -
--bv-eq-solver -
--bv-extract-arith -
--bv-gauss-elim -
--bv-inequality-solver -
--bv-intro-pow2 -
--bv-lazy-reduce-extf -
--bv-lazy-rewrite-extf -
--bv-num-func -
--bv-propagate -
--bv-quick-xplain -
--bv-sat-conflict-step -
--bv-sat-solver -
--bv-skolemize -
--bv-to-bool -
--cbqi -
--cbqi-all -
--cbqi-bv -
--cbqi-bv-concat-inv -
--cbqi-bv-ineq -
--cbqi-bv-interleave-value -
--cbqi-bv-linear -
--cbqi-bv-rm-extract -
--cbqi-bv-solve-nl -
--cbqi-full -
--cbqi-innermost -
--cbqi-lit-dep -
--cbqi-midpoint -
--cbqi-min-bounds -
--cbqi-model -
--cbqi-multi-inst -
--cbqi-nested-qe -
--cbqi-nopt -
--cbqi-prereg-inst -
--cbqi-recurse -
--cbqi-repeat-lit -
--cbqi-round-up-lia -
--cbqi-sat -
--cbqi-use-inf-int -
--cbqi-use-inf-real -
--cdt-bisimilar -
--cegis-sample -
--cegqi -
--cegqi-si -
--cegqi-si-abort -
--cegqi-si-partial -
--cegqi-si-reconstruct -
--cegqi-si-reconstruct-const -
--cegqi-si-sol-min-core -
--cegqi-si-sol-min-inst -
--check-models -
--check-proofs -
--check-synth-sol -
--check-unsat-cores -
--cnf-step -
--collect-pivot-stats -
--cond-rewrite-quant -
--cond-var-split-agg-quant -
--cond-var-split-quant -
--condense-function-values -
--conjecture-filter-active-terms -
--conjecture-filter-canonical -
--conjecture-filter-model -
--conjecture-gen -
--conjecture-gen-gt-enum -
--conjecture-gen-max-depth -
--conjecture-gen-per-round -
--conjecture-gen-uee-intro -
--conjecture-no-filter -
--continued-execution -
--copyright -
--cpu-time -
--cut-all-bounded -
--decision -
--decision-random-weight -
--decision-step -
--decision-threshold -
--decision-use-weight -
--decision-weight-internal -
--default-dag-thresh -
--default-expr-depth -
--dio-decomps -
--dio-repeat -
--dio-solver -
--dio-turns -
--dt-binary-split -
--dt-blast-splits -
--dt-cyclic -
--dt-force-assignment -
--dt-infer-as-lemmas -
--dt-ref-sk-intro -
--dt-rewrite-error-sel -
--dt-share-sel -
--dt-stc-ind -
--dt-use-testers -
--dt-var-exp-quant -
--dump -
--dump-instantiations -
--dump-models -
--dump-proofs -
--dump-synth -
--dump-to -
--dump-unsat-cores -
--dump-unsat-cores-full -
--e-matching -
--eager-type-checking -
--early-exit -
--elim-ext-arith-quant -
--elim-taut-quant -
--error-selection-rule -
--ext-rew-prep -
--ext-rew-prep-agg -
--fallback-sequential -
--fc-penalties -
--fewer-preprocessing-holes -
--filter-lemma-length -
--finite-model-find -
--fmf-bound -
--fmf-bound-int -
--fmf-bound-lazy -
--fmf-bound-min-mode -
--fmf-empty-sorts -
--fmf-fmc-simple -
--fmf-fresh-dc -
--fmf-fun -
--fmf-fun-rlv -
--fmf-inst-engine -
--fmf-inst-gen -
--fmf-inst-gen-one-quant-per-round -
--force-logic -
--force-no-limit-cpu-while-dump -
--fs-interleave -
--full-saturate-quant -
--full-saturate-quant-rd -
--global-negate -
--hard-limit -
--help -
--heuristic-pivots -
--ho-matching -
--ho-matching-var-priority -
--ho-merge-term-db -
--idl-rewrite-equalities -
--increment-triggers -
--incremental -
--incremental-parallel -
--infer-arith-trigger-eq -
--infer-arith-trigger-eq-exp -
--inst-format -
--inst-level-input-only -
--inst-max-level -
--inst-no-entail -
--inst-no-model-true -
--inst-prop -
--inst-when -
--inst-when-phase -
--inst-when-strict-interleave -
--inst-when-tc-first -
--int-wf-ind -
--interactive -
--ite-dtt-split-quant -
--ite-lift-quant -
--ite-simp -
--lemma-step -
--lemmas-on-replay-failure -
--lfsc-letification -
--literal-matching -
--local-t-ext -
--lte-partial-inst -
--lte-restrict-inst-closure -
--macros-quant -
--macros-quant-mode -
--maxCutsInContext -
--mbqi -
--mbqi-interleave -
--mbqi-one-inst-per-round -
--mbqi-one-quant-per-round -
--minisat-dump-dimacs -
--minisat-elimination -
--miniscope-quant -
--miniscope-quant-fv -
--miplib-trick -
--miplib-trick-subs -
--mmap -
--model-format -
--model-u-dt-enum -
--multi-trigger-cache -
--multi-trigger-linear -
--multi-trigger-priority -
--multi-trigger-when-single -
--new-prop -
--nl-ext -
--nl-ext-ent-conf -
--nl-ext-factor -
--nl-ext-inc-prec -
--nl-ext-purify -
--nl-ext-rbound -
--nl-ext-rewrite -
--nl-ext-split-zero -
--nl-ext-tf-taylor-deg -
--nl-ext-tf-tplanes -
--nl-ext-tplanes -
--nl-ext-tplanes-interleave -
--no-simplification -
--omit-dont-cares -
--on-repeat-ite-simp -
--output-lang -
--parse-only -
--parse-step -
--partial-triggers -
--pb-rewrites -
--pivot-threshold -
--pp-assert-max-sub-size -
--pre-skolem-quant -
--pre-skolem-quant-agg -
--pre-skolem-quant-nested -
--prenex-quant -
--prenex-quant-user -
--preprocess-only -
--preprocess-step -
--print-expr-types -
--print-success -
--produce-assertions -
--produce-assignments -
--produce-models -
--produce-unsat-assumptions -
--produce-unsat-cores -
--proof -
--prop-row-length -
--pure-th-triggers -
--purify-dt-triggers -
--purify-triggers -
--qcf-all-conflict -
--qcf-eager-check-rd -
--qcf-eager-test -
--qcf-nested-conflict -
--qcf-skip-rd -
--qcf-tconstraint -
--qcf-vo-exp -
--quant-alpha-equiv -
--quant-anti-skolem -
--quant-cf -
--quant-cf-mode -
--quant-cf-when -
--quant-dsplit-mode -
--quant-epr -
--quant-epr-match -
--quant-fun-wd -
--quant-ind -
--quant-model-ee -
--quant-rep-mode -
--quant-split -
--quantifier-step -
--quiet -
--random-freq -
--random-seed -
--refine-conflicts -
--register-quant-body-terms -
--relational-triggers -
--relevant-triggers -
--repeat-simp -
--replay-early-close-depth -
--replay-failure-penalty -
--replay-lemma-reject-cut -
--replay-num-err-penalty -
--replay-reject-cut -
--replay-soi-major-threshold -
--replay-soi-major-threshold-pen -
--replay-soi-minor-threshold -
--replay-soi-minor-threshold-pen -
--restart-int-base -
--restart-int-inc -
--restart-step -
--restrict-pivots -
--revert-arith-models-on-unsat -
--rewrite-apply-to-const -
--rewrite-divk -
--rewrite-rules -
--rewrite-step -
--rlimit -
--rlimit-per -
--rr-one-inst-per-round -
--rr-turns -
--sat-conflict-step -
--se-solve-int -
--seed -
--segv-spin -
--sep-check-neg -
--sep-child-refine -
--sep-deq-c -
--sep-exp -
--sep-min-refine -
--sep-pre-skolem-emp -
--sets-ext -
--sets-infer-as-lemmas -
--sets-proxy-lemmas -
--sets-rel-eager -
--show-config -
--show-debug-tags -
--show-trace-tags -
--simp-ite-compress -
--simp-ite-hunt-zombies -
--simp-with-care -
--simplex-check-period -
--simplification -
--smtlib-strict -
--snorm-infer-eq -
--soi-qe -
--sort-inference -
--standard-effort-variable-order-pivots -
--static-learning -
--stats -
--stats-every-query -
--stats-hide-zeros -
--strict-parsing -
--strict-triggers -
--strings-abort-loop -
--strings-binary-csp -
--strings-check-entail-len -
--strings-eager -
--strings-eager-len -
--strings-eit -
--strings-exp -
--strings-fmf -
--strings-guess-model -
--strings-infer-as-lemmas -
--strings-infer-sym -
--strings-inm -
--strings-lazy-pp -
--strings-lb -
--strings-len-geqz -
--strings-len-norm -
--strings-lprop-csp -
--strings-min-prefix-explain -
--strings-opt1 -
--strings-opt2 -
--strings-print-ascii -
--strings-process-loop -
--strings-rexplain-lemmas -
--strings-sp-emp -
--strings-uf-reduct -
--sygus-abort-size -
--sygus-add-const-grammar -
--sygus-auto-unfold -
--sygus-bool-ite-return-const -
--sygus-eval-builtin -
--sygus-eval-unfold -
--sygus-eval-unfold-bool -
--sygus-ext-rew -
--sygus-fair -
--sygus-fair-max -
--sygus-grammar-norm -
--sygus-inference -
--sygus-inv-templ -
--sygus-inv-templ-when-sg -
--sygus-min-grammar -
--sygus-opt1 -
--sygus-out -
--sygus-pbe -
--sygus-print-callbacks -
--sygus-qe-preproc -
--sygus-ref-eval -
--sygus-repair-const -
--sygus-rr -
--sygus-rr-synth -
--sygus-rr-synth-accel -
--sygus-rr-synth-check -
--sygus-rr-synth-filter-cong -
--sygus-rr-synth-filter-match -
--sygus-rr-synth-filter-order -
--sygus-rr-verify -
--sygus-rr-verify-abort -
--sygus-sample-grammar -
--sygus-samples -
--sygus-stream -
--sygus-sym-break -
--sygus-sym-break-dynamic -
--sygus-sym-break-lazy -
--sygus-sym-break-pbe -
--sygus-sym-break-rlv -
--sygus-templ-embed-grammar -
--sygus-unif -
--symmetry-breaker -
--symmetry-breaker-exp -
--tear-down-incremental -
--term-db-mode -
--theory-check-step -
--theoryof-mode -
--thread-stack -
--threadN -
--threads -
--tlimit -
--tlimit-per -
--track-inst-lemmas -
--trigger-active-sel -
--trigger-sel -
--type-checking -
--uf-ho -
--uf-ho-ext -
--uf-ss -
--uf-ss-abort-card -
--uf-ss-clique-splits -
--uf-ss-eager-split -
--uf-ss-fair -
--uf-ss-fair-monotone -
--uf-ss-regions -
--uf-ss-totality -
--uf-ss-totality-limited -
--uf-ss-totality-sym-break -
--unate-lemmas -
--unconstrained-simp -
--use-approx -
--use-fcsimplex -
--use-soi -
--use-theory -
--user-pat -
--var-elim-quant -
--var-ineq-elim-quant -
--verbose -
--version -
--wait-to-join -
-V -
-h -
-i -
-m -
-q -
-s -
-v