/******************************************************************************

 * Top contributors (to current version):

 *   Tim King, Gereon Kremer, Andrew Reynolds

 *

 * This file is part of the cvc5 project.

 *

 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS

 * in the top-level source directory and their institutional affiliations.

 * All rights reserved.  See the file COPYING in the top-level source

 * directory for licensing information.

 * ****************************************************************************

 *

 * Options utilities used in the driver.

 */

#include "main/options.h"

#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)

// force use of optreset; mingw32 croaks on argv-switching otherwise

#include "base/cvc5config.h"

#define _BSD_SOURCE

#undef HAVE_DECL_OPTRESET

#define HAVE_DECL_OPTRESET 1

#define CVC5_IS_NOT_REALLY_BSD

#endif /* !_BSD_SOURCE && __MINGW32__ && !__MINGW64__ */

#ifdef __MINGW64__

extern int optreset;

#endif /* __MINGW64__ */

#include <getopt.h>

// clean up

#ifdef CVC5_IS_NOT_REALLY_BSD

#  undef _BSD_SOURCE

#endif /* CVC5_IS_NOT_REALLY_BSD */

#include "base/check.h"

#include "base/output.h"

#include "options/option_exception.h"

#include "util/didyoumean.h"

#include <cstring>

#include <iostream>

#include <limits>

namespace cvc5::main {

// clang-format off

R"FOOBAR(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-lang=LANG | --output-language=LANG

                         force output language (default is "auto"; see

                         --output-lang help)

  --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 [*]

  --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)

  --copyright            show cvc5 copyright information

  --help | -h            full command line reference

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

  --show-config          show cvc5 static configuration

  --version | -V         identify this cvc5 binary

  --strict-parsing       be less tolerant of non-conforming inputs [*]

  --produce-assertions | --interactive-mode

                         keep an assertions list (enables get-assertions

                         command) [*]

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

)FOOBAR";

R"FOOBAR(Additional cvc5 options:

From the Arithmetic Theory module:

  --approx-branch-depth=N

                         maximum branch depth the approximate solver is allowed

                         to take

  --arith-brab           whether to use simple rounding, similar to a unit-cube

                         test, for integers [*]

  --arith-cong-man       (experimental) whether to use the congruence manager

                         when the equality solver is enabled [*]

  --arith-eq-solver      whether to use the equality solver in the theory of

                         arithmetic [*]

  --arith-no-partial-fun do not use partial function semantics for arithmetic

                         (not SMT LIB compliant) [*]

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

                         --arith-prop=help)

  --arith-prop-clauses=N rows shorter than this are propagated as clauses

  --arith-rewrite-equalities

                         turns on the preprocessing rewrite turning equalities

                         into a conjunction of inequalities [*]

  --collect-pivot-stats  collect the pivot history [*]

  --cut-all-bounded      turns on the integer solving step of periodically

                         cutting all integer variables that have both upper and

                         lower bounds [*]

  --dio-decomps          let skolem variables for integer divisibility

                         constraints leak from the dio solver [*]

  --dio-solver           turns on Linear Diophantine Equation solver (Griggio,

                         JSAT 2012) [*]

  --dio-turns=N          turns in a row dio solver cutting gets

  --error-selection-rule=RULE

                         change the pivot rule for the basic variable (default

                         is 'min', see --pivot-rule help)

  --fc-penalties         turns on degenerate pivot penalties [*]

  --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

  --lemmas-on-replay-failure

                         attempt to use external lemmas if approximate solve

                         integer failed [*]

  --maxCutsInContext=N   maximum cuts in a given context before signalling a

                         restart

  --miplib-trick         turns on the preprocessing step of attempting to infer

                         bounds on miplib problems [*]

  --miplib-trick-subs=N  do substitution for miplib 'tmp' vars if defined in <=

                         N eliminated vars

  --new-prop             use the new row propagation system [*]

  --nl-cad               whether to use the cylindrical algebraic decomposition

                         solver for non-linear arithmetic [*]

  --nl-cad-initial       whether to use the linear model as initial guess for

                         the cylindrical algebraic decomposition solver [*]

  --nl-cad-lift=MODE     choose the CAD lifting mode (EXPERTS only)

  --nl-cad-proj=MODE     choose the CAD projection operator (EXPERTS only)

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

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

  --nl-ext-factor        use factoring inference in non-linear incremental

                         linearization solver [*]

  --nl-ext-inc-prec      whether to increment the precision for irrational

                         function constraints [*]

  --nl-ext-purify        purify non-linear terms at preprocess [*]

  --nl-ext-rbound        use resolution-style inference for inferring new bounds

                         in non-linear incremental linearization solver [*]

  --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 [*]

  --nl-ext-tf-taylor-deg=N

                         initial degree of polynomials for Taylor approximation

  --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 [*]

  --nl-rlv=MODE          choose mode for using relevance of assertions in

                         non-linear arithmetic

  --nl-rlv-assert-bounds use bound inference utility to prune when an assertion

                         is entailed by another [*]

  --pb-rewrites          apply pseudo boolean rewrites [*]

  --pivot-threshold=N    sets the number of pivots using --pivot-rule per basic

                         variable per simplex instance before using variable

                         order

  --pp-assert-max-sub-size=N

                         threshold for substituting an equality in ppAssert

  --prop-row-length=N    sets the maximum row length to be used in propagation

  --replay-early-close-depth=N

                         multiples of the depths to try to close the approx log

                         eagerly

  --replay-lemma-reject-cut=N

                         maximum complexity of any coefficient while outputting

                         replaying cut lemmas

  --replay-num-err-penalty=N

                         number of solve integer attempts to skips after a

                         numeric failure

  --replay-reject-cut=N  maximum complexity of any coefficient while replaying

                         cuts

  --restrict-pivots      have a pivot cap for simplex at effort levels below

                         fullEffort [*]

  --revert-arith-models-on-unsat

                         revert the arithmetic model to a known safe model on

                         unsat if one is cached [*]

  --rr-turns=N           round robin turn

  --se-solve-int         attempt to use the approximate solve integer method on

                         standard effort [*]

  --simplex-check-period=N

                         the number of pivots to do in simplex before rechecking

                         for a conflict on all variables

  --soi-qe               use quick explain to minimize the sum of infeasibility

                         conflicts [*]

  --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)

  --use-approx           attempt to use an approximate solver [*]

  --use-fcsimplex        use focusing and converging simplex (FMCAD 2013

                         submission) [*]

  --use-soi              use sum of infeasibility simplex (FMCAD 2013

                         submission) [*]

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 [*]

  --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) [*]

  --arrays-prop=N        propagation effort for arrays: 0 is none, 1 is some, 2

                         is full

  --arrays-reduce-sharing

                         use model information to reduce size of care graph for

                         arrays [*]

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

