Provided by: cvc4_1.6-2build1_amd64 bug

NAME

       cvc4, pcvc4 - an automated theorem prover

SYNOPSIS

       cvc4 [ options ] [ file ]

       pcvc4 [ options ] [ file ]

DESCRIPTION

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

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

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

COMMON OPTIONS

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

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

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

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

       --stats
              give statistics on exit [*]

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

       --copyright
              show CVC4 copyright information

       --help | -h
              full command line reference

       --seed | -s
              seed for random number generator

       --show-config
              show CVC4 static configuration

       --version | -V
              identify this CVC4 binary

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

       --cpu-time
              measures CPU time if set to true and wall time if false (default false) [*]

       --dump-to=FILE
              all dumping goes to FILE (instead of stdout)

       --dump=MODE
              dump preprocessed assertions, etc., see --dump=help

       --hard-limit
              the resource limit is hard potentially leaving the smtEngine  in  an  unsafe  state
              (should be destroyed and rebuild after resourcing out) [*]

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

       --produce-assertions
              keep an assertions list (enables get-assertions command) [*]

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

       --rlimit-per=N
              enable resource limiting per query

       --rlimit=N
              enable resource limiting (currently, roughly the number of SAT conflicts)

       --tlimit-per=MS
              enable time limiting per query (give milliseconds)

       --tlimit=MS
              enable time limiting (give milliseconds)

ARITHMETIC THEORY OPTIONS

       --approx-branch-depth
              maximum branch depth the approximate solver is allowed to take

       --arith-no-partial-fun
              do not use partial function semantics for arithmetic (not SMT LIB compliant) [*]

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

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

       --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-repeat
              handle dio solver constraints in mass or one at a time [*]

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

       --dio-turns
              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
              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-ext
              extended 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 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 [*]

       --nl-ext-rewrite
              do 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 [*]

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

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

       --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
              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
              multiples of the depths to try to close the approx log eagerly

       --replay-failure-penalty
              number of solve integer attempts to skips after a numeric failure

       --replay-lemma-reject-cut
              maximum complexity of any coefficient while outputting replaying cut lemmas

       --replay-num-err-penalty
              number of solve integer attempts to skips after a numeric failure

       --replay-reject-cut
              maximum complexity of any coefficient while replaying cuts

       --replay-soi-major-threshold
              threshold for a major tolerance failure by the approximate solver

       --replay-soi-major-threshold-pen
              threshold for a major tolerance failure by the approximate solver

       --replay-soi-minor-threshold
              threshold for a minor tolerance failure by the approximate solver

       --replay-soi-minor-threshold-pen
              threshold for a minor tolerance failure by the approximate solver

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

       --rewrite-divk
              rewrite division and mod when by a constant into linear terms [*]

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

       --snorm-infer-eq
              infer equalities based on Shostak normalization [*]

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

ARRAYS THEORY OPTIONS

       --arrays-config
              set different array option configurations - for developers only

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

       --arrays-eager-lemmas
              turn on eager lemma generation for arrays [*]

       --arrays-lazy-rintro1
              turn on optimization to only perform RIntro1  rule  lazily  (see  Jovanovic/Barrett
              2012: Being Careful with Theory Combination) [*]

       --arrays-model-based
              turn on model-based array solver [*]

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

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

BASE OPTIONS

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

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

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

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

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

       --stats-hide-zeros
              hide statistics which are zero [*]

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

       --smtlib-strict
              SMT-LIBv2 compliance mode (implies other options)

