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