# options.3cvc man page

options — the options infrastructure

## Available Internal Options

*COMMON OPTIONS***inputLanguage**- (InputLanguage, default = language::input::LANG_AUTO)

force input language (default is "auto"; see --lang help) **outputLanguage**- (OutputLanguage, default = language::output::LANG_AUTO)

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

give statistics on exit **produceModels**- (bool, default = false)

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

force interactive mode **incrementalSolving**- (bool, default = true)

enable incremental solving **cumulativeMillisecondLimit**- (unsigned long)

enable time limiting (give milliseconds) **perCallMillisecondLimit**- (unsigned long)

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

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

enable resource limiting per query **version**- (bool)

identify this CVC4 binary **help**- (bool)

full command line reference **strictParsing**- (bool)

be less tolerant of non-conforming inputs *BASE OPTIONS***binary_name**- (std::string)

[undocumented] **in**- (std::istream*, default = &std::cin)

[undocumented] **out**- (std::ostream*, default = &std::cout)

[undocumented] **err**- (std::ostream*, default = &std::cerr)

[undocumented] **languageHelp**- (bool)

[undocumented] **verbosity**- (int, default = 0)

the verbosity level of CVC4 **statsEveryQuery**- (bool, default = false)

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

hide statistics which are zero **parseOnly**- (bool)

exit after parsing input **preprocessOnly**- (bool)

exit after preprocessing input **printSuccess**- (bool)

print the "success" output required of SMT-LIBv2 *EXPRESSION PACKAGE OPTIONS***defaultExprDepth**- (int, default = 0)

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

dagify common subexprs appearing > N times (1 == default, 0 == don't dagify) **earlyTypeChecking**- (bool, default = USE_EARLY_TYPE_CHECKING_BY_DEFAULT)

type check expressions immediately on creation (debug builds only) **typeChecking**- (bool, default = DO_SEMANTIC_CHECKS_BY_DEFAULT)
**This internal Boolean flag is undocumented; however, its alternate option --no-type-checking, which reverses the sense of the option, is documented thusly:**never type check expressions **biasedITERemoval**- (bool, default = false)

try the new remove ite pass that is biased against term ites appearing *BOOLEAN THEORY OPTIONS***booleanTermConversionMode**- (CVC4::theory::booleans::BooleanTermConversionMode, default = CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS)

policy for converting Boolean terms *THEORY LAYER OPTIONS***theoryOfMode**- (CVC4::theory::TheoryOfMode, default = CVC4::theory::THEORY_OF_TYPE_BASED)

mode for Theory::theoryof() (EXPERTS only) **theoryAlternates**- (::std::map<std::string,bool>)

[undocumented] *BITVECTOR THEORY OPTIONS***theoryAlternates**- (::std::map<std::string,bool>)

[undocumented] **bitblastMode**- (CVC4::theory::bv::BitblastMode, default = CVC4::theory::bv::BITBLAST_MODE_LAZY)

choose bitblasting mode, see --bitblast=help **bitvectorAig**- (bool, default = false)

bitblast by first converting to AIG (only if --bitblast=eager) **bitvectorAigSimplifications**- (std::string)

abc command to run AIG simplifications (EXPERTS only) **bitvectorPropagate**- (bool, default = true)

use bit-vector propagation in the bit-blaster **bitvectorEqualitySolver**- (bool, default = true)

use the equality engine for the bit-vector theory (only if --bitblast=lazy) **bitvectorEqualitySlicer**- (CVC4::theory::bv::BvSlicerMode, default = CVC4::theory::bv::BITVECTOR_SLICER_OFF)

turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy) **bitvectorInequalitySolver**- (bool, default = true)

turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy) **bitvectorAlgebraicSolver**- (bool, default = true)

turn on the algebraic solver for the bit-vector theory (only if --bitblast=lazy) **bitvectorAlgebraicBudget**- (unsigned, default = 1500)

the budget allowed for the algebraic solver in number of SAT conflicts (EXPERTS only) **bitvectorToBool**- (bool, default = false)

lift bit-vectors of size 1 to booleans when possible **bitvectorDivByZeroConst**- (bool, default = false)

always return -1 on division by zero **bvAbstraction**- (bool, default = false)

mcm benchmark abstraction (EXPERTS only) **skolemizeArguments**- (bool, default = false)