BITVECTOR THEORY OPTIONS

       --bitblast-aig
              bitblast by first converting to AIG (implies --bitblast=eager) [*]

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

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

       --bv-abstraction
              mcm benchmark abstraction (EXPERTS only) [*]

       --bv-aig-simp=COMMAND
              abc  command  to  run  AIG  simplifications  (implies  --bitblast-aig,  default  is
              "balance;drw") (EXPERTS only)

       --bv-alg-extf
              algebraic inferences for extended functions [*]

       --bv-algebraic-budget
              the  budget  allowed  for  the algebraic solver in number of SAT conflicts (EXPERTS
              only)

       --bv-algebraic-solver
              turn on the algebraic solver for the bit-vector theory  (only  if  --bitblast=lazy)
              [*]

       --bv-div-zero-const
              always return -1 on division by zero [*]

       --bv-eager-explanations
              compute bit-blasting propagation explanations eagerly (EXPERTS only) [*]

       --bv-eq-slicer=MODE
              turn   on   the  slicing  equality  solver  for  the  bit-vector  theory  (only  if
              --bitblast=lazy)

       --bv-eq-solver
              use the equality engine for the bit-vector theory (only if --bitblast=lazy) [*]

       --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-inequality-solver
              turn  on  the inequality solver for the bit-vector theory (only if --bitblast=lazy)
              [*]

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

       --bv-lazy-reduce-extf
              reduce extended functions like bv2nat and int2bv  at  last  call  instead  of  full
              effort [*]

       --bv-lazy-rewrite-extf
              lazily rewrite extended functions like bv2nat and int2bv [*]

       --bv-num-func=NUM
              number of function symbols in conflicts that are generalized (EXPERTS only)

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

       --bv-quick-xplain
              minimize bv conflicts using the QuickXplain algorithm (EXPERTS only) [*]

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

       --bv-skolemize
              skolemize  arguments for bv abstraction (only does something if --bv-abstraction is
              on) (EXPERTS only) [*]

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

DATATYPES THEORY OPTIONS

       --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-ref-sk-intro
              introduce reference skolems for shorter explanations [*]

       --dt-rewrite-error-sel
              rewrite incorrectly applied selectors to arbitrary ground term (EXPERTS only) [*]

       --dt-share-sel
              internally use shared selectors across multiple constructors [*]

       --dt-use-testers
              do not preprocess away tester predicates [*]

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

       --sygus-eval-builtin
              use builtin kind for evaluation functions in sygus [*]

       --sygus-fair-max
              use max instead of sum for multi-function sygus conjectures [*]

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

       --sygus-opt1
              sygus experimental option [*]

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

       --sygus-sym-break-dynamic
              dynamic sygus sym break lemmas [*]

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

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

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

DECISION HEURISTICS OPTIONS

       --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
              computer weights of internal nodes using children: off,  max,  sum,  usr1  (meaning
              evolving) (EXPERTS only)

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

EXPRESSION PACKAGE OPTIONS

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

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

       --eager-type-checking
              type check expressions immediately on creation (debug builds only) [*]

       --print-expr-types
              print types with variables when printing exprs [*]

       --type-checking
              never type check expressions

IDL OPTIONS

       --idl-rewrite-equalities
              enable  rewriting  equalities  into  two  inequalities  in  IDL  solver (default is
              disabled) [*]

DRIVER OPTIONS

       --continued-execution
              continue executing commands, even on error [*]

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

       --fallback-sequential
              Switch  to  sequential mode (instead of printing an error) if it can't be solved in
              portfolio mode [*]

       --filter-lemma-length=N
              don't share (among portfolio threads) lemmas strictly longer than N

       --incremental-parallel
              Use parallel solver even in incremental mode (may print 'unknown's at times) [*]

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

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

       --tear-down-incremental=N
              implement PUSH/POP/multi-query by  destroying  and  recreating  SmtEngine  every  N
              queries (EXPERTS only)

       --thread-stack=N
              stack size for worker threads in MB (0 means use Boost/thread lib default)

       --threadN=string
              configures portfolio thread N (0..#threads-1)

       --threads=N
              Total number of threads for portfolio

       --wait-to-join
              wait for other threads to join before quitting (EXPERTS only) [*]

PARSER OPTIONS

       --mmap memory map file input [*]

PRINTING OPTIONS

       --inst-format=MODE
              print format mode for instantiations, see --inst-format=help

       --model-format=MODE
              print format mode for models, see --model-format=help

PROOF OPTIONS

       --aggressive-core-min
              turns on aggressive unsat core minimization (experimental) [*]

       --allow-empty-dependencies
              if  unable  to  track  the dependencies of a rewritten/preprocessed assertion, fail
              silently [*]

       --fewer-preprocessing-holes
              try to eliminate preprocessing holes in proofs [*]

       --lfsc-letification
              turns on global letification in LFSC proofs [*]

SAT LAYER OPTIONS

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

       --minisat-elimination
              use Minisat elimination [*]

       --random-freq=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)

