# SmtEngine.3cvc man page

SmtEngine — the primary interface to CVC4's theorem-proving capabilities

## Description

**SmtEngine** is the main entry point into the CVC4 theorem prover API.

## Smtengine Options

The SmtEngine is in charge of setting and getting information and options. Numerous options are available via the *SmtEngine::setOption()* call. *SmtEngine::setOption()* and *SmtEngine::getOption()* use the following option keys.

*COMMON OPTIONS***input-language**(InputLanguage) force input language (default is "auto"; see --lang help)

**output-language**(OutputLanguage) force output language (default is "auto"; see --output-lang help)

**quiet**(void) decrease verbosity (may be repeated)

**statistics**(bool) give statistics on exit

**verbose**(void) increase verbosity (may be repeated)

**copyright**(void) show CVC4 copyright information

**help**(bool) full command line reference

**seed**(uint64_t) seed for random number generator

**show-config**(void) show CVC4 static configuration

**version**(bool) identify this CVC4 binary

**strict-parsing**(bool) be less tolerant of non-conforming inputs

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

**dump-to**(std::string) all dumping goes to FILE (instead of stdout)

**dump**(std::string) dump preprocessed assertions, etc., see --dump=help

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

**incremental**(bool) enable incremental solving

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

**produce-models**(bool) support the get-value and get-model commands

**reproducible-resource-limit**(unsigned long) enable resource limiting per query

**rlimit**(unsigned long) enable resource limiting (currently, roughly the number of SAT conflicts)

**tlimit-per**(unsigned long) enable time limiting per query (give milliseconds)

**tlimit**(unsigned long) enable time limiting (give milliseconds)

*ARITHMETIC THEORY OPTIONS***approx-branch-depth**(int16_t) maximum branch depth the approximate solver is allowed to take

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

**arith-prop-clauses**(uint16_t) rows shorter than this are propagated as clauses

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

**arith-rewrite-equalities**(bool) turns on the preprocessing rewrite turning equalities into a conjunction of inequalities

**collect-pivot-stats**(bool) collect the pivot history

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

**dio-decomps**(bool) let skolem variables for integer divisibility constraints leak from the dio solver

**dio-repeat**(bool) handle dio solver constraints in mass or one at a time

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

**dio-turns**(int) turns in a row dio solver cutting gets

**error-selection-rule**(ErrorSelectionRule) change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)

**fc-penalties**(bool) turns on degenerate pivot penalties

**heuristic-pivots**(int16_t) 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**(bool) attempt to use external lemmas if approximate solve integer failed

**maxCutsInContext**(unsigned) maximum cuts in a given context before signalling a restart

**miplib-trick**(bool) turns on the preprocessing step of attempting to infer bounds on miplib problems

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

**new-prop**(bool) use the new row propagation system

**nl-ext**(bool) extended approach to non-linear

**nl-ext-ent-conf**(bool) check for entailed conflicts in non-linear solver

**nl-ext-factor**(bool) use factoring inference in non-linear solver

**nl-ext-inc-prec**(bool) whether to increment the precision for irrational function constraints

**nl-ext-purify**(bool) purify non-linear terms at preprocess

**nl-ext-rbound**(bool) use resolution-style inference for inferring new bounds

**nl-ext-rewrite**(bool) do rewrites in non-linear solver

**nl-ext-split-zero**(bool) intial splits on zero for all variables

**nl-ext-tf-taylor-deg**(int16_t) initial degree of polynomials for Taylor approximation

**nl-ext-tf-tplanes**(bool) use non-terminating tangent plane strategy for transcendental functions for non-linear

**nl-ext-tplanes**(bool) use non-terminating tangent plane strategy for non-linear

**nl-ext-tplanes-interleave**(bool) interleave tangent plane strategy for non-linear

**pb-rewrites**(bool) apply pseudo boolean rewrites

**pivot-threshold**(uint16_t) sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order

**pp-assert-max-sub-size**(unsigned) threshold for substituting an equality in ppAssert

**prop-row-length**(uint16_t) sets the maximum row length to be used in propagation

**replay-early-close-depth**(int) multiples of the depths to try to close the approx log eagerly

**replay-failure-penalty**(int) number of solve integer attempts to skips after a numeric failure