skolemize arguments for bv abstraction (only does something if --bv-abstraction is on) (EXPERTS only) **bvNumFunc**- (unsigned, default = 1)

number of function symbols in conflicts that are generalized (EXPERTS only) **bvEagerExplanations**- (bool, default = false)

compute bit-blasting propagation explanations eagerly (EXPERTS only) **bitvectorQuickXplain**- (bool, default = false)

minimize bv conflicts using the QuickXplain algorithm (EXPERTS only) **bvIntroducePow2**- (bool, default = false)

introduce bitvector powers of two as a preprocessing pass (EXPERTS only) *DATATYPES THEORY OPTIONS***dtRewriteErrorSel**- (bool, default = false)

rewrite incorrectly applied selectors to arbitrary ground term (EXPERTS only) **dtForceAssignment**- (bool, default = false)

force the datatypes solver to give specific values to all datatypes terms before answering sat *ARITHMETIC THEORY OPTIONS***arithUnateLemmaMode**- (ArithUnateLemmaMode, default = ALL_PRESOLVE_LEMMAS)

determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help) **arithPropagationMode**- (ArithPropagationMode, default = BOTH_PROP)

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

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 **arithStandardCheckVarOrderPivots**- (int16_t, default = -1)

limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule (EXPERTS only) **arithErrorSelectionRule**- (ErrorSelectionRule, default = MINIMUM_AMOUNT)

change the pivot rule for the basic variable (default is 'min', see --pivot-rule help) **arithSimplexCheckPeriod**- (uint16_t, default = 200)

the number of pivots to do in simplex before rechecking for a conflict on all variables **arithPivotThreshold**- (uint16_t, default = 2)

sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order **arithPropagateMaxLength**- (uint16_t, default = 16)

sets the maximum row length to be used in propagation **arithDioSolver**- (bool, default = true)
**This internal Boolean flag is undocumented; however, its alternate option --disable-dio-solver, which reverses the sense of the option, is documented thusly:**turns off Linear Diophantine Equation solver (Griggio, JSAT 2012) **arithRewriteEq**- (bool, default = false)

turns on the preprocessing rewrite turning equalities into a conjunction of inequalities **arithMLTrick**- (bool, default = false)

turns on the preprocessing step of attempting to infer bounds on miplib problems **arithMLTrickSubstitutions**- (unsigned, default = 1)

do substitution for miplib 'tmp' vars if defined in <= N eliminated vars **doCutAllBounded**- (bool, default = false)

turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds **maxCutsInContext**- (unsigned, default = 65535)

maximum cuts in a given context before signalling a restart **revertArithModels**- (bool, default = false)

revert the arithmetic model to a known safe model on unsat if one is cached **havePenalties**- (bool, default = false)

turns on degenerate pivot penalties **useFC**- (bool, default = false)

use focusing and converging simplex (FMCAD 2013 submission) **useSOI**- (bool, default = false)

use sum of infeasibility simplex (FMCAD 2013 submission) **restrictedPivots**- (bool, default = true)

have a pivot cap for simplex at effort levels below fullEffort **collectPivots**- (bool, default = false)

collect the pivot history **useApprox**- (bool, default = false)

attempt to use an approximate solver **maxApproxDepth**- (int16_t, default = 200)

maximum branch depth the approximate solver is allowed to take **exportDioDecompositions**- (bool, default = false)

let skolem variables for integer divisibility constraints leak from the dio solver **newProp**- (bool, default = false)

use the new row propagation system **arithPropAsLemmaLength**- (uint16_t, default = 8)

rows shorter than this are propagated as clauses **soiQuickExplain**- (bool, default = false)

use quick explain to minimize the sum of infeasibility conflicts **rewriteDivk**- (bool, default = false)

rewrite division and mod when by a constant into linear terms **trySolveIntStandardEffort**- (bool, default = false)

attempt to use the approximate solve integer method on standard effort **replayFailureLemma**- (bool, default = false)

attempt to use external lemmas if approximate solve integer failed **dioSolverTurns**- (int, default = 10)

turns in a row dio solver cutting gets **rrTurns**- (int, default = 3)

round robin turn **dioRepeat**- (bool, default = false)