From the Base module:

  --debug=TAG | -d TAG   debug something (e.g. -d arith), can repeat

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

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

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

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

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

  --stats-all            print unchanged (defaulted) statistics as well (EXPERTS

                         only) [*]

  --stats-every-query    in incremental mode, print stats after every

                         satisfiability or validity query [*]

  --stats-expert         print expert (non-public) statistics as well (EXPERTS

                         only) [*]

  --trace=TAG | -t TAG   trace something (e.g. -t pushpop), can repeat

  --verbosity=N          the verbosity level of cvc5

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 [*]

  --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 [*]

  --bv-extract-arith     enable rewrite pushing extract [i:0] over arithmetic

                         operations (can blow up) (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-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

                         [*]

  --bv-propagate         use bit-vector propagation in the bit-blaster [*]

  --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 (EXPERTS only)

  --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 [*]

  --dt-binary-split      do binary splits for datatype constructor types [*]

  --dt-blast-splits      when applicable, blast splitting lemmas for all

                         variables at once [*]

  --dt-cyclic            do cyclicity check for datatypes [*]

  --dt-force-assignment  force the datatypes solver to give specific values to

                         all datatypes terms before answering sat [*]

  --dt-infer-as-lemmas   always send lemmas out instead of making internal

                         inferences [*]

  --dt-nested-rec        allow nested recursion in datatype definitions [*]

  --dt-polite-optimize   turn on optimization for polite combination (EXPERTS

                         only) [*]

  --dt-rewrite-error-sel rewrite incorrectly applied selectors to arbitrary

                         ground term (EXPERTS only) [*]

  --dt-share-sel         internally use shared selectors across multiple

                         constructors [*]

  --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 [*]

  --sygus-sym-break      simple sygus symmetry breaking lemmas [*]

  --sygus-sym-break-agg  use aggressive checks for simple sygus symmetry

                         breaking lemmas [*]

  --sygus-sym-break-dynamic

                         dynamic sygus symmetry breaking lemmas [*]

  --sygus-sym-break-lazy lazily add symmetry breaking lemmas for terms [*]

  --sygus-sym-break-pbe  sygus symmetry breaking lemmas based on pbe conjectures

                         [*]

  --sygus-sym-break-rlv  add relevancy conditions to symmetry breaking lemmas

                         [*]

From the Decision Heuristics module:

  --decision=MODE | --decision-mode=MODE

                         choose decision mode, see --decision=help

  --decision-random-weight=N

                         assign random weights to nodes between 0 and N-1 (0:

                         disable) (EXPERTS only)

  --decision-threshold=N ignore all nodes greater than threshold in first

                         attempt to pick decision (EXPERTS only)

  --decision-use-weight  use the weight nodes (locally, by looking at children)

                         to direct recursive search (EXPERTS only) [*]

  --decision-weight-internal=HOW

                         compute weights of internal nodes using children: off,

                         max, sum, usr1 (EXPERTS only)

  --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:

  --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)

  --type-checking        type check expressions [*]

From the Floating-Point module:

  --fp-exp               Allow floating-point sorts of all sizes, rather than

                         only Float32 (8/24) or Float64 (11/53) (experimental)

                         [*]

  --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 [*]

  --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 [*]

  --early-exit           do not run destructors at exit; default on except in

                         debug builds (EXPERTS only) [*]

  --force-no-limit-cpu-while-dump

                         Force no CPU limit when dumping models and proofs [*]

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

  --print-unsat-cores-full

                         dump the full unsat core, including unlabeled

                         assertions [*]

  --segv-spin            spin on segfault/other crash waiting for gdb [*]

  --show-debug-tags      show all available tags for debugging

  --show-trace-tags      show all available tags for tracing

From the Parser module:

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

                         to change it (EXPERTS only)

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

  --mmap                 memory map file input [*]

  --semantic-checks      enable semantic checks, including type checks [*]