**replay-lemma-reject-cut**(unsigned) maximum complexity of any coefficient while outputting replaying cut lemmas

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

**replay-reject-cut**(unsigned) maximum complexity of any coefficient while replaying cuts

**replay-soi-major-threshold**(double) threshold for a major tolerance failure by the approximate solver

**replay-soi-major-threshold-pen**(int) threshold for a major tolerance failure by the approximate solver

**replay-soi-minor-threshold**(double) threshold for a minor tolerance failure by the approximate solver

**replay-soi-minor-threshold-pen**(int) threshold for a minor tolerance failure by the approximate solver

**restrict-pivots**(bool) have a pivot cap for simplex at effort levels below fullEffort

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

**rewrite-divk**(bool) rewrite division and mod when by a constant into linear terms

**rr-turns**(int) round robin turn

**se-solve-int**(bool) attempt to use the approximate solve integer method on standard effort

**simplex-check-period**(uint16_t) the number of pivots to do in simplex before rechecking for a conflict on all variables

**snorm-infer-eq**(bool) infer equalities based on Shostak normalization

**soi-qe**(bool) use quick explain to minimize the sum of infeasibility conflicts

**standard-effort-variable-order-pivots**(int16_t) 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**(ArithUnateLemmaMode) determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)

**use-approx**(bool) attempt to use an approximate solver

**use-fcsimplex**(bool) use focusing and converging simplex (FMCAD 2013 submission)

**use-soi**(bool) use sum of infeasibility simplex (FMCAD 2013 submission)

*ARRAYS THEORY OPTIONS***arrays-config**(int) set different array option configurations - for developers only

**arrays-eager-index**(bool) turn on eager index splitting for generated array lemmas

**arrays-eager-lemmas**(bool) turn on eager lemma generation for arrays

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

**arrays-model-based**(bool) turn on model-based array solver

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

**arrays-prop**(int) propagation effort for arrays: 0 is none, 1 is some, 2 is full

**arrays-reduce-sharing**(bool) use model information to reduce size of care graph for arrays

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

*BASE OPTIONS***debug**(std::string) debug something (e.g. -d arith), can repeat

**parse-only**(bool) exit after parsing input

**preprocess-only**(bool) exit after preprocessing input

**print-success**(bool) print the "success" output required of SMT-LIBv2

**stats-every-query**(bool) in incremental mode, print stats after every satisfiability or validity query

**stats-hide-zeros**(bool) hide statistics which are zero

**trace**(std::string) trace something (e.g. -t pushpop), can repeat

**verbosity**(int) the verbosity level of CVC4

**hide-zero-stats**[undocumented]

**language**[undocumented]

**no-statistics**[undocumented]

**no-statistics-every-query**[undocumented]

**output-language**[undocumented]

**show-zero-stats**[undocumented]

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

**statistics**[undocumented]

**statistics-every-query**[undocumented]

**stats-show-zeros**[undocumented]

*BITVECTOR THEORY OPTIONS***bitblast-aig**(bool) bitblast by first converting to AIG (implies --bitblast=eager)

**bitblast**(CVC4::theory::bv::BitblastMode) choose bitblasting mode, see --bitblast=help

**bool-to-bv**(bool) convert booleans to bit-vectors of size 1 when possible

**bv-abstraction**(bool) mcm benchmark abstraction (EXPERTS only)

**bv-aig-simp**(std::string) abc command to run AIG simplifications (implies --bitblast-aig, default is "balance;drw") (EXPERTS only)

**bv-alg-extf**(bool) algebraic inferences for extended functions

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

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

**bv-div-zero-const**(bool) always return -1 on division by zero

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

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

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

**bv-extract-arith**(bool) enable rewrite pushing extract [i:0] over arithmetic operations (can blow up) (EXPERTS only)

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

**bv-inequality-solver**(bool) turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy)

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

**bv-lazy-reduce-extf**(bool) reduce extended functions like bv2nat and int2bv at last call instead of full effort

**bv-lazy-rewrite-extf**(bool) lazily rewrite extended functions like bv2nat and int2bv

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

**bv-propagate**(bool) use bit-vector propagation in the bit-blaster

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

**bv-sat-solver**(CVC4::theory::bv::SatSolverMode) choose which sat solver to use, see --bv-sat-solver=help (EXPERTS only)

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

