THIS(1)

NAME
This - Theorem prover for SMT problems

DESCRIPTION
usage: cvc5 [options] [input-file]

Without an input file, or with `-', cvc5 reads from standard input.

cvc5 options: Most commonly-used cvc5 options:

--incremental | -i
    enable incremental solving [*]

--lang=LANG | --input-language=LANG | -L LANG
    force input language (default is "auto"; see --lang help)

--output=TAG | -o TAG
    Enable output tag.

--parse-only
    exit after parsing input [*]

--preprocess-only
    exit after preprocessing input [*]

--quiet | -q
    decrease verbosity (may be repeated)

--rlimit=N
    set resource limit

--rlimit-per=N | --reproducible-resource-limit=N
    set resource limit per query

--stats
    give statistics on exit [*]

--stats-all
    print unchanged (defaulted) statistics as well [*]

--stats-internal
    print internal (non-public) statistics as well [*]

--tlimit=MS
    set time limit in milliseconds of wall clock time

--tlimit-per=MS
    set time limit per query in milliseconds

--verbose | -v
    increase verbosity (may be repeated)

--verbosity=N
    the verbosity level of cvc5

--decision=MODE | --decision-mode=MODE
    choose decision mode, see --decision=help

--copyright
    show cvc5 copyright information

--early-exit
    do not run destructors at exit; default on except in debug builds [*]

--help | -h
    full command line reference

--help-option-categories
    Print summary of options for each category

--help-regular | -H
    regular command line reference

--interactive
    force interactive shell/non-interactive mode [*]

--print-success
    print the "success" output required of SMT-LIBv2 [*]

--seed=N | --random-seed=N | -s N
    seed for random number generator

--show-config
    show cvc5 static configuration

--version | -V
    identify this cvc5 binary

--force-logic=LOGIC
    set the logic, and override all further user attempts to change it

--strict-parsing
    be less tolerant of non-conforming inputs, this is an alias for --parsing-mode=strict [*]

--dag-thresh=N
    dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)

--expr-depth=N
    print exprs to depth N (0 == default, -1 == no limit)

--output-lang=LANG | --output-language=LANG
    force output language (default is "auto"; see --output-lang help)

--proof-check=MODE
    select internal proof checking mode

--proof-granularity=MODE
    modes for proof granularity

--proof-print-conclusion
    Print conclusion of proof steps when printing AST [*]

--proof-print-reference
    Print reference to original file instead of redeclaring [*]

--enum-inst
    enumerative instantiation: instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown [*]

--full-saturate-quant
    resort to full effort techniques instead of answering unknown due to limited quantifier reasoning. Currently enables enumerative instantiation [*]

--print-inst=MODE
    print format for printing instantiations

--check-abducts
    checks whether produced solutions to get-abduct are correct [*]

--check-interpolants
    checks whether produced solutions to get-interpolant are correct [*]

--check-model-subsolver
    use subsolver to compute values when applicable in calls to get-value and check-models [*]

--check-models
    after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions [*]

--check-proofs
    after UNSAT/VALID, check the generated proof (with proof) [*]

--check-synth-sol
    checks whether produced solutions to functions-to-synthesize satisfy the conjecture [*]

--check-unsat-cores
    after UNSAT/VALID, produce and check an unsat core (expensive) [*]

--debug-check-models
    after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions [*]

--produce-models | -m
    support the get-value and get-model commands [*]

--produce-proofs
    produce proofs, support check-proofs and get-proof [*]

--produce-unsat-cores
    turn on unsat core generation. Unless otherwise specified, cores will be produced using SAT soving under assumptions and preprocessing proofs. [*]

--condense-function-values
    condense values for functions in models rather than explicitly representing them [*]

--default-function-value-mode=MODE
    mode for choosing default values for functions

Additional cvc5 options:

  From the Arithmetic Theory module:

--approx-branch-depth=N
    maximum branch depth the approximate solver is allowed to take (EXPERTS only)

--arith-brab
    whether to use simple rounding, similar to a unit-cube test, for integers [*]

--arith-eq-solver
    whether to use the equality solver in the theory of arithmetic (EXPERTS only) [*]

--arith-exp
    enables non-standard extensions of the arithmetic solver (EXPERTS only) [*]

--arith-prop=MODE
    turns on arithmetic propagation (default is 'old', see --arith-prop=help) (EXPERTS only)

--arith-prop-clauses=N rows shorter than this are propagated as clauses
    (EXPERTS only)

--arith-rewrite-equalities
    turns on the preprocessing rewrite turning equalities into a conjunction of inequalities [*]

--arith-static-learning
    do arithmetic static learning for ite terms based on bounds when static learning is enabled [*]

--collect-pivot-stats
    collect the pivot history (EXPERTS only) [*]

--cut-all-bounded
    turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds (EXPERTS only) [*]

--dio-decomps
    let skolem variables for integer divisibility constraints leak from the dio solver (EXPERTS only) [*]

--dio-solver
    turns on Linear Diophantine Equation solver (Griggio, JSAT 2012) (EXPERTS only) [*]

--dio-turns=N
    turns in a row dio solver cutting gets (EXPERTS only)

--error-selection-rule=RULE
    change the pivot rule for the basic variable (default is 'min', see --pivot-rule help) (EXPERTS only)

--fc-penalties
    turns on degenerate pivot penalties (EXPERTS only) [*]

--heuristic-pivots=N
    the number of times to apply the heuristic pivot rule; if N < 0, this defaults to the number of variables; if this is unset, this is tuned by the logic selection (EXPERTS only)

--lemmas-on-replay-failure
    attempt to use external lemmas if approximate solve integer failed (EXPERTS only) [*]

--maxCutsInContext=N
    maximum cuts in a given context before signalling a restart (EXPERTS only)

--miplib-trick
    turns on the preprocessing step of attempting to infer bounds on miplib problems (EXPERTS only) [*]

--miplib-trick-subs=N
    do substitution for miplib 'tmp' vars if defined in <= N eliminated vars (EXPERTS only)

--new-prop
    use the new row propagation system (EXPERTS only) [*]

--nl-cov
    whether to use the cylindrical algebraic coverings solver for non-linear arithmetic [*]

--nl-cov-force
    forces using the cylindrical algebraic coverings solver, even in cases where it is possibly not safe to do so (EXPERTS only) [*]

--nl-cov-lift=MODE
    choose the Coverings lifting mode (EXPERTS only)

--nl-cov-linear-model=MODE
    whether to use the linear model as initial guess for the cylindrical algebraic coverings solver

--nl-cov-proj=MODE
    choose the Coverings projection operator (EXPERTS only)

--nl-cov-prune
    whether to prune intervals more aggressively (EXPERTS only) [*]

--nl-cov-var-elim
    whether to eliminate variables using equalities before going into the cylindrical algebraic coverings solver. It can not be used when producing proofs right now. (EXPERTS only) [*]

--nl-ext=MODE
    incremental linearization approach to non-linear

--nl-ext-ent-conf
    check for entailed conflicts in non-linear solver (EXPERTS only) [*]

--nl-ext-factor
    use factoring inference in non-linear incremental linearization solver [*]

--nl-ext-flatten-mon
    use inference schema based on flattening monomials [*]

--nl-ext-inc-prec
    whether to increment the precision for irrational function constraints (EXPERTS only) [*]

--nl-ext-purify
    purify non-linear terms at preprocess (EXPERTS only) [*]

--nl-ext-rbound
    use resolution-style inference for inferring new bounds in non-linear incremental linearization solver (EXPERTS only) [*]

--nl-ext-rewrite
    do context-dependent simplification based on rewrites in non-linear solver [*]

--nl-ext-split-zero
    initial splits on zero for all variables (EXPERTS only) [*]

--nl-ext-tf-taylor-deg=N
    initial degree of polynomials for Taylor approximation (EXPERTS only)

--nl-ext-tf-tplanes
    use non-terminating tangent plane strategy for transcendental functions for non-linear incremental linearization solver [*]

--nl-ext-tplanes
    use non-terminating tangent plane strategy for non-linear incremental linearization solver [*]

--nl-ext-tplanes-interleave
    interleave tangent plane strategy for non-linear incremental linearization solver [*]

--nl-icp
    whether to use ICP-style propagations for non-linear arithmetic (EXPERTS only) [*]

--nl-rlv=MODE
    choose mode for using relevance of assertions in non-linear arithmetic (EXPERTS only)

--nl-rlv-assert-bounds use bound inference utility to prune when an assertion
    is entailed by another (EXPERTS only) [*]

--pb-rewrites
    apply pseudo boolean rewrites (EXPERTS only) [*]

--pivot-threshold=N
    sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order (EXPERTS only)

--pp-assert-max-sub-size=N
    threshold for substituting an equality in ppAssert (EXPERTS only)

--prop-row-length=N
    sets the maximum row length to be used in propagation (EXPERTS only)

--replay-early-close-depth=N
    multiples of the depths to try to close the approx log eagerly (EXPERTS only)

--replay-lemma-reject-cut=N
    maximum complexity of any coefficient while outputting replaying cut lemmas (EXPERTS only)

--replay-num-err-penalty=N
    number of solve integer attempts to skips after a numeric failure (EXPERTS only)

--replay-reject-cut=N
    maximum complexity of any coefficient while replaying cuts (EXPERTS only)

--restrict-pivots
    have a pivot cap for simplex at effort levels below fullEffort (EXPERTS only) [*]

--revert-arith-models-on-unsat
    revert the arithmetic model to a known safe model on unsat if one is cached (EXPERTS only) [*]

--rr-turns=N
    round robin turn (EXPERTS only)

--se-solve-int
    attempt to use the approximate solve integer method on standard effort (EXPERTS only) [*]

--simplex-check-period=N
    the number of pivots to do in simplex before rechecking for a conflict on all variables (EXPERTS only)

--soi-qe
    use quick explain to minimize the sum of infeasibility conflicts (EXPERTS only) [*]

--standard-effort-variable-order-pivots=N
    limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule (EXPERTS only)

--unate-lemmas=MODE
    determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help) (EXPERTS only)

--use-approx
    attempt to use an approximate solver (EXPERTS only) [*]

--use-fcsimplex
    use focusing and converging simplex (FMCAD 2013 submission) (EXPERTS only) [*]

--use-soi
    use sum of infeasibility simplex (FMCAD 2013 submission) (EXPERTS only) [*]

  From the Arrays Theory module:

--arrays-eager-index
    turn on eager index splitting for generated array lemmas [*]

--arrays-eager-lemmas
    turn on eager lemma generation for arrays (EXPERTS only) [*]

--arrays-exp
    enable experimental features in the theory of arrays (EXPERTS only) [*]

--arrays-optimize-linear
    turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper) (EXPERTS only) [*]

--arrays-prop=N
    propagation effort for arrays: 0 is none, 1 is some, 2 is full (EXPERTS only)

--arrays-reduce-sharing
    use model information to reduce size of care graph for arrays (EXPERTS only) [*]

--arrays-weak-equiv
    use algorithm from Christ/Hoenicke (SMT 2014) (EXPERTS only) [*]

  From the Bags Theory module:

--bags
    enables the bags solver in applicable logics (EXPERTS only) [*]

  From the Base module:

--err=erroutput | --diagnostic-output-channel=erroutput
    Set the error (or diagnostic) output channel. Writes to stderr for "stderr" or "--", stdout for "stdout" or the given filename otherwise. (EXPERTS only)

--in=input
    Set the error (or diagnostic) output channel. Reads from stdin for "stdin" or "--" and the given filename otherwise. (EXPERTS only)

--out=output | --regular-output-channel=output
    Set the error (or diagnostic) output channel. Writes to stdout for "stdout" or "--", stderr for "stderr" or the given filename otherwise. (EXPERTS only)

--plugin-notify-sat-clause-in-solve
    only inform plugins of SAT clauses when we are in the main solving loop of the SAT solver (EXPERTS only) [*]

--plugin-share-skolems true if we permit sharing theory lemmas and SAT clauses
    with skolems (EXPERTS only) [*]

--rweight=VAL=N
    set a single resource weight (EXPERTS only)

--safe-mode=MODE
    modes for restricting expert options and theories (EXPERTS only)

--stats-every-query
    in incremental mode, print stats after every satisfiability or validity query [*]

--trace=TAG | -t TAG
    trace something (e.g. -t pushpop), can repeat and may contain wildcards like (e.g. -t theory::*) (EXPERTS only)

  From the Bitvector Theory module:

--bitblast=MODE
    choose bitblasting mode, see --bitblast=help

--bitwise-eq
    lift equivalence with one-bit bit-vectors to be boolean operations (EXPERTS only) [*]

--bool-to-bv=MODE
    convert booleans to bit-vectors of size 1 at various levels of aggressiveness, see --bool-to-bv=help

--bv-assert-input
    assert input assertions on user-level 0 instead of assuming them in the bit-vector SAT solver (EXPERTS only) [*]

--bv-eager-eval
    perform eager context-dependent evaluation for applications of bv kinds in the equality engine [*]

--bv-eq-engine
    enable equality engine when possible in bitvector theory (EXPERTS only) [*]

--bv-gauss-elim
    simplify formula via Gaussian Elimination if applicable (EXPERTS only) [*]

--bv-intro-pow2
    introduce bitvector powers of two as a preprocessing pass (EXPERTS only) [*]

--bv-propagate
    use bit-vector propagation in the bit-blaster (EXPERTS only) [*]

--bv-rw-extend-eq
    enable additional rewrites over zero/sign extend over equalities with constants (useful on BV/2017-Preiner-scholl-smt08) (EXPERTS only) [*]

--bv-sat-solver=MODE
    choose which sat solver to use, see --bv-sat-solver=help

--bv-solver=MODE
    choose bit-vector solver, see --bv-solver=help

--bv-to-bool
    lift bit-vectors of size 1 to booleans when possible [*]

  From the Datatypes Theory module:

--cdt-bisimilar
    do bisimilarity check for co-datatypes (EXPERTS only) [*]

--datatypes-exp
    enables reasoning about codatatypes and extended datatype terms (EXPERTS only) [*]

--dt-binary-split
    do binary splits for datatype constructor types (EXPERTS only) [*]

--dt-blast-splits
    when applicable, blast splitting lemmas for all variables at once (EXPERTS only) [*]

--dt-cyclic
    do cyclicity check for datatypes (EXPERTS only) [*]

--dt-infer-as-lemmas
    always send lemmas out instead of making internal inferences (EXPERTS only) [*]

--dt-nested-rec
    allow nested recursion in datatype definitions (EXPERTS only) [*]

--dt-polite-optimize
    turn on optimization for polite combination (EXPERTS only) [*]

--dt-share-sel
    internally use shared selectors across multiple constructors (EXPERTS only) [*]

--sygus-abort-size=N
    tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)

--sygus-fair=MODE
    if and how to apply fairness for sygus

--sygus-fair-max
    use max instead of sum for multi-function sygus conjectures (EXPERTS only) [*]

--sygus-rewriter=MODE
    if and how to apply rewriting for sygus symmetry breaking

--sygus-simple-sym-break=MODE
    if and how to apply simple symmetry breaking based on the grammar for smart enumeration

--sygus-sym-break-lazy lazily add symmetry breaking lemmas for terms (EXPERTS
    only) [*]

--sygus-sym-break-pbe
    sygus symmetry breaking lemmas based on pbe conjectures [*]

--sygus-sym-break-rlv
    add relevancy conditions to symmetry breaking lemmas (EXPERTS only) [*]

  From the Decision Heuristics module:

--jh-rlv-order
    maintain activity-based ordering for decision justification heuristic (EXPERTS only) [*]

--jh-skolem=MODE
    policy for when to satisfy skolem definitions in justification heuristic (EXPERTS only)

--jh-skolem-rlv=MODE
    policy for when to consider skolem definitions relevant in justification heuristic (EXPERTS only)

  From the Expression module:

--type-checking
    type check expressions (EXPERTS only) [*]

--wf-checking
    check that terms passed to API methods are well formed (default false for text interface) (EXPERTS only) [*]

  From the Finite Field Theory module:

--ff
    enables the finite field solver in applicable logics (EXPERTS only) [*]

--ff-bitsum
    parse bitsums (EXPERTS only) [*]

--ff-elim-disjunctive-bit
    rewrite disjunctive bit constraints (or (= x 1) (= x 0)) as (= (* x x) x) (EXPERTS only) [*]

--ff-field-polys
    include field polynomials in Groebner basis computation; don't do this (EXPERTS only) [*]

--ff-solver=MODE
    which field solver (default: 'gb'; see --ff-solver=help) (EXPERTS only)

--ff-trace-gb
    use a traced groebner basis engine (EXPERTS only) [*]

  From the Floating-Point module:

--fp
    enables the floating point theory in applicable logics (EXPERTS only) [*]

--fp-exp
    Allow floating-point sorts of all sizes, rather than only Float32 (8/24) or Float64 (11/53) (experimental) (EXPERTS only) [*]

--fp-lazy-wb
    Enable lazier word-blasting (on preNotifyFact instead of registerTerm) (EXPERTS only) [*]

  From the Driver module:

--dump-difficulty
    dump the difficulty measure after every response to check-sat [*]

--dump-instantiations
    output instantiations of quantified formulas after every UNSAT/VALID response [*]

--dump-instantiations-debug
    output instantiations of quantified formulas after every UNSAT/VALID response, with debug information (EXPERTS only) [*]

--dump-models
    output models after every SAT/INVALID/UNKNOWN response [*]

--dump-proofs
    output proofs after every UNSAT/VALID response [*]

--dump-unsat-cores
    output unsat cores after every UNSAT/VALID response [*]

--dump-unsat-cores-lemmas
    output lemmas in unsat cores after every UNSAT/VALID response [*]

--force-no-limit-cpu-while-dump
    Force no CPU limit when dumping models and proofs (EXPERTS only) [*]

--portfolio-dry-run
    Print the strategies that would be run with --use-portfolio, without executing them (EXPERTS only) [*]

--portfolio-jobs=n
    Number of parallel jobs the portfolio engine can run (EXPERTS only)

--segv-spin
    spin on segfault/other crash waiting for gdb (EXPERTS only) [*]

--show-trace-tags
    show all available tags for tracing (EXPERTS only)

--use-portfolio
    Use internal portfolio mode based on the logic (EXPERTS only) [*]

  From the Parallel module:

--append-learned-literals-to-cubes
    emit learned literals with the cubes (EXPERTS only) [*]

--checks-before-partition=N
    number of standard or full effort checks until partitioning (EXPERTS only)

--checks-between-partitions=N
    number of checks between partitions (EXPERTS only)

--compute-partitions=N make n partitions. n <2 disables computing partitions
    entirely (EXPERTS only)

--partition-check=MODE | --check=MODE
    select whether partitioning happens at full or standard check (EXPERTS only)

--partition-conflict-size=N
    number of literals in a cube; if no partition size is set, then the partition conflict size is chosen to be log2(number of requested partitions) (EXPERTS only)

--partition-start-time=N
    time to start creating partitions in seconds (EXPERTS only)

--partition-strategy=MODE | --partition=MODE
    choose partition strategy mode (EXPERTS only)

--partition-time-interval=N
    time to wait between scatter partitions (EXPERTS only)

--partition-tlimit=N
    time limit for partitioning in seconds (EXPERTS only)

--partition-when=MODE
    choose when to partition (EXPERTS only)

--random-partitioning
    create random partitions (EXPERTS only) [*]

--write-partitions-to=output | --partitions-out=output
    set the output channel for writing partitions (EXPERTS only)

  From the Parser module:

--filesystem-access
    limits the file system access if set to false (EXPERTS only) [*]

--fresh-binders
    construct fresh variables always when parsing binders (EXPERTS only) [*]

--fresh-declarations
    use API interface for fresh constants when parsing declarations and definitions [*]

--global-declarations
    force all declarations and definitions to be global when parsing [*]

--parse-skolem-definitions
    allows the parsing of skolems in the input file (EXPERTS only) [*]

--parsing-mode=MODE
    choose parsing mode, see --parsing-mode=help (EXPERTS only)

--semantic-checks
    enable semantic checks, including type checks (EXPERTS only) [*]

--term-sort-overload
    allow overloading of terms and sorts (EXPERTS only) [*]

  From the Printing module:

--bv-print-consts-as-indexed-symbols
    print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x [*]

--flatten-ho-chains
    print (binary) application chains in a flattened way, e.g. (a b c) rather than ((a b) c) (EXPERTS only) [*]

--model-u-print=MODE
    determines how to print uninterpreted elements in models

--print-arith-lit-token
    print rationals and negative arithmetic literals as lexed tokens, e.g. 1/4, -1.5 (EXPERTS only) [*]

--print-skolem-definitions
    print skolems based on their definitions e.g. @ARRAY_DIFF_N prints instead as (@array.diff A B) (EXPERTS only) [*]

  From the Proof module:

--check-proof-steps
    Check proof steps for satisfiability, for refutation soundness testing. Note this checks only steps for non-core proof rules (EXPERTS only) [*]

--check-proofs-complete
    treat an incomplete proof as a failure (enabled by default in safe builds) (EXPERTS only) [*]

--drat-binary-format
    Print the DRAT proof in binary format (EXPERTS only) [*]

--lfsc-expand-trust
    Print the children of trusted proof steps (EXPERTS only) [*]

--lfsc-flatten
    Flatten steps in the LFSC proof (EXPERTS only) [*]

--opt-res-reconstruction-size
    Optimize resolution reconstruction to reduce proof size [*]

--print-dot-clusters
    Whether the proof node clusters (e.g. SAT, CNF, INPUT) will be printed when using the dot format or not. (EXPERTS only) [*]

--proof-alethe-define-skolems
    In Alethe proofs, use define-funs in proof preamble for Skolemization terms (EXPERTS only) [*]

--proof-alethe-res-pivots
    Add pivots to Alethe resolution steps (EXPERTS only) [*]

--proof-allow-trust
    Whether to allow trust in the proof printer (when applicable) (EXPERTS only) [*]

--proof-chain-m-res
    Use chain multiset resolution [*]

--proof-dag-global
    Dagify terms in proofs using global definitions (EXPERTS only) [*]

--proof-dot-dag
    Indicates if the dot proof will be printed as a DAG or as a tree (EXPERTS only) [*]

--proof-elim-subtypes
    Eliminate subtypes (mixed arithmetic) in proofs (EXPERTS only) [*]

--proof-format-mode=MODE
    select language of proof output (EXPERTS only)

--proof-log
    Proof logging mode (EXPERTS only) [*]

--proof-pedantic=N
    assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof (EXPERTS only)

--proof-pp-merge
    merge subproofs in final proof post-processor (EXPERTS only) [*]

--proof-pre-simp-lookahead=N
    the lookahead depth for merging proofs at previsit (EXPERTS only)

--proof-prune-input
    Prune unused input assumptions from final scope (EXPERTS only) [*]

--proof-rewrite-rcons-rec-limit=N
    the matching recursion limit for reconstructing proofs of theory rewrites

--proof-rewrite-rcons-step-limit=N
    the limit of steps considered for reconstructing proofs of theory rewrites

--prop-proof-mode=MODE modes for the type of proof generated by the SAT solver

--sat-proof-min-dimacs Minimize the DIMACs emitted when prop-proof-mode is set
    to sat-external-prove (EXPERTS only) [*]

  From the SAT Layer module:

--minisat-dump-dimacs
    instead of solving minisat dumps the asserted clauses in Dimacs format (EXPERTS only) [*]

--minisat-simplification=MODE
    Simplifications to be performed by Minisat. (EXPERTS only)

--preregister-mode=MODE
    Modes for when to preregister literals.

--random-freq=P | --random-frequency=P
    sets the frequency of random decisions in the sat solver (P=0.0 by default) (EXPERTS only)

--restart-int-base=N
    sets the base restart interval for the sat solver (N=25 by default) (EXPERTS only)

--restart-int-inc=F
    sets the restart interval increase factor for the sat solver (F=3.0 by default) (EXPERTS only)

--sat-random-seed=N
    sets the random seed for the sat solver

--sat-solver=MODE
    choose which sat solver to use, see --sat-solver=help (EXPERTS only)

  From the Quantifiers module:

--cbqi
    enable conflict-based quantifier instantiation [*]

--cbqi-all-conflict
    add all available conflicting instances during conflict-based instantiation [*]

--cbqi-mode=MODE
    what effort to apply conflict find mechanism

--cbqi-skip-rd
    optimization, skip instances based on possibly irrelevant portions of quantified formulas (EXPERTS only) [*]

--cbqi-tconstraint
    enable entailment checks for t-constraints in cbqi algorithm (EXPERTS only) [*]

--cbqi-vo-exp
    cbqi experimental variable ordering (EXPERTS only) [*]

--cegis-sample=MODE
    mode for using samples in the counterexample-guided inductive synthesis loop

--cegqi
    turns on counterexample-based quantifier instantiation [*]

--cegqi-all
    apply counterexample-based instantiation to all quantified formulas (EXPERTS only) [*]

--cegqi-bv
    use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors [*]

--cegqi-bv-ineq=MODE
    choose mode for handling bit-vector inequalities with counterexample-guided instantiation (EXPERTS only)

--cegqi-bv-interleave-value
    interleave model value instantiation with word-level inversion approach (EXPERTS only) [*]

--cegqi-bv-linear
    linearize adder chains for variables (EXPERTS only) [*]

--cegqi-bv-rm-extract
    replaces extract terms with variables for counterexample-guided instantiation for bit-vectors (EXPERTS only) [*]

--cegqi-bv-solve-nl
    try to solve non-linear bv literals using model value projections (EXPERTS only) [*]

--cegqi-full
    turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation (EXPERTS only) [*]

--cegqi-inf-int
    use integer infinity for vts in counterexample-based quantifier instantiation (EXPERTS only) [*]

--cegqi-inf-real
    use real infinity for vts in counterexample-based quantifier instantiation (EXPERTS only) [*]

--cegqi-innermost
    only process innermost quantified formulas in counterexample-based quantifier instantiation [*]

--cegqi-midpoint
    choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation [*]

--cegqi-min-bounds
    use minimally constrained lower/upper bound for counterexample-based quantifier instantiation (EXPERTS only) [*]

--cegqi-multi-inst
    when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation (EXPERTS only) [*]

--cegqi-nested-qe
    process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation [*]

--cegqi-nopt
    non-optimal bounds for counterexample-based quantifier instantiation (EXPERTS only) [*]

--cegqi-round-up-lia
    round up integer lower bounds in substitutions for counterexample-based quantifier instantiation (EXPERTS only) [*]

--cond-var-split-quant=MODE
    split quantified formulas that lead to variable eliminations (EXPERTS only)

--conjecture-gen
    generate candidate conjectures for inductive proofs (EXPERTS only) [*]

--conjecture-gen-gt-enum=N
    number of ground terms to generate for model filtering (EXPERTS only)

--conjecture-gen-max-depth=N
    maximum depth of terms to consider for conjectures (EXPERTS only)

--conjecture-gen-per-round=N
    number of conjectures to generate per instantiation round (EXPERTS only)

--cons-exp-triggers
    use constructor expansion for single constructor datatypes triggers (EXPERTS only) [*]

--dt-stc-ind
    apply strengthening for existential quantification over datatypes based on structural induction (EXPERTS only) [*]

--dt-var-exp-quant
    expand datatype variables bound to one constructor in quantifiers (EXPERTS only) [*]

--e-matching
    whether to do heuristic E-matching [*]

--elim-taut-quant
    eliminate tautological disjuncts of quantified formulas [*]

--enum-inst-interleave interleave enumerative instantiation with other
    techniques [*]

--enum-inst-limit=N
    maximum number of rounds of enumerative instantiation to apply (-1 means no limit) (EXPERTS only)

--enum-inst-rd
    whether to use relevant domain first for enumerative instantiation strategy (EXPERTS only) [*]

--enum-inst-stratify
    stratify effort levels in enumerative instantiation, which favors speed over fairness (EXPERTS only) [*]

--enum-inst-sum
    enumerating tuples of quantifiers by increasing the sum of indices, rather than the maximum [*]

--ext-rewrite-quant
    apply extended rewriting to bodies of quantified formulas [*]

--finite-model-find
    use finite model finding heuristic for quantifier instantiation [*]

--fmf-bound
    finite model finding on bounded quantification [*]

--fmf-bound-blast
    send all instantiations for bounded ranges in a single round (EXPERTS only) [*]

--fmf-bound-lazy
    enforce bounds for bounded quantification lazily via use of proxy variables (EXPERTS only) [*]

--fmf-fun
    find models for recursively defined functions, assumes functions are admissible (EXPERTS only) [*]

--fmf-fun-rlv
    find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant (EXPERTS only) [*]

--fmf-mbqi=MODE
    choose mode for model-based quantifier instantiation (EXPERTS only)

--fmf-type-completion-thresh=N
    the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted

--full-sygus-verify
    resort to full effort techniques instead of answering unknown when checking sygus candidates (EXPERTS only) [*]

--global-negate
    do global negation of input formula (EXPERTS only) [*]

--ho-elim
    eagerly eliminate higher-order constraints (EXPERTS only) [*]

--ho-elim-store-ax
    use store axiom during ho-elim (EXPERTS only) [*]

--ho-matching
    do higher-order matching algorithm for triggers with variable operators (EXPERTS only) [*]

--ho-merge-term-db
    merge term indices modulo equality (EXPERTS only) [*]

--ieval=MODE
    mode for using instantiation evaluation

--increment-triggers
    generate additional triggers as needed during search (EXPERTS only) [*]

--inst-local
    Instantiations are local to the SAT context [*]

--inst-max-level=N
    maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) (EXPERTS only)

--inst-max-rounds=N
    maximum number of instantiation rounds (-1 == no limit, default)

--inst-no-entail
    do not consider instances of quantified formulas that are currently entailed [*]

--inst-when=MODE
    when to apply instantiation

--inst-when-phase=N
    instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen (EXPERTS only)

--int-wf-ind
    apply strengthening for integers based on well-founded induction (EXPERTS only) [*]

--ite-dtt-split-quant
    split ites with dt testers as conditions (EXPERTS only) [*]

--ite-lift-quant=MODE
    ite lifting mode for quantified formulas

--literal-matching=MODE
    choose literal matching mode (EXPERTS only)

--macros-quant
    perform quantifiers macro expansion [*]

--macros-quant-mode=MODE
    mode for quantifiers macro expansion

--mbqi
    use model-based quantifier instantiation [*]

--mbqi-check-timeout=N timeout (in milliseconds) for verifying subcalls for
    model-based instantiation (0 == no limit)

--mbqi-enum
    use fast enumeration to augment instantiations from MBQI [*]

--mbqi-enum-ext-vars-grammar
    include variables defined in terms of others in grammars for fast enumerative mbqi (EXPERTS only) [*]

--mbqi-enum-free-syms-grammar
    include free symbols from the body of the quantified formula in grammars for fast enumerative mbqi (EXPERTS only) [*]

--mbqi-enum-global-syms-grammar
    include global symbols from all available assertions in grammars for fast enumerative mbqi (EXPERTS only) [*]

--mbqi-interleave
    interleave model-based quantifier instantiation with other techniques (EXPERTS only) [*]

--mbqi-nested-check
    check nested quantified formulas in MBQI (EXPERTS only) [*]

--mbqi-one-inst-per-round
    only add one instantiation per quantifier per round for mbqi [*]

--miniscope-quant=MODE miniscope mode for quantified formulas

--miniscope-quant-user miniscope quantified formulas with user patterns [*]

--multi-trigger-cache
    caching version of multi triggers [*]

--multi-trigger-linear implementation of multi triggers where maximum number
    of instantiations is linear wrt number of ground terms [*]

--multi-trigger-priority
    only try multi triggers if single triggers give no instantiations [*]

--multi-trigger-when-single
    select multi triggers when single triggers exist [*]

--oracles
    Enable interface to external oracles (EXPERTS only) [*]

--partial-triggers
    use triggers that do not contain all free variables (EXPERTS only) [*]

--pool-inst
    pool-based instantiation: instantiate with ground terms occurring in user-specified pools (EXPERTS only) [*]

--pre-skolem-quant=MODE
    modes to apply skolemization eagerly to bodies of quantified formulas

--pre-skolem-quant-nested
    apply skolemization to nested quantified formulas (EXPERTS only) [*]

--prenex-quant=MODE
    prenex mode for quantified formulas (EXPERTS only)

--prenex-quant-user
    prenex quantified formulas with user patterns [*]

--print-inst-full
    print instantiations for formulas that do not have given identifiers [*]

--purify-triggers
    purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1 (EXPERTS only) [*]

--quant-alpha-equiv
    infer alpha equivalence between quantified formulas [*]

--quant-dsplit=MODE
    mode for dynamic quantifiers splitting

--quant-fun-wd
    assume that function defined by quantifiers are well defined (EXPERTS only) [*]

--quant-ind
    use all available techniques for inductive reasoning (EXPERTS only) [*]

--quant-rep-mode=MODE
    selection mode for representatives in quantifiers engine (EXPERTS only)

--register-quant-body-terms
    consider ground terms within bodies of quantified formulas for matching (EXPERTS only) [*]

--relational-triggers
    choose relational triggers such as x = f(y), x >= f(y) (EXPERTS only) [*]

--relevant-triggers
    prefer triggers that are more relevant based on SInE style analysis [*]

--sub-cbqi
    Enable conflict-based instantiation subsolver strategy [*]

--sub-cbqi-timeout=N
    Timeout (in milliseconds) for subsolver calls for sub-cbqi (EXPERTS only)

--sygus
    support SyGuS commands [*]

--sygus-add-const-grammar
    statically add constants appearing in conjecture to grammars [*]

--sygus-arg-relevant
    static inference techniques for computing whether arguments of functions-to-synthesize are relevant (EXPERTS only) [*]

--sygus-auto-unfold
    enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems (EXPERTS only) [*]

--sygus-bool-ite-return-const
    Only use Boolean constants for return values in unification-based function synthesis (EXPERTS only) [*]

--sygus-core-connective
    use unsat core analysis to construct Boolean connective to sygus conjectures [*]

--sygus-crepair-abort
    abort if constant repair techniques are not applicable (EXPERTS only) [*]

--sygus-enum=MODE
    mode for sygus enumeration

--sygus-enum-fast-num-consts=N
    the branching factor for the number of interpreted constants to consider for each size when using --sygus-enum=fast (EXPERTS only)

--sygus-enum-random-p=P
    the parameter of the geometric distribution used to determine the size of terms generated by --sygus-enum=random (EXPERTS only)

--sygus-eval-unfold=MODE
    modes for sygus evaluation unfolding

--sygus-expr-miner-check-timeout=N
    timeout (in milliseconds) for satisfiability checks in expression miners (EXPERTS only)

--sygus-filter-sol=MODE
    mode for filtering sygus solutions (EXPERTS only)

--sygus-filter-sol-rev compute backwards filtering to compute whether previous
    solutions are filtered based on later ones (EXPERTS only) [*]

--sygus-grammar-cons=MODE
    mode for SyGuS grammar construction

--sygus-grammar-ho-partial
    add partial function applications to the grammar (EXPERTS only) [*]

--sygus-grammar-norm
    statically normalize sygus grammars based on flattening (linearization) (EXPERTS only) [*]

--sygus-grammar-use-disj
    use disjunctions in internally generated grammars. this is set to false when solving abduction queries. (EXPERTS only) [*]

--sygus-inference=MODE mode for preprocessing arbitrary inputs to sygus
    conjectures (EXPERTS only)

--sygus-inst
    Enable SyGuS instantiation quantifiers module [*]

--sygus-inst-mode=MODE select instantiation lemma mode (EXPERTS only)

--sygus-inst-scope=MODE
    select scope of ground terms (EXPERTS only)

--sygus-inst-term-sel=MODE
    granularity for ground terms (EXPERTS only)

--sygus-inv-templ=MODE template mode for sygus invariant synthesis (weaken
    pre-condition, strengthen post-condition, or none)

--sygus-inv-templ-when-sg
    use invariant templates (with solution reconstruction) for syntax guided problems (EXPERTS only) [*]

--sygus-min-grammar
    statically minimize sygus grammars [*]

--sygus-out=MODE
    output mode for sygus

--sygus-pbe
    enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures [*]

--sygus-pbe-multi-fair when using multiple enumerators, ensure that we only
    register value of minimial term size (EXPERTS only) [*]

--sygus-pbe-multi-fair-diff=N
    when using multiple enumerators, ensure that we only register values of minimial term size plus this value (default 0) (EXPERTS only)

--sygus-qe-preproc
    use quantifier elimination as a preprocessing step for sygus (EXPERTS only) [*]

--sygus-query-gen=MODE mode for generating interesting satisfiability queries
    using SyGuS, for internal fuzzing (EXPERTS only)

--sygus-query-gen-dump-files=MODE
    mode for dumping external files corresponding to interesting satisfiability queries with sygus-query-gen (EXPERTS only)

--sygus-query-gen-filter-solved
    do not print queries that are solved (EXPERTS only) [*]

--sygus-query-gen-thresh=N
    number of points that we allow to be equal for enumerating satisfiable queries with sygus-query-gen (EXPERTS only)

--sygus-rec-fun
    enable efficient support for recursive functions in sygus (EXPERTS only) [*]

--sygus-rec-fun-eval-limit=N
    use a hard limit for how many times in a given evaluator call a recursive function can be evaluated (so infinite loops can be avoided) (EXPERTS only)

--sygus-rec-fun-infer
    automatically infer recursive definitions for sygus (EXPERTS only) [*]

--sygus-repair-const
    use approach to repair constants in sygus candidate solutions [*]

--sygus-repair-const-timeout=N
    timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions (EXPERTS only)

--sygus-rr-synth-accel add dynamic symmetry breaking clauses based on
    candidate rewrites (EXPERTS only) [*]

--sygus-rr-synth-check use satisfiability check to verify correctness of
    candidate rewrites (EXPERTS only) [*]

--sygus-rr-synth-filter-cong
    filter candidate rewrites based on congruence (EXPERTS only) [*]

--sygus-rr-synth-filter-match
    filter candidate rewrites based on matching (EXPERTS only) [*]

--sygus-rr-synth-filter-nl
    filter non-linear candidate rewrites (EXPERTS only) [*]

--sygus-rr-synth-filter-order
    filter candidate rewrites based on variable ordering (EXPERTS only) [*]

--sygus-rr-synth-input-nvars=N
    the maximum number of variables per type that appear in rewrites from sygus-rr-synth-input (EXPERTS only)

--sygus-rr-synth-rec
    synthesize rewrite rules over all sygus grammar types recursively (EXPERTS only) [*]

--sygus-sample-fp-uniform
    sample floating-point values uniformly instead of in a biased fashion (EXPERTS only) [*]

--sygus-sample-grammar when applicable, use grammar for choosing sample points
    (EXPERTS only) [*]

--sygus-samples=N
    number of points to consider when doing sygus rewriter sample testing (EXPERTS only)

--sygus-si=MODE
    mode for processing single invocation synthesis conjectures

--sygus-si-abort
    abort if synthesis conjecture is not single invocation [*]

--sygus-si-rcons=MODE
    policy for reconstructing solutions for single invocation conjectures

--sygus-si-rcons-limit=N
    number of rounds of enumeration to use during solution reconstruction (negative means unlimited) (EXPERTS only)

--sygus-si-rcons-p=P
    the parameter of the geometric distribution used to determine the number of unification patterns generated by single invocation techniques. (EXPERTS only)

--sygus-stream
    enumerate a stream of solutions instead of terminating after the first one [*]

--sygus-unif-cond-independent-no-repeat-sol
    Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis (EXPERTS only) [*]

--sygus-unif-pi=MODE
    mode for synthesis via piecewise-indepedent unification

--sygus-unif-shuffle-cond
    Shuffle condition pool when building solutions (may change solutions sizes) (EXPERTS only) [*]

--sygus-verify-inst-max-rounds=N
    maximum number of instantiation rounds for sygus verification calls (-1 == no limit, default is 10) (EXPERTS only)

--sygus-verify-timeout=N
    timeout (in milliseconds) for verifying satisfiability of synthesized terms (0 == no limit)

--term-db-mode=MODE
    which ground terms to consider for instantiation

--trigger-active-sel=MODE
    selection mode to activate triggers (EXPERTS only)

--trigger-sel=MODE
    selection mode for triggers

--user-pat=MODE
    policy for handling user-provided patterns for quantifier instantiation

--user-pool=MODE
    policy for handling user-provided pools for quantifier instantiation (EXPERTS only)

--var-elim-quant
    enable simple variable elimination for quantified formulas [*]

--var-ent-eq-elim-quant
    enable variable elimination for quantified formulas that infers entailed equalities corresponding to eliminations [*]

--var-ineq-elim-quant
    enable variable elimination based on infinite projection of unbound arithmetic variables [*]

  From the Separation Logic Theory module:

--sep
    enables the separation logic solver in applicable logics (EXPERTS only) [*]

--sep-min-refine
    only add refinement lemmas for minimal (innermost) assertions (EXPERTS only) [*]

--sep-pre-skolem-emp
    eliminate emp constraint at preprocess time (EXPERTS only) [*]

  From the Sets Theory module:

--rels-exp
    enable the relations extension of the theory of sets (EXPERTS only) [*]

--sets-card-exp
    enable the cardinality extension of the theory of sets (EXPERTS only) [*]

--sets-exp
    enable extended symbols such as complement and universe in theory of sets (EXPERTS only) [*]

--sets-proxy-lemmas
    introduce proxy variables eagerly to shorten lemmas (EXPERTS only) [*]

  From the SMT Layer module:

--abstract-values
    in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard (EXPERTS only) [*]

--ackermann
    eliminate functions by ackermannization (EXPERTS only) [*]

--bv-to-int-use-pow2
    use internal pow2 operator when translating shift notes (EXPERTS only) [*]

--bvand-integer-granularity=N
    granularity to use in --solve-bv-as-int mode and for iand operator (experimental) (EXPERTS only)

--deep-restart=MODE
    mode for deep restarts (EXPERTS only)

--deep-restart-factor=F
    sets the threshold for average assertions per literal before a deep restart (EXPERTS only)

--difficulty-mode=MODE choose output mode for get-difficulty, see
    --difficulty-mode=help (EXPERTS only)

--early-ite-removal
    remove ITEs early in preprocessing (EXPERTS only) [*]

--ext-rew-prep=MODE
    mode for using extended rewriter as a preprocessing pass, see --ext-rew-prep=help (EXPERTS only)

--foreign-theory-rewrite
    Cross-theory rewrites (EXPERTS only) [*]

--iand-mode=mode
    Set the refinement scheme for integer AND (EXPERTS only)

--interpolants-mode=MODE
    choose interpolants production mode, see --interpolants-mode=help

--ite-simp
    turn on ite simplification (Kim (and Somenzi) et al., SAT 2009) (EXPERTS only) [*]

--learned-rewrite
    rewrite the input based on learned literals [*]

--minimal-unsat-cores
    if an unsat core is produced, it is reduced to a minimal unsat core (EXPERTS only) [*]

--model-cores=MODE
    mode for producing model cores

--model-var-elim-uneval
    allow variable elimination based on unevaluatable terms to variables (EXPERTS only) [*]

--on-repeat-ite-simp
    do the ite simplification pass again if repeating simplification (EXPERTS only) [*]

--print-cores-full
    print all formulas regardless of whether they are named, e.g. in unsat cores [*]

--produce-abducts
    support the get-abduct command [*]

--produce-assertions | --interactive-mode
    keep an assertions list. Note this option is always enabled. [*]

--produce-assignments
    support the get-assignment command [*]

--produce-difficulty
    enable tracking of difficulty. [*]

--produce-interpolants turn on interpolation generation. [*]

--produce-learned-literals
    produce learned literals, support get-learned-literals [*]

--produce-unsat-assumptions
    turn on unsat assumptions generation [*]

--proof-mode=MODE
    choose proof mode, see --proof-mode=help (EXPERTS only)

--repeat-simp
    make multiple passes with nonclausal simplifier (EXPERTS only) [*]

--simp-ite-compress
    enables compressing ites after ite simplification (EXPERTS only) [*]

--simp-with-care
    enables simplifyWithCare in ite simplificiation (EXPERTS only) [*]

--simplification=MODE | --simplification-mode=MODE
    choose simplification mode, see --simplification=help

--simplification-bcp
    apply Boolean constant propagation as a substitution during simplification (EXPERTS only) [*]

--solve-bv-as-int=MODE mode for translating BVAnd to integer

--solve-int-as-bv=N
    attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)

--solve-real-as-int
    attempt to solve a pure real satisfiable problem as an integer problem (for non-linear) [*]

--sort-inference
    calculate sort inference of input problem, convert the input based on monotonic sorts (EXPERTS only) [*]

--static-learning
    use static learning (on by default) [*]

--timeout-core-timeout=N
    timeout (in milliseconds) for satisfiability checks for timeout cores (EXPERTS only)

--unconstrained-simp
    turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis). Fully supported only in (subsets of) the logic QF_ABV. (EXPERTS only) [*]

--unsat-cores-mode=MODE
    choose unsat core mode, see --unsat-cores-mode=help (EXPERTS only)

  From the Strings Theory module:

--re-elim=MODE
    regular expression elimination mode

--re-first-class
    allow regular expressions as first class terms (EXPERTS only) [*]

--re-inter-mode=MODE
    determines which regular expressions intersections to compute (EXPERTS only)

--seq-array=MODE
    use array-inspired solver for sequence updates in eager or lazy mode (EXPERTS only)

--strings-alpha-card=N the assumed cardinality of the alphabet of characters
    for strings, which is a prefix of the interval of unicode code points in the SMT-LIB standard (EXPERTS only)

--strings-check-entail-len
    check entailment between length terms to reduce splitting [*]

--strings-deq-ext
    use extensionality for string disequalities [*]

--strings-eager-eval
    perform eager context-dependent evaluation for applications of string kinds in the equality engine [*]

--strings-eager-len-re use regular expressions for eager length conflicts [*]

--strings-eager-reg
    do registration lemmas for terms during preregistration. If false, do registration lemmas for terms when they appear in asserted literals (EXPERTS only) [*]

--strings-eager-solver use the eager solver [*]

--strings-exp
    experimental features in the theory of strings [*]

--strings-ff
    do flat form inferences (EXPERTS only) [*]

--strings-fmf
    the finite model finding used by the theory of strings [*]

--strings-infer-as-lemmas
    always send lemmas out instead of making internal inferences (EXPERTS only) [*]

--strings-infer-sym
    generalized inferences in strings based on proxy symbols (EXPERTS only) [*]

--strings-lazy-pp
    perform string preprocessing lazily [*]

--strings-len-norm
    strings length normalization lemma (EXPERTS only) [*]

--strings-mbr
    use models to avoid reductions for extended functions that introduce quantified formulas [*]

--strings-model-max-len=N
    The maximum size of string values in models (EXPERTS only)

--strings-process-loop-mode=MODE
    determines how to process looping string equations

--strings-re-derive-conf
    use regular expression derive for conflict finding (EXPERTS only) [*]

--strings-re-posc-eager
    eager reduction of positive membership into concatenation (EXPERTS only) [*]

--strings-rec-arith-approx
    use possibly recursive reasoning when finding approximations for arithmetic string terms (EXPERTS only) [*]

--strings-regexp-inclusion
    use regular expression inclusion for finding conflicts and avoiding regular expression unfolding [*]

--strings-rexplain-lemmas
    regression explanations for string lemmas (EXPERTS only) [*]

  From the Theory Layer module:

--assign-function-values
    assign values for uninterpreted functions in models (EXPERTS only) [*]

--conflict-process=MODE
    mode for processing theory conflicts (EXPERTS only)

--ee-mode=MODE
    mode for managing equalities across theory solvers

--lemma-inprocess=MODE Modes for inprocessing lemmas. (EXPERTS only)

--lemma-inprocess-infer-eq-lit
    Infer equivalent literals when using lemma inprocess (EXPERTS only) [*]

--lemma-inprocess-subs=MODE
    Modes for substitutions for inprocessing lemmas. (EXPERTS only)

--relevance-filter
    enable analysis of relevance of asserted literals with respect to the input formula (EXPERTS only) [*]

--tc-mode=MODE
    mode for theory combination (EXPERTS only)

--theoryof-mode=MODE
    mode for Theory::theoryof() (EXPERTS only)

  From the Uninterpreted Functions Theory module:

--eager-arith-bv-conv
    eagerly expand bit-vector to arithmetic conversions during preprocessing [*]

--model-based-arith-bv-conv
    model-based inferences for bit-vector to arithmetic conversions (EXPERTS only) [*]

--symmetry-breaker
    use UF symmetry breaker (Deharbe et al., CADE 2011) [*]

--uf-card-exp
    allows logics with UF+cardinality (EXPERTS only) [*]

--uf-ho-exp
    enables the higher-order logic solver in applicable logics (EXPERTS only) [*]

--uf-ho-ext
    apply extensionality on function symbols (EXPERTS only) [*]

--uf-lambda-qe
    apply quantifier elimination eagerly when two lambdas are equated (EXPERTS only) [*]

--uf-lazy-ll
    do lambda lifting lazily [*]

--uf-ss=MODE
    mode of operation for uf with cardinality solver.

--uf-ss-abort-card=N
    tells the uf with cardinality to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)

--uf-ss-fair
    use fair strategy for finite model finding multiple sorts [*]

--uf-ss-fair-monotone
    group monotone sorts when enforcing fairness for finite model finding (EXPERTS only) [*]

[*] Each of these options has a --no-OPTIONNAME variant, which reverses the

    sense of the option.

compiled with GCC version 15.2.0 on Jan 23 2026 14:45:16

COPYRIGHT
Copyright © 2009-2025 by the authors and their institutional affiliations listed at https://cvc5.github.io/people.html

This build of cvc5 uses GPLed libraries, and is thus covered by the GNU General Public License (GPL) version 3. Versions of cvc5 are available that are covered by the (modified) BSD license. If you want to license cvc5 under this license, please configure cvc5 with the "--no-gpl" option before building from sources.

THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE AT YOUR OWN RISK.

This version of cvc5 is linked against the following non-(L)GPL'ed third party libraries.

    CaDiCaL - Simplified Satisfiability Solver See https://github.com/arminbiere/cadical for copyright information.

    CryptoMiniSat - An Advanced SAT Solver See https://github.com/msoos/cryptominisat for copyright information.

    SymFPU - The Symbolic Floating Point Unit See https://github.com/martin-cs/symfpu/tree/CVC4 for copyright information.

This version of cvc5 is linked against the following third party libraries covered by the GPLv3 license. See licenses/gpl-3.0.txt for more information.

    CLN - Class Library for Numbers See http://www.ginac.de/CLN for copyright information.

See the file COPYING (distributed with the source code, and with all binaries) for the full cvc5 copyright, licensing, and (lack of) warranty information.

SEE ALSO
The full documentation for This is maintained as a Texinfo manual. If the info and This programs are properly installed at your site, the command

    info This

should give you access to the complete manual.