From the Printing module:

  --flatten-ho-chains    print (binary) application chains in a flattened way,

                         e.g. (a b c) rather than ((a b) c) [*]

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

  --print-inst-full      print instantiations for formulas that do not have

                         given identifiers [*]

From the Proof module:

  --proof-check=MODE     select proof checking mode

  --proof-format-mode=MODE

                         select language of proof output

  --proof-granularity=MODE

                         modes for proof granularity

  --proof-pedantic=N     assertion failure for any incorrect rule application or

                         untrusted lemma having pedantic level <=N with proof

  --proof-pp-merge       merge subproofs in final proof post-processor [*]

  --proof-print-conclusion

                         Print conclusion of proof steps when printing AST [*]

From the SAT Layer module:

  --minisat-dump-dimacs  instead of solving minisat dumps the asserted clauses

                         in Dimacs format [*]

  --minisat-elimination  use Minisat elimination [*]

  --random-freq=P | --random-frequency=P

                         sets the frequency of random decisions in the sat

                         solver (P=0.0 by default)

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

  --refine-conflicts     refine theory conflict clauses (default false) [*]

  --restart-int-base=N   sets the base restart interval for the sat solver (N=25

                         by default)

  --restart-int-inc=F    sets the restart interval increase factor for the sat

                         solver (F=3.0 by default)