**bv-to-bool**(bool) lift bit-vectors of size 1 to booleans when possible

*DATATYPES THEORY OPTIONS***cdt-bisimilar**(bool) do bisimilarity check for co-datatypes

**dt-binary-split**(bool) do binary splits for datatype constructor types

**dt-blast-splits**(bool) when applicable, blast splitting lemmas for all variables at once

**dt-cyclic**(bool) do cyclicity check for datatypes

**dt-force-assignment**(bool) force the datatypes solver to give specific values to all datatypes terms before answering sat

**dt-infer-as-lemmas**(bool) always send lemmas out instead of making internal inferences

**dt-ref-sk-intro**(bool) introduce reference skolems for shorter explanations

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

**dt-share-sel**(bool) internally use shared selectors across multiple constructors

**dt-use-testers**(bool) do not preprocess away tester predicates

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

**sygus-eval-builtin**(bool) use builtin kind for evaluation functions in sygus

**sygus-fair-max**(bool) use max instead of sum for multi-function sygus conjectures

**sygus-fair**(CVC4::theory::SygusFairMode) if and how to apply fairness for sygus

**sygus-opt1**(bool) sygus experimental option

**sygus-sym-break**(bool) simple sygus sym break lemmas

**sygus-sym-break-dynamic**(bool) dynamic sygus sym break lemmas

**sygus-sym-break-lazy**(bool) lazily add symmetry breaking lemmas for terms

**sygus-sym-break-pbe**(bool) sygus sym break lemmas based on pbe conjectures

**sygus-sym-break-rlv**(bool) add relevancy conditions to symmetry breaking lemmas

*DECISION HEURISTICS OPTIONS***decision-random-weight**(int) assign random weights to nodes between 0 and N-1 (0: disable) (EXPERTS only)

**decision-threshold**(decision::DecisionWeight) ignore all nodes greater than threshold in first attempt to pick decision (EXPERTS only)

**decision-use-weight**(bool) use the weight nodes (locally, by looking at children) to direct recursive search (EXPERTS only)

**decision-weight-internal**(decision::DecisionWeightInternal) computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving) (EXPERTS only)

**decision-mode**(decision::DecisionMode) choose decision mode, see --decision=help

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

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

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

**print-expr-types**(bool) print types with variables when printing exprs

**type-checking**(bool) never type check expressions

**dag-thresh**[undocumented]

**dag-threshold**[undocumented]

**expr-depth**[undocumented]

**no-type-checking**[undocumented]

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

*DRIVER OPTIONS***continued-execution**(bool) continue executing commands, even on error

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

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

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

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

**interactive**(bool) force interactive/non-interactive mode

**interactive-prompt**(bool) interactive prompting while in interactive mode

**segv-spin**(bool) spin on segfault/other crash waiting for gdb

**show-debug-tags**(void) show all available tags for debugging

**show-trace-tags**(void) show all available tags for tracing

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

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