QUANTIFIERS OPTIONS

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

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

       --cbqi-all
              apply counterexample-based instantiation to all quantified formulas [*]

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

       --cbqi-bv-concat-inv
              compute  inverse  for concat over equalities rather than producing an invertibility
              condition [*]

       --cbqi-bv-ineq=MODE
              choose  mode  for  handling  bit-vector  inequalities  with   counterexample-guided
              instantiation

       --cbqi-bv-interleave-value
              interleave model value instantiation with word-level inversion approach [*]

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

       --cbqi-bv-rm-extract
              replaces  extract  terms with variables for counterexample-guided instantiation for
              bit-vectors [*]

       --cbqi-bv-solve-nl
              try to solve non-linear bv literals using model value projections [*]

       --cbqi-full
              turns on full  effort  counterexample-based  quantifier  instantiation,  which  may
              resort to model-value instantiation [*]

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

       --cbqi-lit-dep
              dependency lemmas for quantifier  alternation  in  counterexample-based  quantifier
              instantiation [*]

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

       --cbqi-min-bounds
              use minimally constrained lower/upper  bound  for  counterexample-based  quantifier
              instantiation [*]

       --cbqi-model
              guide   instantiations   by   model   values  for  counterexample-based  quantifier
              instantiation [*]

       --cbqi-multi-inst
              when  applicable,  do  multi   instantiations   per   quantifier   per   round   in
              counterexample-based quantifier instantiation [*]

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

       --cbqi-nopt
              non-optimal bounds for counterexample-based quantifier instantiation [*]

       --cbqi-prereg-inst
              preregister ground instantiations in counterexample-based quantifier  instantiation
              [*]

       --cbqi-recurse
              turns on recursive counterexample-based quantifier instantiation [*]

       --cbqi-repeat-lit
              solve literals more than once in counterexample-based quantifier instantiation [*]

       --cbqi-round-up-lia
              round  up integer lower bounds in substitutions for counterexample-based quantifier
              instantiation [*]

       --cbqi-sat
              answer sat when  quantifiers  are  asserted  with  counterexample-based  quantifier
              instantiation [*]

       --cbqi-use-inf-int
              use integer infinity for vts in counterexample-based quantifier instantiation [*]

       --cbqi-use-inf-real
              use real infinity for vts in counterexample-based quantifier instantiation [*]

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

       --cegqi
              counterexample-guided quantifier instantiation for sygus [*]

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

       --cegqi-si-partial
              combined  techniques for synthesis conjectures that are partially single invocation
              [*]

       --cegqi-si-reconstruct
              reconstruct solutions for single invocation conjectures in original grammar [*]

       --cegqi-si-reconstruct-const
              include constants when reconstruct solutions for single invocation  conjectures  in
              original grammar [*]

       --cegqi-si-sol-min-core
              minimize solutions for single invocation conjectures based on unsat core [*]

       --cegqi-si-sol-min-inst
              minimize individual instantiations for single invocation conjectures based on unsat
              core [*]

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

       --cond-rewrite-quant
              conditional rewriting of quantified formulas [*]

       --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-ext-arith-quant
              eliminate extended arithmetic symbols in quantified formulas [*]

       --elim-taut-quant
              eliminate tautological disjuncts 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-bound-min-mode=MODE
              mode for which types of bounds to minimize via first decision heuristics

       --fmf-empty-sorts
              allow  finite  model finding to assume sorts that do not occur in ground assertions
              are empty [*]

       --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-inst-gen
              enable Inst-Gen instantiation techniques for finite model finding [*]

       --fmf-inst-gen-one-quant-per-round
              only perform Inst-Gen instantiation techniques on one quantifier per round [*]

       --fs-interleave
              interleave full saturate instantiation with other techniques [*]

       --full-saturate-quant
              when  all  other  quantifier instantiation strategies fail, instantiate with ground
              terms from relevant domain, then arbitrary ground terms  before  answering  unknown
              [*]

       --full-saturate-quant-rd
              whether to use relevant domain first for full saturation instantiation strategy [*]

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

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

       --infer-arith-trigger-eq
              infer equalities for trigger terms based on solving arithmetic equalities [*]

       --infer-arith-trigger-eq-exp
              record explanations for inferArithTriggerEq [*]

       --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-no-entail
              do not consider instances of quantified formulas that are currently entailed [*]

       --inst-no-model-true
              do not consider instances of quantified formulas that are currently true in  model,
              if it is available [*]

       --inst-prop
              internal propagation for instantiations for selecting relevant instances [*]

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

       --inst-when=MODE
              when to apply instantiation

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

       --local-t-ext
              do instantiation based on local theory extensions [*]

       --lte-partial-inst
              partially instantiate local theory quantifiers [*]

       --lte-restrict-inst-closure
              treat arguments of inst closure as restricted terms for instantiation [*]

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

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

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

       --mbqi-one-quant-per-round
              only add instantiations for one quantifier per round for mbqi [*]

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

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

       --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-user
              prenex quantified formulas with user patterns [*]

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

       --pure-th-triggers
              use pure theory terms as single triggers [*]

       --purify-dt-triggers
              purify dt triggers, match all constructors of correct form instead of selectors [*]

       --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-anti-skolem
              perform anti-skolemization for 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-epr
              infer whether in effectively propositional fragment, use for cbqi [*]

       --quant-epr-match
              use matching heuristics for EPR instantiation [*]

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

       --quant-ind
              use all available techniques for inductive reasoning [*]

       --quant-model-ee
              use equality engine of model for last call effort [*]

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

       --rewrite-rules
              use rewrite rules module [*]

       --rr-one-inst-per-round
              add one instance of rewrite rule per round [*]

       --strict-triggers
              only instantiate quantifiers with user patterns based on triggers [*]

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

       --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-eval-unfold
              do unfolding of sygus evaluation functions [*]

       --sygus-eval-unfold-bool
              do unfolding of Boolean evaluation functions that appear in refinement lemmas [*]

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

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

       --sygus-inference
              attempt to preprocess arbitrary inputs to sygus conjectures [*]

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

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

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

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

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

       --sygus-ref-eval
              direct evaluation of refinement lemmas for conflict analysis [*]

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

       --sygus-rr
              use sygus to enumerate and verify correctness of rewrite rules via sampling [*]

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

       --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-order
              filter candidate rewrites based on variable ordering [*]

       --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-grammar
              when applicable, use grammar for choosing sample points [*]

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

       --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
              Unification-based function synthesis [*]

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

       --track-inst-lemmas
              track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)
              [*]

       --trigger-active-sel
              selection mode to activate triggers

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

