Reference

cvc4(1)

an automated theorem prover

NAME

cvc4, pcvc4 - an automated theorem prover

SYNOPSIS

cvc4 [ options ] [ file ]

pcvc4 [ options ] [ file ]

DESCRIPTION

cvc4 is an automated theorem prover for first-order formulas with respect to background theories of interest. pcvc4 is CVC4's "portfolio" variant, which is capable of running multiple CVC4 instances in parallel, configured differently.

With file , commands are read from file and executed. CVC4 supports the SMT-LIB (versions 1.2 and 2.0) input format, as well as its own native “presentation language” (see cvc4(5) ), which is similar in many respects to CVC3's presentation language, but not identical.

If file is unspecified, standard input is read (and the CVC4 presentation language is assumed). If file is unspecified and CVC4 is connected to a terminal, interactive mode is assumed.

COMMON OPTIONS

Each option marked with [*] has a --no-OPTIONNAME variant, which reverses the sense of the option.

$

$

Each option marked with [*] has a --no-OPTIONNAME variant, which reverses the sense of the option.

DIAGNOSTICS

CVC4 reports all syntactic and semantic errors on standard error.

HISTORY

The CVC4 effort is the culmination of fifteen years of theorem proving research, starting with the Stanford Validity Checker (SVC) in 1996.

SVC's successor, the Cooperating Validity Checker (CVC), had a more optimized internal design, produced proofs, used the Chaff SAT solver, and featured a number of usability enhancements. Its name comes from the cooperative nature of decision procedures in Nelson-Oppen theory combination, which share amongst each other equalities between shared terms.

CVC Lite, first made available in 2003, was a rewrite of CVC that attempted to make CVC more flexible (hence the “lite”) while extending the feature set: CVCLite supported quantifiers where its predecessors did not. CVC3 was a major overhaul of portions of CVC Lite: it added better decision procedure implementations, added support for using MiniSat in the core, and had generally better performance.

CVC4 is the new version, the fifth generation of this validity checker line that is now celebrating fifteen years of heritage. It represents a complete re-evaluation of the core architecture to be both performant and to serve as a cutting-edge research vehicle for the next several years. Rather than taking CVC3 and redesigning problem parts, we've taken a clean-room approach, starting from scratch. Before using any designs from CVC3, we have thoroughly scrutinized, vetted, and updated them. Many parts of CVC4 bear only a superficial resemblance, if any, to their correspondent in CVC3.

However, CVC4 is fundamentally similar to CVC3 and many other modern SMT solvers: it is a DPLL( T ) solver, with a SAT solver at its core and a delegation path to different decision procedure implementations, each in charge of solving formulas in some background theory.

The re-evaluation and ground-up rewrite was necessitated, we felt, by the performance characteristics of CVC3. CVC3 has many useful features, but some core aspects of the design led to high memory use, and the use of heavyweight computation (where more nimble engineering approaches could suffice) makes CVC3 a much slower prover than other tools. As these designs are central to CVC3, a new version was preferable to a selective re-engineering, which would have ballooned in short order.

VERSION

This manual page refers to CVC4 version CVC4_RELEASE_STRING.

BUGS

An issue tracker for the CVC4 project is maintained at https://github.com/CVC4/CVC4/issues.

AUTHORS

CVC4 is developed by a team of researchers at Stanford University and the University of Iowa. See the AUTHORS file in the distribution for a full list of contributors.

SEE ALSO

libcvc4(3), libcvc4parser(3)

Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4. It is maintained at http://cvc4.cs.stanford.edu/wiki/.

History

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