**threadN**(void) configures portfolio thread N (0..#threads-1)

**threads**(unsigned) Total number of threads for portfolio

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

**license**[undocumented]

**segv-nospin**[undocumented]

*PARSER OPTIONS***filesystem-access**(bool) [undocumented]

**global-declarations**(bool) force all declarations and definitions to be global

**mmap**(bool) memory map file input

**semantic-checks**(bool) disable ALL semantic checks, including type checks

**no-checking**[undocumented]

**no-include-file**[undocumented]

*PRINTING OPTIONS***inst-format**(InstFormatMode) print format mode for instantiations, see --inst-format=help

**model-format**(ModelFormatMode) print format mode for models, see --model-format=help

*PROOF OPTIONS***aggressive-core-min**(bool) turns on aggressive unsat core minimization (experimental)

**allow-empty-dependencies**(bool) if unable to track the dependencies of a rewritten/preprocessed assertion, fail silently

**fewer-preprocessing-holes**(bool) try to eliminate preprocessing holes in proofs

**lfsc-letification**(bool) turns on global letification in LFSC proofs

*SAT LAYER OPTIONS***minisat-dump-dimacs**(bool) instead of solving minisat dumps the asserted clauses in Dimacs format

**minisat-elimination**(bool) use Minisat elimination

**random-frequency**(double) sets the frequency of random decisions in the sat solver (P=0.0 by default)

**random-seed**(uint32_t) sets the random seed for the sat solver

**refine-conflicts**(bool) refine theory conflict clauses (default false)

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

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

*QUANTIFIERS OPTIONS***ag-miniscope-quant**(bool) perform aggressive miniscoping for quantifiers

**cbqi**(bool) turns on counterexample-based quantifier instantiation

**cbqi-all**(bool) apply counterexample-based instantiation to all quantified formulas

**cbqi-bv**(bool) use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors

**cbqi-bv-concat-inv**(bool) compute inverse for concat over equalities rather than producing an invertibility condition

**cbqi-bv-ineq**(CVC4::theory::quantifiers::CbqiBvIneqMode) choose mode for handling bit-vector inequalities with counterexample-guided instantiation

**cbqi-bv-interleave-value**(bool) interleave model value instantiation with word-level inversion approach

**cbqi-bv-linear**(bool) linearize adder chains for variables

**cbqi-bv-rm-extract**(bool) replaces extract terms with variables for counterexample-guided instantiation for bit-vectors

**cbqi-bv-solve-nl**(bool) try to solve non-linear bv literals using model value projections

**cbqi-full**(bool) turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation

**cbqi-innermost**(bool) only process innermost quantified formulas in counterexample-based quantifier instantiation

**cbqi-lit-dep**(bool) dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation

**cbqi-midpoint**(bool) choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation

**cbqi-min-bounds**(bool) use minimally constrained lower/upper bound for counterexample-based quantifier instantiation

**cbqi-model**(bool) guide instantiations by model values for counterexample-based quantifier instantiation

**cbqi-multi-inst**(bool) when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation

**cbqi-nested-qe**(bool) process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation

**cbqi-nopt**(bool) non-optimal bounds for counterexample-based quantifier instantiation

**cbqi-prereg-inst**(bool) preregister ground instantiations in counterexample-based quantifier instantiation

**cbqi-recurse**(bool) turns on recursive counterexample-based quantifier instantiation

**cbqi-repeat-lit**(bool) solve literals more than once in counterexample-based quantifier instantiation

**cbqi-round-up-lia**(bool) round up integer lower bounds in substitutions for counterexample-based quantifier instantiation

**cbqi-sat**(bool) answer sat when quantifiers are asserted with counterexample-based quantifier instantiation

**cbqi-use-inf-int**(bool) use integer infinity for vts in counterexample-based quantifier instantiation

**cbqi-use-inf-real**(bool) use real infinity for vts in counterexample-based quantifier instantiation

**cegis-sample**(CVC4::theory::quantifiers::CegisSampleMode) mode for using samples in the counterexample-guided inductive synthesis loop

**cegqi**(bool) counterexample-guided quantifier instantiation for sygus

**cegqi-si-abort**(bool) abort if synthesis conjecture is not single invocation

**cegqi-si-partial**(bool) combined techniques for synthesis conjectures that are partially single invocation

**cegqi-si-reconstruct**(bool) reconstruct solutions for single invocation conjectures in original grammar

**cegqi-si-reconstruct-const**(bool) include constants when reconstruct solutions for single invocation conjectures in original grammar

**cegqi-si-sol-min-core**(bool) minimize solutions for single invocation conjectures based on unsat core

**cegqi-si-sol-min-inst**(bool) minimize individual instantiations for single invocation conjectures based on unsat core

**cegqi-si**(CVC4::theory::quantifiers::CegqiSingleInvMode) mode for processing single invocation synthesis conjectures

**cond-rewrite-quant**(bool) conditional rewriting of quantified formulas

**cond-var-split-agg-quant**(bool) aggressive split quantified formulas that lead to variable eliminations

**cond-var-split-quant**(bool) split quantified formulas that lead to variable eliminations

**conjecture-filter-active-terms**(bool) filter based on active terms

**conjecture-filter-canonical**(bool) filter based on canonicity

**conjecture-filter-model**(bool) filter based on model

**conjecture-gen**(bool) generate candidate conjectures for inductive proofs

**conjecture-gen-gt-enum**(int) number of ground terms to generate for model filtering

**conjecture-gen-max-depth**(int) maximum depth of terms to consider for conjectures

**conjecture-gen-per-round**(int) number of conjectures to generate per instantiation round

**conjecture-gen-uee-intro**(bool) more aggressive merging for universal equality engine, introduces terms

**conjecture-no-filter**(bool) do not filter conjectures

**dt-stc-ind**(bool) apply strengthening for existential quantification over datatypes based on structural induction

**dt-var-exp-quant**(bool) expand datatype variables bound to one constructor in quantifiers

**e-matching**(bool) whether to do heuristic E-matching

**elim-ext-arith-quant**(bool) eliminate extended arithmetic symbols in quantified formulas

**elim-taut-quant**(bool) eliminate tautological disjuncts of quantified formulas

**finite-model-find**(bool) use finite model finding heuristic for quantifier instantiation

**fmf-bound**(bool) finite model finding on bounded quantification

**fmf-bound-int**(bool) finite model finding on bounded integer quantification

**fmf-bound-lazy**(bool) enforce bounds for bounded quantification lazily via use of proxy variables

**fmf-bound-min-mode**(CVC4::theory::quantifiers::FmfBoundMinMode) mode for which types of bounds to minimize via first decision heuristics

**fmf-empty-sorts**(bool) allow finite model finding to assume sorts that do not occur in ground assertions are empty

**fmf-fmc-simple**(bool) simple models in full model check for finite model finding

**fmf-fresh-dc**(bool) use fresh distinguished representative when applying Inst-Gen techniques

**fmf-fun**(bool) find models for recursively defined functions, assumes functions are admissible

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

**fmf-inst-engine**(bool) use instantiation engine in conjunction with finite model finding

**fmf-inst-gen**(bool) enable Inst-Gen instantiation techniques for finite model finding

**fmf-inst-gen-one-quant-per-round**(bool) only perform Inst-Gen instantiation techniques on one quantifier per round

**fs-interleave**(bool) interleave full saturate instantiation with other techniques

**full-saturate-quant**(bool) 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**(bool) whether to use relevant domain first for full saturation instantiation strategy

**global-negate**(bool) do global negation of input formula

**ho-matching**(bool) do higher-order matching algorithm for triggers with variable operators

**ho-matching-var-priority**(bool) give priority to variable arguments over constant arguments

**ho-merge-term-db**(bool) merge term indices modulo equality

**increment-triggers**(bool) generate additional triggers as needed during search

**infer-arith-trigger-eq**(bool) infer equalities for trigger terms based on solving arithmetic equalities

**infer-arith-trigger-eq-exp**(bool) record explanations for inferArithTriggerEq

**inst-level-input-only**(bool) only input terms are assigned instantiation level zero

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

**inst-no-entail**(bool) do not consider instances of quantified formulas that are currently entailed

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

**inst-prop**(bool) internal propagation for instantiations for selecting relevant instances

**inst-when-phase**(int) instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen

**inst-when-strict-interleave**(bool) ensure theory combination and standard quantifier effort strategies take turns

**inst-when-tc-first**(bool) allow theory combination to happen once initially, before quantifier strategies are run

**inst-when**(CVC4::theory::quantifiers::InstWhenMode) when to apply instantiation

**int-wf-ind**(bool) apply strengthening for integers based on well-founded induction

**ite-dtt-split-quant**(bool) split ites with dt testers as conditions

**ite-lift-quant**(CVC4::theory::quantifiers::IteLiftQuantMode) ite lifting mode for quantified formulas

**literal-matching**(CVC4::theory::quantifiers::LiteralMatchMode) choose literal matching mode

**local-t-ext**(bool) do instantiation based on local theory extensions

**lte-partial-inst**(bool) partially instantiate local theory quantifiers

**lte-restrict-inst-closure**(bool) treat arguments of inst closure as restricted terms for instantiation

**macros-quant**(bool) perform quantifiers macro expansion

**macros-quant-mode**(CVC4::theory::quantifiers::MacrosQuantMode) mode for quantifiers macro expansion

**mbqi-interleave**(bool) interleave model-based quantifier instantiation with other techniques

**mbqi-one-inst-per-round**(bool) only add one instantiation per quantifier per round for mbqi

**mbqi-one-quant-per-round**(bool) only add instantiations for one quantifier per round for mbqi

**mbqi**(CVC4::theory::quantifiers::MbqiMode) choose mode for model-based quantifier instantiation

**miniscope-quant**(bool) miniscope quantifiers

**miniscope-quant-fv**(bool) miniscope quantifiers for ground subformulas

**multi-trigger-cache**(bool) caching version of multi triggers

**multi-trigger-linear**(bool) implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms

**multi-trigger-priority**(bool) only try multi triggers if single triggers give no instantiations

**multi-trigger-when-single**(bool) select multi triggers when single triggers exist

**partial-triggers**(bool) use triggers that do not contain all free variables

**pre-skolem-quant**(bool) apply skolemization eagerly to bodies of quantified formulas

**pre-skolem-quant-agg**(bool) apply skolemization to quantified formulas aggressively

**pre-skolem-quant-nested**(bool) apply skolemization to nested quantified formulas

**prenex-quant-user**(bool) prenex quantified formulas with user patterns

**prenex-quant**(CVC4::theory::quantifiers::PrenexQuantMode) prenex mode for quantified formulas

**pure-th-triggers**(bool) use pure theory terms as single triggers

**purify-dt-triggers**(bool) purify dt triggers, match all constructors of correct form instead of selectors

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

**qcf-all-conflict**(bool) add all available conflicting instances during conflict-based instantiation

**qcf-eager-check-rd**(bool) optimization, eagerly check relevant domain of matched position

**qcf-eager-test**(bool) optimization, test qcf instances eagerly

**qcf-nested-conflict**(bool) consider conflicts for nested quantifiers

**qcf-skip-rd**(bool) optimization, skip instances based on possibly irrelevant portions of quantified formulas

**qcf-tconstraint**(bool) enable entailment checks for t-constraints in qcf algorithm

**qcf-vo-exp**(bool) qcf experimental variable ordering

**quant-alpha-equiv**(bool) infer alpha equivalence between quantified formulas

**quant-anti-skolem**(bool) perform anti-skolemization for quantified formulas

**quant-cf**(bool) enable conflict find mechanism for quantifiers

**quant-cf-mode**(CVC4::theory::quantifiers::QcfMode) what effort to apply conflict find mechanism

**quant-cf-when**(CVC4::theory::quantifiers::QcfWhenMode) when to invoke conflict find mechanism for quantifiers

**quant-dsplit-mode**(CVC4::theory::quantifiers::QuantDSplitMode) mode for dynamic quantifiers splitting

**quant-epr**(bool) infer whether in effectively propositional fragment, use for cbqi

**quant-epr-match**(bool) use matching heuristics for EPR instantiation

**quant-fun-wd**(bool) assume that function defined by quantifiers are well defined

**quant-ind**(bool) use all available techniques for inductive reasoning

**quant-model-ee**(bool) use equality engine of model for last call effort

**quant-rep-mode**(CVC4::theory::quantifiers::QuantRepMode) selection mode for representatives in quantifiers engine

**quant-split**(bool) apply splitting to quantified formulas based on variable disjoint disjuncts

**register-quant-body-terms**(bool) consider ground terms within bodies of quantified formulas for matching

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

**relevant-triggers**(bool) prefer triggers that are more relevant based on SInE style analysis

**rewrite-rules**(bool) use rewrite rules module

**rr-one-inst-per-round**(bool) add one instance of rewrite rule per round

**strict-triggers**(bool) only instantiate quantifiers with user patterns based on triggers

**sygus-add-const-grammar**(bool) statically add constants appearing in conjecture to grammars

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

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

**sygus-eval-unfold**(bool) do unfolding of sygus evaluation functions

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

**sygus-ext-rew**(bool) use extended rewriter for sygus

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

**sygus-inference**(bool) attempt to preprocess arbitrary inputs to sygus conjectures

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

**sygus-inv-templ**(CVC4::theory::quantifiers::SygusInvTemplMode) template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)