SEP OPTIONS

       --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-exp
              experimental flag for sep [*]

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

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

SETS OPTIONS

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

       --sets-rel-eager
              standard effort checks for relations [*]

SMT LAYER OPTIONS

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

       --bitblast-step
              amount of resources spent for each bitblast step (EXPERTS only)

       --bv-sat-conflict-step
              amount of resources spent for each sat conflict (bitvectors) (EXPERTS only)

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

       --check-proofs
              after UNSAT/VALID, machine-check the generated 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) [*]

       --cnf-step
              amount of resources spent for each call to cnf conversion (EXPERTS only)

       --decision-step
              amount of getNext decision calls in the decision engine (EXPERTS only)

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

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

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

       --dump-synth
              output solution for synthesis conjectures after every UNSAT/VALID response [*]

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

       --dump-unsat-cores-full
              dump the full unsat core, including unlabeled assertions [*]

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

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

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

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

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

       --lemma-step
              amount of resources spent when adding lemmas (EXPERTS only)

       --model-u-dt-enum
              in models, output uninterpreted sorts as datatype enumerations [*]

       --omit-dont-cares
              When producing a model, omit variables whose value does not matter [*]

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

       --parse-step
              amount of resources spent for each command/expression parsing (EXPERTS only)

       --preprocess-step
              amount of resources spent for each preprocessing step in SmtEngine (EXPERTS only)

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

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

       --produce-unsat-cores
              turn on unsat core generation [*]

       --proof
              turn on proof generation [*]

       --quantifier-step
              amount of resources spent for quantifier instantiations (EXPERTS only)

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

       --restart-step
              amount of resources spent for each theory restart (EXPERTS only)

       --rewrite-apply-to-const
              eliminate  function  applications, rewriting e.g. f(5) to a new symbol f_5 (EXPERTS
              only) [*]

       --rewrite-step
              amount of resources spent for each rewrite step (EXPERTS only)

       --sat-conflict-step
              amount of resources spent for each sat conflict (main sat solver) (EXPERTS only)

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

       --simp-ite-hunt-zombies
              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
              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

       --sygus-print-callbacks
              use sygus print callbacks to print sygus terms in the user-provided  form  (disable
              for debugging) [*]

       --symmetry-breaker-exp
              generate symmetry breaking constraints after symmetry detection [*]

       --theory-check-step
              amount of resources spent for each theory check call (EXPERTS only)

       --unconstrained-simp
              turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis) [*]

       --no-simplification
              turn off all simplification (same as --simplification=none)