From the Quantifiers module:

  --ag-miniscope-quant   perform aggressive miniscoping for quantifiers [*]

  --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 [*]

  --cegqi-bv             use word-level inversion approach for

                         counterexample-guided quantifier instantiation for

                         bit-vectors [*]

  --cegqi-bv-concat-inv  compute inverse for concat over equalities rather than

                         producing an invertibility condition [*]

  --cegqi-bv-ineq=MODE   choose mode for handling bit-vector inequalities with

                         counterexample-guided instantiation

  --cegqi-bv-interleave-value

                         interleave model value instantiation with word-level

                         inversion approach [*]

  --cegqi-bv-linear      linearize adder chains for variables [*]

  --cegqi-bv-rm-extract  replaces extract terms with variables for

                         counterexample-guided instantiation for bit-vectors [*]

  --cegqi-bv-solve-nl    try to solve non-linear bv literals using model value

                         projections [*]

  --cegqi-full           turns on full effort counterexample-based quantifier

                         instantiation, which may resort to model-value

                         instantiation [*]

  --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 [*]

  --cegqi-model          guide instantiations by model values for

                         counterexample-based quantifier instantiation [*]

  --cegqi-multi-inst     when applicable, do multi instantiations per quantifier

                         per round in counterexample-based quantifier

                         instantiation [*]

  --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 [*]

  --cegqi-repeat-lit     solve literals more than once in counterexample-based

                         quantifier instantiation [*]

  --cegqi-round-up-lia   round up integer lower bounds in substitutions for

                         counterexample-based quantifier instantiation [*]

  --cegqi-sat            answer sat when quantifiers are asserted with

                         counterexample-based quantifier instantiation [*]

  --cegqi-use-inf-int    use integer infinity for vts in counterexample-based

                         quantifier instantiation [*]

  --cegqi-use-inf-real   use real infinity for vts in counterexample-based

                         quantifier instantiation [*]

  --cond-var-split-agg-quant

                         aggressive split quantified formulas that lead to

                         variable eliminations [*]

  --cond-var-split-quant split quantified formulas that lead to variable

                         eliminations [*]

  --conjecture-filter-active-terms

                         filter based on active terms [*]

  --conjecture-filter-canonical

                         filter based on canonicity [*]

  --conjecture-filter-model

                         filter based on model [*]

  --conjecture-gen       generate candidate conjectures for inductive proofs [*]

  --conjecture-gen-gt-enum=N

                         number of ground terms to generate for model filtering

  --conjecture-gen-max-depth=N

                         maximum depth of terms to consider for conjectures

  --conjecture-gen-per-round=N

                         number of conjectures to generate per instantiation

                         round

  --conjecture-gen-uee-intro

                         more aggressive merging for universal equality engine,

                         introduces terms [*]

  --conjecture-no-filter do not filter conjectures [*]

  --dt-stc-ind           apply strengthening for existential quantification over

                         datatypes based on structural induction [*]

  --dt-var-exp-quant     expand datatype variables bound to one constructor in

                         quantifiers [*]

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

  --elim-taut-quant      eliminate tautological disjuncts of quantified formulas

                         [*]

  --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-int        finite model finding on bounded integer quantification

                         [*]

  --fmf-bound-lazy       enforce bounds for bounded quantification lazily via

                         use of proxy variables [*]

  --fmf-fmc-simple       simple models in full model check for finite model

                         finding [*]

  --fmf-fresh-dc         use fresh distinguished representative when applying

                         Inst-Gen techniques [*]

  --fmf-fun              find models for recursively defined functions, assumes

                         functions are admissible [*]

  --fmf-fun-rlv          find models for recursively defined functions, assumes

                         functions are admissible, allows empty type when

                         function is irrelevant [*]

  --fmf-inst-engine      use instantiation engine in conjunction with finite

                         model finding [*]

  --fmf-type-completion-thresh=N

                         the maximum cardinality of an interpreted type for

                         which exhaustive enumeration in finite model finding is

                         attempted

  --fs-interleave        interleave enumerative instantiation with other

                         techniques [*]

  --fs-stratify          stratify effort levels in enumerative instantiation,

                         which favors speed over fairness [*]

  --fs-sum               enumerating tuples of quantifiers by increasing the sum

                         of indices, rather than the maximum [*]

  --full-saturate-quant  enumerative instantiation: instantiate with ground

                         terms from relevant domain, then arbitrary ground terms

                         before answering unknown [*]

  --full-saturate-quant-limit=N

                         maximum number of rounds of enumerative instantiation

                         to apply (-1 means no limit)

  --full-saturate-quant-rd

                         whether to use relevant domain first for enumerative

                         instantiation strategy [*]

  --global-negate        do global negation of input formula [*]

  --ho-elim              eagerly eliminate higher-order constraints [*]

  --ho-elim-store-ax     use store axiom during ho-elim [*]

  --ho-matching          do higher-order matching algorithm for triggers with

                         variable operators [*]

  --ho-matching-var-priority

                         give priority to variable arguments over constant

                         arguments [*]

  --ho-merge-term-db     merge term indices modulo equality [*]

  --increment-triggers   generate additional triggers as needed during search

                         [*]

  --inst-level-input-only

                         only input terms are assigned instantiation level zero

                         [*]

  --inst-max-level=N     maximum inst level of terms used to instantiate

                         quantified formulas with (-1 == no limit, default)

  --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

  --inst-when-strict-interleave

                         ensure theory combination and standard quantifier

                         effort strategies take turns [*]

  --inst-when-tc-first   allow theory combination to happen once initially,

                         before quantifier strategies are run [*]

  --int-wf-ind           apply strengthening for integers based on well-founded

                         induction [*]

  --ite-dtt-split-quant  split ites with dt testers as conditions [*]

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

  --literal-matching=MODE

                         choose literal matching mode

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

  --macros-quant-mode=MODE

                         mode for quantifiers macro expansion

  --mbqi=MODE            choose mode for model-based quantifier instantiation

  --mbqi-interleave      interleave model-based quantifier instantiation with

                         other techniques [*]

  --mbqi-one-inst-per-round

                         only add one instantiation per quantifier per round for

                         mbqi [*]

  --miniscope-quant      miniscope quantifiers [*]

  --miniscope-quant-fv   miniscope quantifiers for ground subformulas [*]

  --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 [*]

  --partial-triggers     use triggers that do not contain all free variables [*]

  --pool-inst            pool-based instantiation: instantiate with ground terms

                         occurring in user-specified pools [*]

  --pre-skolem-quant     apply skolemization eagerly to bodies of quantified

                         formulas [*]

  --pre-skolem-quant-agg apply skolemization to quantified formulas aggressively

                         [*]

  --pre-skolem-quant-nested

                         apply skolemization to nested quantified formulas [*]

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

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

  --purify-triggers      purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto

                         y-1 [*]

  --qcf-all-conflict     add all available conflicting instances during

                         conflict-based instantiation [*]

  --qcf-eager-check-rd   optimization, eagerly check relevant domain of matched

                         position [*]

  --qcf-eager-test       optimization, test qcf instances eagerly [*]

  --qcf-nested-conflict  consider conflicts for nested quantifiers [*]

  --qcf-skip-rd          optimization, skip instances based on possibly

                         irrelevant portions of quantified formulas [*]

  --qcf-tconstraint      enable entailment checks for t-constraints in qcf

                         algorithm [*]

  --qcf-vo-exp           qcf experimental variable ordering [*]

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

  --quant-cf             enable conflict find mechanism for quantifiers [*]

  --quant-cf-mode=MODE   what effort to apply conflict find mechanism

  --quant-cf-when=MODE   when to invoke conflict find mechanism for quantifiers

  --quant-dsplit-mode=MODE

                         mode for dynamic quantifiers splitting

  --quant-fun-wd         assume that function defined by quantifiers are well

                         defined [*]

  --quant-ind            use all available techniques for inductive reasoning

                         [*]

  --quant-rep-mode=MODE  selection mode for representatives in quantifiers

                         engine

  --quant-split          apply splitting to quantified formulas based on

                         variable disjoint disjuncts [*]

  --register-quant-body-terms

                         consider ground terms within bodies of quantified

                         formulas for matching [*]

  --relational-triggers  choose relational triggers such as x = f(y), x >= f(y)

                         [*]

  --relevant-triggers    prefer triggers that are more relevant based on SInE

                         style analysis [*]

  --sygus                use sygus solver (default is true for sygus inputs) [*]

  --sygus-active-gen=MODE

                         mode for actively-generated sygus enumerators

  --sygus-active-gen-cfactor=N

                         the branching factor for the number of interpreted

                         constants to consider for each size when using

                         --sygus-active-gen=enum

  --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 [*]

  --sygus-auto-unfold    enable approach which automatically unfolds transition

                         systems for directly solving invariant synthesis

                         problems [*]

  --sygus-bool-ite-return-const

                         Only use Boolean constants for return values in

                         unification-based function synthesis [*]

  --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

                         [*]

  --sygus-eval-opt       use optimized approach for evaluation in sygus [*]

  --sygus-eval-unfold    do unfolding of sygus evaluation functions [*]

  --sygus-eval-unfold-bool

                         do unfolding of Boolean evaluation functions that

                         appear in refinement lemmas [*]

  --sygus-expr-miner-check-timeout=N

                         timeout (in milliseconds) for satisfiability checks in

                         expression miners

  --sygus-ext-rew        use extended rewriter for sygus [*]

  --sygus-filter-sol=MODE

                         mode for filtering sygus solutions

  --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-norm   statically normalize sygus grammars based on flattening

                         (linearization) [*]

  --sygus-inference      attempt to preprocess arbitrary inputs to sygus

                         conjectures [*]

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

  --sygus-inst-mode=MODE select instantiation lemma mode

  --sygus-inst-scope=MODE

                         select scope of ground terms

  --sygus-inst-term-sel=MODE

                         granularity for ground terms

  --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 [*]

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

  --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 [*]

  --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)

  --sygus-qe-preproc     use quantifier elimination as a preprocessing step for

                         sygus [*]

  --sygus-query-gen=MODE mode for generating interesting satisfiability queries

                         using SyGuS, for internal fuzzing

  --sygus-query-gen-check

                         use interesting satisfiability queries to check

                         soundness of cvc5 [*]

  --sygus-query-gen-dump-files=MODE

                         mode for dumping external files corresponding to

                         interesting satisfiability queries with sygus-query-gen

  --sygus-query-gen-thresh=N

                         number of points that we allow to be equal for

                         enumerating satisfiable queries with sygus-query-gen

  --sygus-rec-fun        enable efficient support for recursive functions in

                         sygus grammars [*]

  --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)

  --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

  --sygus-rr             use sygus to enumerate and verify correctness of

                         rewrite rules [*]

  --sygus-rr-synth       use sygus to enumerate candidate rewrite rules [*]

  --sygus-rr-synth-accel add dynamic symmetry breaking clauses based on

                         candidate rewrites [*]

  --sygus-rr-synth-check use satisfiability check to verify correctness of

                         candidate rewrites [*]

  --sygus-rr-synth-filter-cong

                         filter candidate rewrites based on congruence [*]

  --sygus-rr-synth-filter-match

                         filter candidate rewrites based on matching [*]

  --sygus-rr-synth-filter-nl

                         filter non-linear candidate rewrites [*]

  --sygus-rr-synth-filter-order

                         filter candidate rewrites based on variable ordering

                         [*]

  --sygus-rr-synth-input synthesize rewrite rules based on the input formula [*]

  --sygus-rr-synth-input-nvars=N

                         the maximum number of variables per type that appear in

                         rewrites from sygus-rr-synth-input

  --sygus-rr-synth-input-use-bool

                         synthesize Boolean rewrite rules based on the input

                         formula [*]

  --sygus-rr-synth-rec   synthesize rewrite rules over all sygus grammar types

                         recursively [*]

  --sygus-rr-verify      use sygus to verify the correctness of rewrite rules

                         via sampling [*]

  --sygus-rr-verify-abort

                         abort when sygus-rr-verify finds an instance of

                         unsoundness [*]

  --sygus-sample-fp-uniform

                         sample floating-point values uniformly instead of in a

                         biased fashion [*]

  --sygus-sample-grammar when applicable, use grammar for choosing sample points

                         [*]

  --sygus-samples=N      number of points to consider when doing sygus rewriter

                         sample testing

  --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)

  --sygus-stream         enumerate a stream of solutions instead of terminating

                         after the first one [*]

  --sygus-templ-embed-grammar

                         embed sygus templates into grammars [*]

  --sygus-unif-cond-independent-no-repeat-sol

                         Do not try repeated solutions when using independent

                         synthesis of conditions in unification-based function

                         synthesis [*]

  --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) [*]

  --sygus-verify-inst-max-rounds=N

                         maximum number of instantiation rounds for sygus

                         verification calls (-1 == no limit, default is 3)

  --term-db-cd           register terms in term database based on the SAT

                         context [*]

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

  --trigger-active-sel=MODE

                         selection mode to activate triggers

  --trigger-sel=MODE     selection mode for triggers

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

                         quantifier instantiation

  --var-elim-quant       enable simple variable elimination for quantified

                         formulas [*]

  --var-ineq-elim-quant  enable variable elimination based on infinite

                         projection of unbound arithmetic variables [*]