**sygus-min-grammar**(bool) statically minimize sygus grammars

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

**sygus-qe-preproc**(bool) use quantifier elimination as a preprocessing step for sygus

**sygus-ref-eval**(bool) direct evaluation of refinement lemmas for conflict analysis

**sygus-repair-const**(bool) use approach to repair constants in sygus candidate solutions

**sygus-rr**(bool) use sygus to enumerate and verify correctness of rewrite rules via sampling

**sygus-rr-synth**(bool) use sygus to enumerate candidate rewrite rules via sampling

**sygus-rr-synth-accel**(bool) add dynamic symmetry breaking clauses based on candidate rewrites

**sygus-rr-synth-check**(bool) use satisfiability check to verify correctness of candidate rewrites

**sygus-rr-synth-filter-cong**(bool) filter candidate rewrites based on congruence

**sygus-rr-synth-filter-match**(bool) filter candidate rewrites based on matching

**sygus-rr-synth-filter-order**(bool) filter candidate rewrites based on variable ordering

**sygus-rr-verify**(bool) use sygus to verify the correctness of rewrite rules via sampling

**sygus-rr-verify-abort**(bool) abort when sygus-rr-verify finds an instance of unsoundness

**sygus-sample-grammar**(bool) when applicable, use grammar for choosing sample points