STRINGS THEORY OPTIONS

       --strings-abort-loop
              abort when a looping word equation is encountered [*]

       --strings-binary-csp
              use binary search when splitting strings [*]

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

       --strings-eager
              strings eager check [*]

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

       --strings-eit
              the eager intersection used by the theory of strings [*]

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

       --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-inm
              internal  for strings: ignore negative membership constraints (fragment checking is
              needed, left to users for now) [*]

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

       --strings-lb=N
              the strategy of LB rule application: 0-lazy, 1-eager, 2-no

       --strings-len-geqz
              strings length greater than zero lemmas [*]

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

       --strings-lprop-csp
              do length propagation based on constant splits [*]

       --strings-min-prefix-explain
              minimize explanations for prefix of normal forms in strings [*]

       --strings-opt1
              internal option1 for strings: normal form [*]

       --strings-opt2
              internal option2 for strings: constant regexp splitting [*]

       --strings-print-ascii
              the alphabet contains only printable characters from the  standard  extended  ASCII
              [*]

       --strings-process-loop
              reduce looping word equations to regular expressions [*]

       --strings-rexplain-lemmas
              regression explanations for string lemmas [*]

       --strings-sp-emp
              strings split on empty string [*]

       --strings-uf-reduct
              use uninterpreted functions when applying extended function reductions [*]

THEORY LAYER OPTIONS

       --assign-function-values
              assign values for uninterpreted functions in models [*]

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

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

       --use-theory=NAME
              use alternate theory implementation  NAME  (--use-theory=help  for  a  list).  This
              option may be repeated or a comma separated list.

UNINTERPRETED FUNCTIONS THEORY OPTIONS

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

       --uf-ho
              enable support for higher-order reasoning [*]

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

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

       --uf-ss-clique-splits
              use cliques instead of splitting on demand to shrink model [*]

       --uf-ss-eager-split
              add splits eagerly for uf strong solver [*]

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

       --uf-ss-regions
              disable region-based method for discovering cliques and splits in uf strong  solver
              [*]

       --uf-ss-totality
              always use totality axioms for enforcing cardinality constraints [*]

       --uf-ss-totality-limited=N
              apply  totality  axioms,  but only up to cardinality N (-1 == do not apply totality
              axioms, default)

       --uf-ss-totality-sym-break
              apply symmetry breaking for totality axioms [*]

       --uf-ss=MODE
              mode of operation for uf strong solver.

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

DIAGNOSTICS

       CVC4 reports all syntactic and semantic errors on standard error.

HISTORY

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

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

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

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

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

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

VERSION

       This manual page refers to CVC4 version 1.6.

BUGS

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

AUTHORS

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

SEE ALSO

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