From the Separation Logic Theory module:

  --sep-check-neg        check negated spatial assertions [*]

  --sep-child-refine     child-specific refinements of negated star, positive

                         wand [*]

  --sep-deq-c            assume cardinality elements are distinct [*]

  --sep-min-refine       only add refinement lemmas for minimal (innermost)

                         assertions [*]

  --sep-pre-skolem-emp   eliminate emp constraint at preprocess time [*]

From the Sets Theory module:

  --sets-ext             enable extended symbols such as complement and universe

                         in theory of sets [*]

  --sets-infer-as-lemmas send inferences as lemmas [*]

  --sets-proxy-lemmas    introduce proxy variables eagerly to shorten lemmas [*]

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 [*]

  --ackermann            eliminate functions by ackermannization [*]

  --block-models=MODE    mode for producing several models

  --check-abducts        checks whether produced solutions to get-abduct are

                         correct [*]

  --check-interpols      checks whether produced solutions to get-interpol are

                         correct [*]

  --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 [*]

  --difficulty-mode=MODE choose output mode for get-difficulty, see

                         --difficulty-mode=help

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

  --expand-definitions   always expand symbol definitions in output [*]

  --ext-rew-prep         use extended rewriter as a preprocessing pass [*]

  --ext-rew-prep-agg     use aggressive extended rewriter as a preprocessing

                         pass [*]

  --foreign-theory-rewrite

                         Cross-theory rewrites [*]

  --ite-simp             turn on ite simplification (Kim (and Somenzi) et al.,

                         SAT 2009) [*]

  --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 [*]

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

  --model-u-print=MODE | --model-uninterp-print=MODE

                         determines how to print uninterpreted elements in

                         models

  --model-witness-value  in models, use a witness constant for choice functions

                         [*]

  --on-repeat-ite-simp   do the ite simplification pass again if repeating

                         simplification [*]

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

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

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

  --produce-unsat-assumptions

                         turn on unsat assumptions generation [*]

  --produce-unsat-cores  turn on unsat core generation. Unless otherwise

                         specified, cores will be produced using SAT soving

                         under assumptions and preprocessing proofs. [*]

  --repeat-simp          make multiple passes with nonclausal simplifier [*]

  --simp-ite-compress    enables compressing ites after ite simplification [*]

  --simp-ite-hunt-zombies=N

                         post ite compression enables zombie removal while the

                         number of nodes is above this threshold

  --simp-with-care       enables simplifyWithCare in ite simplificiation [*]

  --simplification=MODE | --simplification-mode=MODE

                         choose simplification mode, see --simplification=help

  --sort-inference       calculate sort inference of input problem, convert the

                         input based on monotonic sorts [*]

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

  --sygus-out=MODE       output mode for sygus

  --unconstrained-simp   turn on unconstrained simplification (see

                         Bruttomesso/Brummayer PhD thesis). Fully supported only

                         in (subsets of) the logic QF_ABV. [*]

  --unsat-cores-mode=MODE

                         choose unsat core mode, see --unsat-cores-mode=help