**sygus-samples**(int) number of points to consider when doing sygus rewriter sample testing

**sygus-stream**(bool) enumerate a stream of solutions instead of terminating after the first one

**sygus-templ-embed-grammar**(bool) embed sygus templates into grammars

**sygus-unif**(bool) Unification-based function synthesis

**term-db-mode**(CVC4::theory::quantifiers::TermDbMode) which ground terms to consider for instantiation

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

**trigger-active-sel**(CVC4::theory::quantifiers::TriggerActiveSelMode) selection mode to activate triggers

**trigger-sel**(CVC4::theory::quantifiers::TriggerSelMode) selection mode for triggers

**user-pat**(CVC4::theory::quantifiers::UserPatMode) policy for handling user-provided patterns for quantifier instantiation

**var-elim-quant**(bool) enable simple variable elimination for quantified formulas

**var-ineq-elim-quant**(bool) enable variable elimination based on infinite projection of unbound arithmetic variables

*SEP OPTIONS***sep-check-neg**(bool) check negated spatial assertions

**sep-child-refine**(bool) child-specific refinements of negated star, positive wand

**sep-deq-c**(bool) assume cardinality elements are distinct

**sep-exp**(bool) experimental flag for sep

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

**sep-pre-skolem-emp**(bool) eliminate emp constraint at preprocess time