handle dio solver constraints in mass or one at a time **replayEarlyCloseDepths**- (int, default = 1)

multiples of the depths to try to close the approx log eagerly **replayFailurePenalty**- (int, default = 100)

number of solve integer attempts to skips after a numeric failure **replayNumericFailurePenalty**- (int, default = 4194304)

number of solve integer attempts to skips after a numeric failure **replayRejectCutSize**- (unsigned, default = 25500)

maximum complexity of any coefficient while replaying cuts **lemmaRejectCutSize**- (unsigned, default = 25500)

maximum complexity of any coefficient while outputing replaying cut lemmas **soiApproxMajorFailure**- (double, default = .01)

threshold for a major tolerance failure by the approximate solver **soiApproxMajorFailurePen**- (int, default = 50)

threshold for a major tolerance failure by the approximate solver **soiApproxMinorFailure**- (double, default = .0001)

threshold for a minor tolerance failure by the approximate solver **soiApproxMinorFailurePen**- (int, default = 10)

threshold for a minor tolerance failure by the approximate solver **ppAssertMaxSubSize**- (unsigned, default = 2)

threshold for substituting an equality in ppAssert **maxReplayTree**- (int, default = 512)

threshold for attempting to replay a tree **pbRewrites**- (bool, default = false)

apply pseudo boolean rewrites **pbRewriteThreshold**- (int, default = 256)

threshold of number of pseudoboolean variables to have before doing rewrites *UNINTERPRETED FUNCTIONS THEORY OPTIONS***ufSymmetryBreaker**- (bool, default = true)

use UF symmetry breaker (Deharbe et al., CADE 2011) **condenseFunctionValues**- (bool, default = true)

condense models for functions rather than explicitly representing them **ufssRegions**- (bool, default = true)
**This internal Boolean flag is undocumented; however, its alternate option --disable-uf-ss-regions, which reverses the sense of the option, is documented thusly:**disable region-based method for discovering cliques and splits in uf strong solver **ufssEagerSplits**- (bool, default = false)

add splits eagerly for uf strong solver **ufssTotality**- (bool, default = false)

always use totality axioms for enforcing cardinality constraints **ufssTotalityLimited**- (int, default = -1)

apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default) **ufssTotalitySymBreak**- (bool, default = false)

apply symmetry breaking for totality axioms **ufssAbortCardinality**- (int, default = -1)

tells the uf strong solver a cardinality to abort at (-1 == no limit, default) **ufssExplainedCliques**- (bool, default = false)

use explained clique lemmas for uf strong solver **ufssSimpleCliques**- (bool, default = true)

always use simple clique lemmas for uf strong solver **ufssDiseqPropagation**- (bool, default = false)

eagerly propagate disequalities for uf strong solver **ufssMinimalModel**- (bool, default = true)
**This internal Boolean flag is undocumented; however, its alternate option --disable-uf-ss-min-model, which reverses the sense of the option, is documented thusly:**disable finding a minimal model in uf strong solver **ufssCliqueSplits**- (bool, default = false)

use cliques instead of splitting on demand to shrink model **ufssSymBreak**- (bool, default = false)

finite model finding symmetry breaking techniques **ufssFairness**- (bool, default = false)

use fair strategy for finite model finding multiple sorts *ARRAYS THEORY OPTIONS***arraysOptimizeLinear**- (bool, default = true)

turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper) **arraysLazyRIntro1**- (bool, default = true)

turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination) **arraysModelBased**- (bool, default = false)

turn on model-based arrray solver **arraysEagerIndexSplitting**- (bool, default = true)

turn on eager index splitting for generated array lemmas **arraysEagerLemmas**- (bool, default = false)