From the Strings Theory module:

  --re-elim              elimination techniques for regular expressions [*]

  --re-elim-agg          aggressive elimination techniques for regular

                         expressions [*]

  --re-inter-mode=MODE   determines which regular expressions intersections to

                         compute (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

  --strings-check-entail-len

                         check entailment between length terms to reduce

                         splitting [*]

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

  --strings-eager        strings eager check [*]

  --strings-eager-eval   perform eager context-dependent evaluation for

                         applications of string kinds [*]

  --strings-eager-len    strings eager length lemmas [*]

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

  --strings-ff           do flat form inferences [*]

  --strings-fmf          the finite model finding used by the theory of strings

                         [*]

  --strings-guess-model  use model guessing to avoid string extended function

                         reductions [*]

  --strings-infer-as-lemmas

                         always send lemmas out instead of making internal

                         inferences [*]

  --strings-infer-sym    strings split on empty string [*]

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

  --strings-len-norm     strings length normalization lemma [*]

  --strings-min-prefix-explain

                         minimize explanations for prefix of normal forms in

                         strings [*]

  --strings-process-loop-mode=MODE

                         determines how to process looping string equations

                         (EXPERTS only)

  --strings-rexplain-lemmas

                         regression explanations for string lemmas [*]

  --strings-unified-vspt use a single skolem for the variable splitting rule [*]

From the Theory Layer module:

  --assign-function-values

                         assign values for uninterpreted functions in models [*]

  --condense-function-values

                         condense values for functions in models rather than

                         explicitly representing them [*]

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

                         (EXPERTS only)

  --relevance-filter     enable analysis of relevance of asserted literals with

                         respect to the input formula [*]

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

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

From the Uninterpreted Functions Theory module:

  --symmetry-breaker | --uf-symmetry-breaker

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

  --uf-ho-ext            apply extensionality on function symbols [*]

  --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 [*]

)FOOBAR";

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

    sense of the option.\n\

";

// clang-format on