*SETS OPTIONS***sets-ext**(bool) enable extended symbols such as complement and universe in theory of sets

**sets-infer-as-lemmas**(bool) send inferences as lemmas

**sets-proxy-lemmas**(bool) introduce proxy variables eagerly to shorten lemmas

**sets-rel-eager**(bool) standard effort checks for relations

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

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

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

**check-models**(bool) after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions

**check-proofs**(bool) after UNSAT/VALID, machine-check the generated proof

**check-synth-sol**(bool) checks whether produced solutions to functions-to-synthesize satisfy the conjecture

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

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

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

**diagnostic-output-channel**(std::string) set the diagnostic output channel of the solver

**dump-instantiations**(bool) output instantiations of quantified formulas after every UNSAT/VALID response

**dump-models**(bool) output models after every SAT/INVALID/UNKNOWN response

**dump-proofs**(bool) output proofs after every UNSAT/VALID response

**dump-synth**(bool) output solution for synthesis conjectures after every UNSAT/VALID response

**dump-unsat-cores**(bool) output unsat cores after every UNSAT/VALID response

**dump-unsat-cores-full**(bool) dump the full unsat core, including unlabeled assertions

**expand-definitions**(bool) always expand symbol definitions in output

**ext-rew-prep**(bool) use extended rewriter as a preprocessing pass

**ext-rew-prep-agg**(bool) use aggressive extended rewriter as a preprocessing pass

**force-logic**(std::string) set the logic, and override all further user attempts to change it (EXPERTS only)

**force-no-limit-cpu-while-dump**(bool) Force no CPU limit when dumping models and proofs

**interactive-mode**(bool) deprecated name for produce-assertions

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

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

**model-u-dt-enum**(bool) in models, output uninterpreted sorts as datatype enumerations

**omit-dont-cares**(bool) When producing a model, omit variables whose value does not matter

**on-repeat-ite-simp**(bool) do the ite simplification pass again if repeating simplification

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

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

**produce-assignments**(bool) support the get-assignment command

**produce-unsat-assumptions**(bool) turn on unsat assumptions generation