turn on eager lemma generation for arrays *QUANTIFIERS OPTIONS***miniscopeQuant**- (bool, default = true)
**This internal Boolean flag is undocumented; however, its alternate option --disable-miniscope-quant, which reverses the sense of the option, is documented thusly:**disable miniscope quantifiers **miniscopeQuantFreeVar**- (bool, default = true)
**This internal Boolean flag is undocumented; however, its alternate option --disable-miniscope-quant-fv, which reverses the sense of the option, is documented thusly:**disable miniscope quantifiers for ground subformulas **prenexQuant**- (bool, default = true)
**This internal Boolean flag is undocumented; however, its alternate option --disable-prenex-quant, which reverses the sense of the option, is documented thusly:**disable prenexing of quantified formulas **varElimQuant**- (bool, default = true)
**This internal Boolean flag is undocumented; however, its alternate option --disable-var-elim-quant, which reverses the sense of the option, is documented thusly:**disable simple variable elimination for quantified formulas **simpleIteLiftQuant**- (bool, default = true)
**This internal Boolean flag is undocumented; however, its alternate option --disable-ite-lift-quant, which reverses the sense of the option, is documented thusly:**disable simple ite lifting for quantified formulas **cnfQuant**- (bool, default = false)

apply CNF conversion to quantified formulas **nnfQuant**- (bool, default = false)

apply NNF conversion to quantified formulas **clauseSplit**- (bool, default = false)

apply clause splitting to quantified formulas **preSkolemQuant**- (bool, default = false)

apply skolemization eagerly to bodies of quantified formulas **aggressiveMiniscopeQuant**- (bool, default = false)

perform aggressive miniscoping for quantifiers **macrosQuant**- (bool, default = false)

perform quantifiers macro expansions **foPropQuant**- (bool, default = false)

perform first-order propagation on quantifiers **smartTriggers**- (bool, default = true)
**This internal Boolean flag is undocumented; however, its alternate option --disable-smart-triggers, which reverses the sense of the option, is documented thusly:**disable smart triggers **relevantTriggers**- (bool, default = false)

prefer triggers that are more relevant based on SInE style analysis **relationalTriggers**- (bool, default = false)

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

consider ground terms within bodies of quantified formulas for matching **instWhenMode**- (CVC4::theory::quantifiers::InstWhenMode, default = CVC4::theory::quantifiers::INST_WHEN_FULL)

when to apply instantiation **instMaxLevel**- (int, default = -1)

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

apply quantifier instantiation eagerly **fullSaturateQuant**- (bool, default = false)

when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown **literalMatchMode**- (CVC4::theory::quantifiers::LiteralMatchMode, default = CVC4::theory::quantifiers::LITERAL_MATCH_NONE)

choose literal matching mode **cbqi**- (bool, default = false)

turns on counterexample-based quantifier instantiation **recurseCbqi**- (bool, default = false)

turns on recursive counterexample-based quantifier instantiation **userPatternsQuant**- (CVC4::theory::quantifiers::UserPatMode, default = CVC4::theory::quantifiers::USER_PAT_MODE_DEFAULT)

policy for handling user-provided patterns for quantifier instantiation **flipDecision**- (bool, default = false)

turns on flip decision heuristic **internalReps**- (bool, default = true)
**This internal Boolean flag is undocumented; however, its alternate option --disable-quant-internal-reps, which reverses the sense of the option, is documented thusly:**disables instantiating with representatives chosen by quantifiers engine **finiteModelFind**- (bool, default = false)

use finite model finding heuristic for quantifier instantiation **mbqiMode**- (CVC4::theory::quantifiers::MbqiMode, default = CVC4::theory::quantifiers::MBQI_FMC)

choose mode for model-based quantifier instantiation **fmfOneInstPerRound**- (bool, default = false)

only add one instantiation per quantifier per round for mbqi **fmfOneQuantPerRound**- (bool, default = false)

only add instantiations for one quantifier per round for mbqi **fmfInstEngine**- (bool, default = false)

use instantiation engine in conjunction with finite model finding **fmfInstGen**- (bool, default = true)
**This internal Boolean flag is undocumented; however, its alternate option --disable-fmf-inst-gen, which reverses the sense of the option, is documented thusly:**disable Inst-Gen instantiation techniques for finite model finding **fmfInstGenOneQuantPerRound**- (bool, default = false)

only perform Inst-Gen instantiation techniques on one quantifier per round **fmfFreshDistConst**- (bool, default = false)

use fresh distinguished representative when applying Inst-Gen techniques **fmfFmcSimple**- (bool, default = true)
**This internal Boolean flag is undocumented; however, its alternate option --disable-fmf-fmc-simple, which reverses the sense of the option, is documented thusly:**disable simple models in full model check for finite model finding **fmfBoundInt**- (bool, default = false)

finite model finding on bounded integer quantification **fmfBoundIntLazy**- (bool, default = false)