{

  os << msg << "\n"

     << commonOptionsDescription << "\n\n"

{

  os << msg << "\n"

/**

 * This is a table of long options.  By policy, each short option

 * should have an equivalent long option (but the reverse isn't the

 * case), so this table should thus contain all command-line options.

 *

 * Each option in this array has four elements:

 *

 * 1. the long option string

 * 2. argument behavior for the option:

 *    no_argument - no argument permitted

 *    required_argument - an argument is expected

 *    optional_argument - an argument is permitted but not required

 * 3. this is a pointer to an int which is set to the 4th entry of the

 *    array if the option is present; or nullptr, in which case

 *    getopt_long() returns the 4th entry

 * 4. the return value for getopt_long() when this long option (or the

 *    value to set the 3rd entry to; see #3)

 */

static struct option cmdlineOptions[] = {

// clang-format off

  { "approx-branch-depth", required_argument, nullptr, 256 },

  { "arith-brab", no_argument, nullptr, 257 },

  { "no-arith-brab", no_argument, nullptr, 258 },

  { "arith-cong-man", no_argument, nullptr, 259 },

  { "no-arith-cong-man", no_argument, nullptr, 260 },

  { "arith-eq-solver", no_argument, nullptr, 261 },

  { "no-arith-eq-solver", no_argument, nullptr, 262 },

  { "arith-no-partial-fun", no_argument, nullptr, 263 },

  { "no-arith-no-partial-fun", no_argument, nullptr, 264 },

  { "arith-prop", required_argument, nullptr, 265 },

  { "arith-prop-clauses", required_argument, nullptr, 266 },

  { "arith-rewrite-equalities", no_argument, nullptr, 267 },

  { "no-arith-rewrite-equalities", no_argument, nullptr, 268 },

  { "collect-pivot-stats", no_argument, nullptr, 269 },

  { "no-collect-pivot-stats", no_argument, nullptr, 270 },

  { "cut-all-bounded", no_argument, nullptr, 271 },

  { "no-cut-all-bounded", no_argument, nullptr, 272 },

  { "dio-decomps", no_argument, nullptr, 273 },

  { "no-dio-decomps", no_argument, nullptr, 274 },

  { "dio-solver", no_argument, nullptr, 275 },

  { "no-dio-solver", no_argument, nullptr, 276 },

  { "dio-turns", required_argument, nullptr, 277 },

  { "error-selection-rule", required_argument, nullptr, 278 },

  { "fc-penalties", no_argument, nullptr, 279 },

  { "no-fc-penalties", no_argument, nullptr, 280 },

  { "heuristic-pivots", required_argument, nullptr, 281 },

  { "lemmas-on-replay-failure", no_argument, nullptr, 282 },

  { "no-lemmas-on-replay-failure", no_argument, nullptr, 283 },

  { "maxCutsInContext", required_argument, nullptr, 284 },

  { "miplib-trick", no_argument, nullptr, 285 },

  { "no-miplib-trick", no_argument, nullptr, 286 },

  { "miplib-trick-subs", required_argument, nullptr, 287 },

  { "new-prop", no_argument, nullptr, 288 },

  { "no-new-prop", no_argument, nullptr, 289 },

  { "nl-cad", no_argument, nullptr, 290 },

  { "no-nl-cad", no_argument, nullptr, 291 },

  { "nl-cad-initial", no_argument, nullptr, 292 },

  { "no-nl-cad-initial", no_argument, nullptr, 293 },

  { "nl-cad-lift", required_argument, nullptr, 294 },

  { "nl-cad-proj", required_argument, nullptr, 295 },

  { "nl-ext", required_argument, nullptr, 296 },

  { "nl-ext-ent-conf", no_argument, nullptr, 297 },

  { "no-nl-ext-ent-conf", no_argument, nullptr, 298 },

  { "nl-ext-factor", no_argument, nullptr, 299 },

  { "no-nl-ext-factor", no_argument, nullptr, 300 },

  { "nl-ext-inc-prec", no_argument, nullptr, 301 },

  { "no-nl-ext-inc-prec", no_argument, nullptr, 302 },

  { "nl-ext-purify", no_argument, nullptr, 303 },

  { "no-nl-ext-purify", no_argument, nullptr, 304 },

  { "nl-ext-rbound", no_argument, nullptr, 305 },

  { "no-nl-ext-rbound", no_argument, nullptr, 306 },

  { "nl-ext-rewrite", no_argument, nullptr, 307 },

  { "no-nl-ext-rewrite", no_argument, nullptr, 308 },

  { "nl-ext-split-zero", no_argument, nullptr, 309 },

  { "no-nl-ext-split-zero", no_argument, nullptr, 310 },

  { "nl-ext-tf-taylor-deg", required_argument, nullptr, 311 },

  { "nl-ext-tf-tplanes", no_argument, nullptr, 312 },

  { "no-nl-ext-tf-tplanes", no_argument, nullptr, 313 },

  { "nl-ext-tplanes", no_argument, nullptr, 314 },

  { "no-nl-ext-tplanes", no_argument, nullptr, 315 },

  { "nl-ext-tplanes-interleave", no_argument, nullptr, 316 },

  { "no-nl-ext-tplanes-interleave", no_argument, nullptr, 317 },

  { "nl-icp", no_argument, nullptr, 318 },

  { "no-nl-icp", no_argument, nullptr, 319 },

  { "nl-rlv", required_argument, nullptr, 320 },

  { "nl-rlv-assert-bounds", no_argument, nullptr, 321 },

  { "no-nl-rlv-assert-bounds", no_argument, nullptr, 322 },

  { "pb-rewrites", no_argument, nullptr, 323 },

  { "no-pb-rewrites", no_argument, nullptr, 324 },

  { "pivot-threshold", required_argument, nullptr, 325 },

  { "pp-assert-max-sub-size", required_argument, nullptr, 326 },

  { "prop-row-length", required_argument, nullptr, 327 },

  { "replay-early-close-depth", required_argument, nullptr, 328 },

  { "replay-lemma-reject-cut", required_argument, nullptr, 329 },

  { "replay-num-err-penalty", required_argument, nullptr, 330 },

  { "replay-reject-cut", required_argument, nullptr, 331 },

  { "restrict-pivots", no_argument, nullptr, 332 },

  { "no-restrict-pivots", no_argument, nullptr, 333 },

  { "revert-arith-models-on-unsat", no_argument, nullptr, 334 },

  { "no-revert-arith-models-on-unsat", no_argument, nullptr, 335 },

  { "rr-turns", required_argument, nullptr, 336 },

  { "se-solve-int", no_argument, nullptr, 337 },

  { "no-se-solve-int", no_argument, nullptr, 338 },

  { "simplex-check-period", required_argument, nullptr, 339 },

  { "soi-qe", no_argument, nullptr, 340 },

  { "no-soi-qe", no_argument, nullptr, 341 },

  { "standard-effort-variable-order-pivots", required_argument, nullptr, 342 },

  { "unate-lemmas", required_argument, nullptr, 343 },

  { "use-approx", no_argument, nullptr, 344 },

  { "no-use-approx", no_argument, nullptr, 345 },

  { "use-fcsimplex", no_argument, nullptr, 346 },

  { "no-use-fcsimplex", no_argument, nullptr, 347 },

  { "use-soi", no_argument, nullptr, 348 },

  { "no-use-soi", no_argument, nullptr, 349 },

  { "arrays-eager-index", no_argument, nullptr, 350 },

  { "no-arrays-eager-index", no_argument, nullptr, 351 },

  { "arrays-eager-lemmas", no_argument, nullptr, 352 },

  { "no-arrays-eager-lemmas", no_argument, nullptr, 353 },

  { "arrays-exp", no_argument, nullptr, 354 },

  { "no-arrays-exp", no_argument, nullptr, 355 },

  { "arrays-optimize-linear", no_argument, nullptr, 356 },

  { "no-arrays-optimize-linear", no_argument, nullptr, 357 },

  { "arrays-prop", required_argument, nullptr, 358 },

  { "arrays-reduce-sharing", no_argument, nullptr, 359 },

  { "no-arrays-reduce-sharing", no_argument, nullptr, 360 },

  { "arrays-weak-equiv", no_argument, nullptr, 361 },

  { "no-arrays-weak-equiv", no_argument, nullptr, 362 },

  { "debug", required_argument, nullptr, 363 },

  { "err", required_argument, nullptr, 364 },

  { "diagnostic-output-channel", required_argument, nullptr, 365 },

  { "in", required_argument, nullptr, 366 },

  { "incremental", no_argument, nullptr, 367 },

  { "no-incremental", no_argument, nullptr, 368 },

  { "lang", required_argument, nullptr, 369 },

  { "input-language", required_argument, nullptr, 370 },

  { "out", required_argument, nullptr, 371 },

  { "regular-output-channel", required_argument, nullptr, 372 },

  { "output", required_argument, nullptr, 373 },

  { "output-lang", required_argument, nullptr, 374 },

  { "output-language", required_argument, nullptr, 375 },

  { "parse-only", no_argument, nullptr, 376 },

  { "no-parse-only", no_argument, nullptr, 377 },

  { "preprocess-only", no_argument, nullptr, 378 },

  { "no-preprocess-only", no_argument, nullptr, 379 },

  { "print-success", no_argument, nullptr, 380 },

  { "no-print-success", no_argument, nullptr, 381 },

  { "quiet", no_argument, nullptr, 382 },

  { "rlimit", required_argument, nullptr, 383 },

  { "rlimit-per", required_argument, nullptr, 384 },

  { "reproducible-resource-limit", required_argument, nullptr, 385 },

  { "rweight", required_argument, nullptr, 386 },

  { "stats", no_argument, nullptr, 387 },

  { "no-stats", no_argument, nullptr, 388 },

  { "stats-all", no_argument, nullptr, 389 },

  { "no-stats-all", no_argument, nullptr, 390 },

  { "stats-every-query", no_argument, nullptr, 391 },

  { "no-stats-every-query", no_argument, nullptr, 392 },

  { "stats-expert", no_argument, nullptr, 393 },

  { "no-stats-expert", no_argument, nullptr, 394 },

  { "tlimit", required_argument, nullptr, 395 },

  { "tlimit-per", required_argument, nullptr, 396 },

  { "trace", required_argument, nullptr, 397 },

  { "verbose", no_argument, nullptr, 398 },

  { "verbosity", required_argument, nullptr, 399 },

  { "bitblast", required_argument, nullptr, 400 },

  { "bitwise-eq", no_argument, nullptr, 401 },

  { "no-bitwise-eq", no_argument, nullptr, 402 },

  { "bool-to-bv", required_argument, nullptr, 403 },

  { "bv-assert-input", no_argument, nullptr, 404 },

  { "no-bv-assert-input", no_argument, nullptr, 405 },

  { "bv-extract-arith", no_argument, nullptr, 406 },

  { "no-bv-extract-arith", no_argument, nullptr, 407 },

  { "bv-gauss-elim", no_argument, nullptr, 408 },

  { "no-bv-gauss-elim", no_argument, nullptr, 409 },

  { "bv-intro-pow2", no_argument, nullptr, 410 },

  { "no-bv-intro-pow2", no_argument, nullptr, 411 },

  { "bv-print-consts-as-indexed-symbols", no_argument, nullptr, 412 },

  { "no-bv-print-consts-as-indexed-symbols", no_argument, nullptr, 413 },

  { "bv-propagate", no_argument, nullptr, 414 },

  { "no-bv-propagate", no_argument, nullptr, 415 },

  { "bv-rw-extend-eq", no_argument, nullptr, 416 },

  { "no-bv-rw-extend-eq", no_argument, nullptr, 417 },

  { "bv-sat-solver", required_argument, nullptr, 418 },

  { "bv-solver", required_argument, nullptr, 419 },

  { "bv-to-bool", no_argument, nullptr, 420 },

  { "no-bv-to-bool", no_argument, nullptr, 421 },

  { "cdt-bisimilar", no_argument, nullptr, 422 },

  { "no-cdt-bisimilar", no_argument, nullptr, 423 },

  { "dt-binary-split", no_argument, nullptr, 424 },