**produce-unsat-cores**(bool) turn on unsat core generation

**produce-proofs**(bool) turn on proof generation

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

**regular-output-channel**(std::string) set the regular output channel of the solver

**repeat-simp**(bool) make multiple passes with nonclausal simplifier

**replay-log**(std::string) replay decisions from file

**replay**(std::string) replay decisions from file

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

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

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

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

**simp-ite-compress**(bool) enables compressing ites after ite simplification

**simp-ite-hunt-zombies**(uint32_t) post ite compression enables zombie removal while the number of nodes is above this threshold

**simp-with-care**(bool) enables simplifyWithCare in ite simplificiation

**simplification-mode**(SimplificationMode) choose simplification mode, see --simplification=help

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

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

**sort-inference**(bool) calculate sort inference of input problem, convert the input based on monotonic sorts

**static-learning**(bool) use static learning (on by default)

**sygus-out**(SygusSolutionOutMode) output mode for sygus

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

**symmetry-breaker-exp**(bool) generate symmetry breaking constraints after symmetry detection

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

**unconstrained-simp**(bool) 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**(bool) abort when a looping word equation is encountered

**strings-binary-csp**(bool) use binary search when splitting strings

**strings-check-entail-len**(bool) check entailment between length terms to reduce splitting

**strings-eager**(bool) strings eager check

**strings-eager-len**(bool) strings eager length lemmas

**strings-eit**(bool) the eager intersection used by the theory of strings

**strings-exp**(bool) experimental features in the theory of strings

**strings-fmf**(bool) the finite model finding used by the theory of strings

**strings-guess-model**(bool) use model guessing to avoid string extended function reductions

**strings-infer-as-lemmas**(bool) always send lemmas out instead of making internal inferences

**strings-infer-sym**(bool) strings split on empty string

**strings-inm**(bool) internal for strings: ignore negative membership constraints (fragment checking is needed, left to users for now)

**strings-lazy-pp**(bool) perform string preprocessing lazily

**strings-lb**(unsigned) the strategy of LB rule application: 0-lazy, 1-eager, 2-no

**strings-len-geqz**(bool) strings length greater than zero lemmas

**strings-len-norm**(bool) strings length normalization lemma

**strings-lprop-csp**(bool) do length propagation based on constant splits

**strings-min-prefix-explain**(bool) minimize explanations for prefix of normal forms in strings

**strings-opt1**(bool) internal option1 for strings: normal form

**strings-opt2**(bool) internal option2 for strings: constant regexp splitting

**strings-print-ascii**(bool) the alphabet contains only printable characters from the standard extended ASCII

**strings-process-loop**(bool) reduce looping word equations to regular expressions

**strings-rexplain-lemmas**(bool) regression explanations for string lemmas

**strings-sp-emp**(bool) strings split on empty string

**strings-uf-reduct**(bool) use uninterpreted functions when applying extended function reductions

*THEORY LAYER OPTIONS***assign-function-values**(bool) assign values for uninterpreted functions in models

**condense-function-values**(bool) condense values for functions in models rather than explicitly representing them

**theoryof-mode**(CVC4::theory::TheoryOfMode) mode for Theory::theoryof() (EXPERTS only)

**use-theory**(std::string) 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***uf-symmetry-breaker**(bool) use UF symmetry breaker (Deharbe et al., CADE 2011)

**uf-ho**(bool) enable support for higher-order reasoning

**uf-ho-ext**(bool) apply extensionality on function symbols

**uf-ss-abort-card**(int) 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**(bool) use cliques instead of splitting on demand to shrink model

**uf-ss-eager-split**(bool) add splits eagerly for uf strong solver

**uf-ss-fair**(bool) use fair strategy for finite model finding multiple sorts

**uf-ss-fair-monotone**(bool) group monotone sorts when enforcing fairness for finite model finding

**uf-ss-regions**(bool) disable region-based method for discovering cliques and splits in uf strong solver

**uf-ss-totality**(bool) always use totality axioms for enforcing cardinality constraints

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

**uf-ss-totality-sym-break**(bool) apply symmetry breaking for totality axioms

**uf-ss**(CVC4::theory::uf::UfssMode) mode of operation for uf strong solver.

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

libcvc4(3), libcvc4parser(3), libcvc4compat(3)

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