enforce bounds for bounded integer quantification lazily via use of proxy variables **axiomInstMode**- (CVC4::theory::quantifiers::AxiomInstMode, default = CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT)

policy for instantiating axioms **quantConflictFind**- (bool, default = false)

enable conflict find mechanism for quantifiers **qcfMode**- (CVC4::theory::quantifiers::QcfMode, default = CVC4::theory::quantifiers::QCF_PROP_EQ)

what effort to apply conflict find mechanism **qcfWhenMode**- (CVC4::theory::quantifiers::QcfWhenMode, default = CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT)

when to invoke conflict find mechanism for quantifiers **qcfTConstraint**- (bool, default = false)

enable entailment checks for t-constraints in qcf algorithm **quantRewriteRules**- (bool, default = true)

use rewrite rules module **rrOneInstPerRound**- (bool, default = false)

add one instance of rewrite rule per round **dtStcInduction**- (bool, default = false)

apply strengthening for existential quantification over datatypes based on structural induction *STRINGS THEORY OPTIONS***stringExp**- (bool, default = false)

experimental features in the theory of strings **stringLB**- (unsigned, default = 0)

the strategy of LB rule application: 0-lazy, 1-eager, 2-no **stringFMF**- (bool, default = false)

the finite model finding used by the theory of strings **stringEIT**- (bool, default = false)

the eager intersection used by the theory of strings **stringOpt1**- (bool, default = true)

internal option1 for strings: normal form **stringOpt2**- (bool, default = false)

internal option2 for strings: constant regexp splitting **stringCharCardinality**- (int16_t, default = 256)

the cardinality of the characters used by the theory of strings, default 256 (EXPERTS only) *SAT LAYER OPTIONS***satRandomFreq**- (double, default = 0.0)

sets the frequency of random decisions in the sat solver (P=0.0 by default) **satRandomSeed**- (uint32_t, default = 0)

sets the random seed for the sat solver **satVarDecay**- (double, default = 0.95)

variable activity decay factor for Minisat **satClauseDecay**- (double, default = 0.999)

clause activity decay factor for Minisat **satRestartFirst**- (unsigned, default = 25)

sets the base restart interval for the sat solver (N=25 by default) **satRestartInc**- (double, default = 3.0)

sets the restart interval increase factor for the sat solver (F=3.0 by default) **sat_refine_conflicts**- (bool, default = false)

refine theory conflict clauses (default false) **minisatUseElim**- (bool, default = true)

use Minisat elimination **minisatDumpDimacs**- (bool, default = false)

instead of solving minisat dumps the asserted clauses in Dimacs format *PRINTING OPTIONS***modelFormatMode**- (ModelFormatMode, default = MODEL_FORMAT_MODE_DEFAULT)

print format mode for models, see --model-format=help **instFormatMode**- (InstFormatMode, default = INST_FORMAT_MODE_DEFAULT)

print format mode for instantiations, see --inst-format=help *SMT LAYER OPTIONS***forceLogic**- (LogicInfo, default = "")

set the logic, and override all further user attempts to change it (EXPERTS only) **simplificationMode**- (SimplificationMode, default = SIMPLIFICATION_MODE_BATCH)

choose simplification mode, see --simplification=help **doStaticLearning**- (bool, default = true)

use static learning (on by default) **expandDefinitions**- (bool, default = false)

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

after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions **dumpModels**- (bool, default = false)

output models after every SAT/INVALID/UNKNOWN response **proof**- (bool, default = false)

turn on proof generation **checkProofs**- (bool)

after UNSAT/VALID, machine-check the generated proof **dumpProofs**- (bool, default = false)

output proofs after every UNSAT/VALID response **dumpInstantiations**- (bool, default = false)

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

turn on unsat core generation (NOT YET SUPPORTED) **produceAssignments**- (bool, default = false)

support the get-assignment command **doITESimp**- (bool)

turn on ite simplification (Kim (and Somenzi) et al., SAT 2009) **doITESimpOnRepeat**- (bool, default = false)

do the ite simplification pass again if repeating simplification **simplifyWithCareEnabled**- (bool, default = false)

enables simplifyWithCare in ite simplificiation **compressItes**- (bool, default = false)

enables compressing ites after ite simplification **unconstrainedSimp**- (bool, default = false)

turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis) **repeatSimp**- (bool)

make multiple passes with nonclausal simplifier **zombieHuntThreshold**- (uint32_t, default = 524288)

post ite compression enables zombie removal while the number of nodes is above this threshold **sortInference**- (bool, default = false)

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

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

in models, output uninterpreted sorts as datatype enumerations **rewriteApplyToConst**- (bool, default = false)

eliminate function applications, rewriting e.g. f(5) to a new symbol f_5 (EXPERTS only) **replayFilename**- (std::string)

replay decisions from file **replayLog**- (std::ostream*)

log decisions and propagations to file **replayStream**- (ExprStream*)

[undocumented] **lemmaInputChannel**- (LemmaInputChannel*, default = NULL)

The input channel to receive notfication events for new lemmas **lemmaOutputChannel**- (LemmaOutputChannel*, default = NULL)

The output channel to receive notfication events for new lemmas **forceNoLimitCpuWhileDump**- (bool, default = false)

Force no CPU limit when dumping models and proofs *DECISION HEURISTICS OPTIONS***decisionMode**- (decision::DecisionMode, default = decision::DECISION_STRATEGY_INTERNAL)

choose decision mode, see --decision=help **decisionStopOnly**- (bool)

[undocumented] **decisionThreshold**- (decision::DecisionWeight, default = 0)

ignore all nodes greater than threshold in first attempt to pick decision (EXPERTS only) **decisionUseWeight**- (bool, default = false)

use the weight nodes (locally, by looking at children) to direct recursive search (EXPERTS only) **decisionRandomWeight**- (int, default = 0)

assign random weights to nodes between 0 and N-1 (0: disable) (EXPERTS only) **decisionWeightInternal**- (decision::DecisionWeightInternal, default = decision::DECISION_WEIGHT_INTERNAL_OFF)

computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving) (EXPERTS only) *DRIVER OPTIONS***earlyExit**- (bool, default = true)

do not run destructors at exit; default on except in debug builds (EXPERTS only) **threads**- (unsigned, default = 2)

Total number of threads for portfolio **threadStackSize**- (unsigned, default = 0)

stack size for worker threads in MB (0 means use Boost/thread lib default) **threadArgv**- (std::vector<std::string>)

Thread configuration (a string to be passed to parseOptions) **thread_id**- (int, default = -1)

Thread ID, for internal use in case of multi-threaded run **sharingFilterByLength**- (int, default = -1)

don't share (among portfolio threads) lemmas strictly longer than N **fallbackSequential**- (bool, default = false)

Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode **incrementalParallel**- (bool, default = false)

Use parallel solver even in incremental mode (may print 'unknown's at times) **interactivePrompt**- (bool, default = true)
**This internal Boolean flag is undocumented; however, its alternate option --no-interactive-prompt, which reverses the sense of the option, is documented thusly:**turn off interactive prompting while in interactive mode **continuedExecution**- (bool, default = false)

continue executing commands, even on error **segvSpin**- (bool, default = false)

spin on segfault/other crash waiting for gdb **tearDownIncremental**- (bool, default = false)

implement PUSH/POP/multi-query by destroying and recreating SmtEngine (EXPERTS only) **waitToJoin**- (bool, default = true)

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

memory map file input **semanticChecks**- (bool, default = DO_SEMANTIC_CHECKS_BY_DEFAULT)
**This internal Boolean flag is undocumented; however, its alternate option --no-checking, which reverses the sense of the option, is documented thusly:**disable ALL semantic checks, including type checks **filesystemAccess**- (bool, default = true)

[undocumented] *IDL OPTIONS***idlRewriteEq**- (bool, default = false)

enable rewriting equalities into two inequalities in IDL solver (default is disabled) *SETS OPTIONS***setsPropagate**- (bool, default = true)

determines whether to propagate learnt facts to Theory Engine / SAT solver **setsEagerLemmas**- (bool, default = true)

add lemmas even at regular effort

## Version

This manual page refers to **CVC4** version 1.4.

## Bugs

A Bugzilla for the CVC4 project is maintained at http://cvc4.cs.nyu.edu/bugzilla3/.

## Authors

**CVC4** is developed by a team of researchers at New York 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.nyu.edu/wiki/.