# 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**version**(bool)

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

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

be less tolerant of non-conforming inputs**dumpModeString**(std::string)

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

all dumping goes to FILE (instead of stdout)**produceModels**(bool, default = false)

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

keep an assertions list (enables get-assertions command)**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**hardLimit**(bool, default = false)

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

measures CPU time if set to true and wall time if false (default false)*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)

turns on 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 outputting 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**sNormInferEq**(bool, default = false)

infer equalities based on Shostak normalization**nlExt**(bool, default = true)

extended approach to non-linear**nlExtResBound**(bool, default = false)

use resolution-style inference for inferring new bounds**nlExtTangentPlanes**(bool, default = false)

use non-terminating tangent plane strategy for non-linear**nlExtEntailConflicts**(bool, default = false)

check for entailed conflicts in non-linear solver**nlExtRewrites**(bool, default = true)

do rewrites in non-linear solver**nlExtSolveSubs**(bool, default = false)

do solving for determining constant substitutions**nlExtPurify**(bool, default = false)

purify non-linear terms at preprocess**nlExtSplitZero**(bool, default = false)

intial splits on zero for all variables*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)**arraysWeakEquivalence**(bool, default = false)

use algorithm from Christ/Hoenicke (SMT 2014)**arraysModelBased**(bool, default = false)

turn on model-based array 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**arraysConfig**(int, default = 0)

set different array option configurations - for developers only**arraysReduceSharing**(bool, default = false)

use model information to reduce size of care graph for arrays**arraysPropagate**(int, default = 2)

propagation effort for arrays: 0 is none, 1 is some, 2 is full*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*BITVECTOR THEORY OPTIONS***bvSatSolver**(CVC4::theory::bv::SatSolverMode, default = CVC4::theory::bv::SAT_SOLVER_MINISAT)

choose which sat solver to use, see --bv-sat-solver=help (EXPERTS only)**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 (implies --bitblast=eager)**bitvectorAigSimplifications**(std::string)

abc command to run AIG simplifications (implies --bitblast-aig, default is "balance;drw") (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**boolToBitvector**(bool, default = false)

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

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

enable rewrite pushing extract [i:0] over arithmetic operations (can blow up) (EXPERTS only)**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)**bvLazyRewriteExtf**(bool, default = true)

lazily rewrite extended functions like bv2nat and int2bv**bvLazyReduceExtf**(bool, default = false)

reduce extended functions like bv2nat and int2bv at last call instead of full effort**bvAlgExtf**(bool, default = true)

algebraic inferences for extended functions*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**dtBinarySplit**(bool, default = false)

do binary splits for datatype constructor types**dtRefIntro**(bool, default = false)

introduce reference skolems for shorter explanations**dtUseTesters**(bool, default = true)

do not preprocess away tester predicates**cdtBisimilar**(bool, default = true)

do bisimilarity check for co-datatypes**dtCyclic**(bool, default = true)

do cyclicity check for datatypes**dtInferAsLemmas**(bool, default = false)

always send lemmas out instead of making internal inferences**dtBlastSplits**(bool, default = false)

when applicable, blast splitting lemmas for all variables at once*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)*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)**printExprTypes**(bool, default = false)

print types with variables when printing exprs**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)

never type check expressions*IDL OPTIONS***idlRewriteEq**(bool, default = false)

enable rewriting equalities into two inequalities in IDL solver (default is disabled)*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)**interactive**(bool)

force interactive/non-interactive mode**interactivePrompt**(bool, default = true)

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**(int, default = 0)

implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N queries (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)

disable ALL semantic checks, including type checks**globalDeclarations**(bool, default = false)

force all declarations and definitions to be global**filesystemAccess**(bool, default = true)

[undocumented]*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*PROOF OPTIONS***lfscLetification**(bool, default = true)

turns on global letification in LFSC proofs**aggressiveCoreMin**(bool, default = false)

turns on aggressive unsat core minimization (experimental)**fewerPreprocessingHoles**(bool, default = false)

try to eliminate preprocessing holes in proofs**allowEmptyDependencies**(bool, default = false)

if unable to track the dependencies of a rewritten/preprocessed assertion, fail silently*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*QUANTIFIERS OPTIONS***miniscopeQuant**(bool, default = true)

miniscope quantifiers**miniscopeQuantFreeVar**(bool, default = true)

miniscope quantifiers for ground subformulas**quantSplit**(bool, default = true)

apply splitting to quantified formulas based on variable disjoint disjuncts**prenexQuant**(CVC4::theory::quantifiers::PrenexQuantMode, default = CVC4::theory::quantifiers::PRENEX_QUANT_SIMPLE)

prenex mode for quantified formulas**prenexQuantUser**(bool, default = false)

prenex quantified formulas with user patterns**varElimQuant**(bool, default = true)

enable simple variable elimination for quantified formulas**varIneqElimQuant**(bool, default = true)

enable variable elimination based on infinite projection of unbound arithmetic variables**dtVarExpandQuant**(bool, default = true)

expand datatype variables bound to one constructor in quantifiers**iteLiftQuant**(CVC4::theory::quantifiers::IteLiftQuantMode, default = CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE)

ite lifting mode for quantified formulas**condVarSplitQuant**(bool, default = true)

split quantified formulas that lead to variable eliminations**condVarSplitQuantAgg**(bool, default = false)

aggressive split quantified formulas that lead to variable eliminations**iteDtTesterSplitQuant**(bool, default = false)

split ites with dt testers as conditions**preSkolemQuant**(bool, default = false)

apply skolemization eagerly to bodies of quantified formulas**preSkolemQuantNested**(bool, default = true)

apply skolemization to nested quantified formulas**preSkolemQuantAgg**(bool, default = true)

apply skolemization to quantified formulas aggressively**aggressiveMiniscopeQuant**(bool, default = false)

perform aggressive miniscoping for quantifiers**elimTautQuant**(bool, default = true)

eliminate tautological disjuncts of quantified formulas**elimExtArithQuant**(bool, default = true)

eliminate extended arithmetic symbols in quantified formulas**condRewriteQuant**(bool, default = true)

conditional rewriting of quantified formulas**eMatching**(bool, default = true)

whether to do heuristic E-matching**termDbMode**(CVC4::theory::quantifiers::TermDbMode, default = CVC4::theory::quantifiers::TERM_DB_ALL)

which ground terms to consider for instantiation**registerQuantBodyTerms**(bool, default = false)

consider ground terms within bodies of quantified formulas for matching**inferArithTriggerEq**(bool, default = false)

infer equalities for trigger terms based on solving arithmetic equalities**inferArithTriggerEqExp**(bool, default = false)

record explanations for inferArithTriggerEq**strictTriggers**(bool, default = false)

only instantiate quantifiers with user patterns based on 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)**purifyTriggers**(bool, default = false)

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

purify dt triggers, match all constructors of correct form instead of selectors**pureThTriggers**(bool, default = false)

use pure theory terms as single triggers**partialTriggers**(bool, default = false)

use triggers that do not contain all free variables**multiTriggerWhenSingle**(bool, default = false)

select multi triggers when single triggers exist**multiTriggerPriority**(bool, default = false)

only try multi triggers if single triggers give no instantiations**multiTriggerCache**(bool, default = false)

caching version of multi triggers**multiTriggerLinear**(bool, default = true)

implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms**triggerSelMode**(CVC4::theory::quantifiers::TriggerSelMode, default = CVC4::theory::quantifiers::TRIGGER_SEL_MIN)

selection mode for triggers**triggerActiveSelMode**(CVC4::theory::quantifiers::TriggerActiveSelMode, default = CVC4::theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL)

selection mode to activate triggers**userPatternsQuant**(CVC4::theory::quantifiers::UserPatMode, default = CVC4::theory::quantifiers::USER_PAT_MODE_TRUST)

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

generate additional triggers as needed during search**instWhenMode**(CVC4::theory::quantifiers::InstWhenMode, default = CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL)

when to apply instantiation**instWhenStrictInterleave**(bool, default = true)

ensure theory combination and standard quantifier effort strategies take turns**instWhenPhase**(int, default = 2)

instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen**instWhenTcFirst**(bool, default = true)

allow theory combination to happen once initially, before quantifier strategies are run**quantModelEe**(bool, default = false)

use equality engine of model for last call effort**instMaxLevel**(int, default = -1)

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

only input terms are assigned instantiation level zero**quantRepMode**(CVC4::theory::quantifiers::QuantRepMode, default = CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST)

selection mode for representatives in quantifiers engine**instRelevantCond**(bool, default = false)

add relevancy conditions for instantiations**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**fullSaturateQuantRd**(bool, default = true)

whether to use relevant domain first for full saturation instantiation strategy**fullSaturateInst**(bool, default = false)

interleave full saturate instantiation with other techniques**literalMatchMode**(CVC4::theory::quantifiers::LiteralMatchMode, default = CVC4::theory::quantifiers::LITERAL_MATCH_USE)

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

use finite model finding heuristic for quantifier instantiation**quantFunWellDefined**(bool, default = false)

assume that function defined by quantifiers are well defined**fmfFunWellDefined**(bool, default = false)

find models for recursively defined functions, assumes functions are admissible**fmfFunWellDefinedRelevant**(bool, default = false)

find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant**fmfEmptySorts**(bool, default = false)

allow finite model finding to assume sorts that do not occur in ground assertions are empty**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)

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

simple models in full model check for finite model finding**fmfBoundInt**(bool, default = false)

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

finite model finding on bounded quantification**fmfBoundLazy**(bool, default = false)

enforce bounds for bounded quantification lazily via use of proxy variables**fmfBoundMinMode**(CVC4::theory::quantifiers::FmfBoundMinMode, default = CVC4::theory::quantifiers::FMF_BOUND_MIN_INT_RANGE)

mode for which types of bounds to minimize via first decision heuristics**quantConflictFind**(bool, default = true)

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**qcfAllConflict**(bool, default = false)

add all available conflicting instances during conflict-based instantiation**qcfNestedConflict**(bool, default = false)

consider conflicts for nested quantifiers**qcfVoExp**(bool, default = false)

qcf experimental variable ordering**instNoEntail**(bool, default = true)

do not consider instances of quantified formulas that are currently entailed**instNoModelTrue**(bool, default = false)

do not consider instances of quantified formulas that are currently true in model, if it is available**instPropagate**(bool, default = false)

internal propagation for instantiations for selecting relevant instances**qcfEagerTest**(bool, default = true)

optimization, test qcf instances eagerly**qcfEagerCheckRd**(bool, default = true)

optimization, eagerly check relevant domain of matched position**qcfSkipRd**(bool, default = false)

optimization, skip instances based on possibly irrelevant portions of quantified formulas**quantRewriteRules**(bool, default = false)

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

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

use all available techniques for inductive reasoning**dtStcInduction**(bool, default = false)

apply strengthening for existential quantification over datatypes based on structural induction**intWfInduction**(bool, default = false)

apply strengthening for integers based on well-founded induction**conjectureGen**(bool, default = false)

generate candidate conjectures for inductive proofs**conjectureGenPerRound**(int, default = 1)

number of conjectures to generate per instantiation round**conjectureNoFilter**(bool, default = false)

do not filter conjectures**conjectureFilterActiveTerms**(bool, default = true)

filter based on active terms**conjectureFilterCanonical**(bool, default = true)

filter based on canonicity**conjectureFilterModel**(bool, default = true)

filter based on model**conjectureGenGtEnum**(int, default = 50)

number of ground terms to generate for model filtering**conjectureUeeIntro**(bool, default = false)

more aggressive merging for universal equality engine, introduces terms**conjectureGenMaxDepth**(int, default = 3)

maximum depth of terms to consider for conjectures**ceGuidedInst**(bool, default = false)

counterexample-guided quantifier instantiation**ceGuidedInstFair**(CVC4::theory::quantifiers::CegqiFairMode, default = CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE)

if and how to apply fairness for cegqi**cegqiSingleInvMode**(CVC4::theory::quantifiers::CegqiSingleInvMode, default = CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE)

mode for processing single invocation synthesis conjectures**cegqiSingleInvPartial**(bool, default = false)

combined techniques for synthesis conjectures that are partially single invocation**cegqiSingleInvReconstruct**(bool, default = true)

reconstruct solutions for single invocation conjectures in original grammar**cegqiSolMinCore**(bool, default = false)

minimize solutions for single invocation conjectures based on unsat core**cegqiSolMinInst**(bool, default = true)

minimize individual instantiations for single invocation conjectures based on unsat core**cegqiSingleInvReconstructConst**(bool, default = true)

include constants when reconstruct solutions for single invocation conjectures in original grammar**cegqiSingleInvAbort**(bool, default = false)

abort if synthesis conjecture is not single invocation**sygusNormalForm**(bool, default = true)

only search for sygus builtin terms that are in normal form**sygusNormalFormArg**(bool, default = true)

account for relationship between arguments of operations in sygus normal form**sygusNormalFormGlobal**(bool, default = true)

narrow sygus search space based on global state of current candidate program**sygusNormalFormGlobalGen**(bool, default = true)

generalize lemmas for global search space narrowing**sygusNormalFormGlobalArg**(bool, default = true)

generalize based on arguments in global search space narrowing**sygusNormalFormGlobalContent**(bool, default = true)

generalize based on content in global search space narrowing**sygusInvTemplMode**(CVC4::theory::quantifiers::SygusInvTemplMode, default = CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE)

template mode for sygus invariant synthesis**sygusUnifCondSol**(bool, default = false)

enable approach which unifies conditional solutions**sygusDirectEval**(bool, default = true)

direct unfolding of evaluation functions**sygusCRefEval**(bool, default = false)

direct evaluation of refinement lemmas for conflict analysis**cbqi**(bool, default = false)

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

turns on recursive counterexample-based quantifier instantiation**cbqiSat**(bool, default = true)

answer sat when quantifiers are asserted with counterexample-based quantifier instantiation**cbqiModel**(bool, default = true)

guide instantiations by model values for counterexample-based quantifier instantiation**cbqiAll**(bool, default = false)

apply counterexample-based instantiation to all quantified formulas**cbqiUseInfInt**(bool, default = false)

use integer infinity for vts in counterexample-based quantifier instantiation**cbqiUseInfReal**(bool, default = false)

use real infinity for vts in counterexample-based quantifier instantiation**cbqiPreRegInst**(bool, default = false)

preregister ground instantiations in counterexample-based quantifier instantiation**cbqiMinBounds**(bool, default = false)

use minimally constrained lower/upper bound for counterexample-based quantifier instantiation**cbqiRoundUpLowerLia**(bool, default = false)

round up integer lower bounds in substitutions for counterexample-based quantifier instantiation**cbqiMidpoint**(bool, default = false)

choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation**cbqiNopt**(bool, default = true)

non-optimal bounds for counterexample-based quantifier instantiation**cbqiLitDepend**(bool, default = true)

dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation**cbqiInnermost**(bool, default = true)

only process innermost quantified formulas in counterexample-based quantifier instantiation**cbqiNestedQE**(bool, default = false)

process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation**quantEpr**(bool, default = false)

infer whether in effectively propositional fragment, use for cbqi**quantEprMatching**(bool, default = true)

use matching heuristics for EPR instantiation**localTheoryExt**(bool, default = false)

do instantiation based on local theory extensions**ltePartialInst**(bool, default = false)

partially instantiate local theory quantifiers**lteRestrictInstClosure**(bool, default = false)

treat arguments of inst closure as restricted terms for instantiation**quantAlphaEquiv**(bool, default = true)

infer alpha equivalence between quantified formulas**macrosQuant**(bool, default = false)

perform quantifiers macro expansion**macrosQuantMode**(CVC4::theory::quantifiers::MacrosQuantMode, default = CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF)

mode for quantifiers macro expansion**quantDynamicSplit**(CVC4::theory::quantifiers::QuantDSplitMode, default = CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE)

mode for dynamic quantifiers splitting**quantAntiSkolem**(bool, default = false)

perform anti-skolemization for quantified formulas**quantEqualityEngine**(bool, default = false)

maintain congrunce closure over universal equalities**trackInstLemmas**(bool, default = false)

track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)*SEP OPTIONS***sepCheckNeg**(bool, default = true)

check negated spatial assertions**sepExp**(bool, default = false)

experimental flag for sep**sepMinimalRefine**(bool, default = false)

only add refinement lemmas for minimal (innermost) assertions**sepDisequalC**(bool, default = true)

assume cardinality elements are distinct**sepPreSkolemEmp**(bool, default = false)

eliminate emp constraint at preprocess time**sepChildRefine**(bool, default = false)

child-specific refinements of negated star, positive wand*SETS OPTIONS***setsProxyLemmas**(bool, default = false)

introduce proxy variables eagerly to shorten lemmas**setsInferAsLemmas**(bool, default = true)

send inferences as lemmas**setsRelEager**(bool, default = true)

standard effort checks for relations**setsExt**(bool, default = false)

enable extended symbols such as complement and universe in theory of sets*SMT LAYER OPTIONS***forceLogicString**(std::string)

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**omitDontCares**(bool, default = false)

When producing a model, omit variables whose value does not matter**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**dumpSynth**(bool, default = false)

output solution for synthesis conjectures after every UNSAT/VALID response**unsatCores**(bool)

turn on unsat core generation**checkUnsatCores**(bool)

after UNSAT/VALID, produce and check an unsat core (expensive)**dumpUnsatCores**(bool, default = false)

output unsat cores after every UNSAT/VALID response**dumpUnsatCoresFull**(bool, default = false)

dump the full unsat core, including unlabeled assertions**produceAssignments**(bool, default = false)

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

deprecated name for produce-assertions**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**regularChannelName**(std::string)

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

set the diagnostic output channel of the solver**rewriteStep**(unsigned, default = 1)

amount of resources spent for each rewrite step (EXPERTS only)**theoryCheckStep**(unsigned, default = 1)

amount of resources spent for each theory check call (EXPERTS only)**decisionStep**(unsigned, default = 1)

amount of getNext decision calls in the decision engine (EXPERTS only)**bitblastStep**(unsigned, default = 1)

amount of resources spent for each bitblast step (EXPERTS only)**parseStep**(unsigned, default = 1)

amount of resources spent for each command/expression parsing (EXPERTS only)**lemmaStep**(unsigned, default = 1)

amount of resources spent when adding lemmas (EXPERTS only)**restartStep**(unsigned, default = 1)

amount of resources spent for each theory restart (EXPERTS only)**cnfStep**(unsigned, default = 1)

amount of resources spent for each call to cnf conversion (EXPERTS only)**preprocessStep**(unsigned, default = 1)

amount of resources spent for each preprocessing step in SmtEngine (EXPERTS only)**quantifierStep**(unsigned, default = 1)

amount of resources spent for quantifier instantiations (EXPERTS only)**satConflictStep**(unsigned, default = 1)

amount of resources spent for each sat conflict (main sat solver) (EXPERTS only)**bvSatConflictStep**(unsigned, default = 1)

amount of resources spent for each sat conflict (bitvectors) (EXPERTS only)**rewriteApplyToConst**(bool, default = false)

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

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

replay decisions from file**forceNoLimitCpuWhileDump**(bool, default = false)

Force no CPU limit when dumping models and proofs**solveIntAsBV**(uint32_t, default = 0)

attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)**solveRealAsInt**(bool, default = false)

attempt to solve a pure real satisfiable problem as a integer problem (for non-linear)*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**stdASCII**(bool, default = true)

the alphabet contains only characters from the standard ASCII or the extended one**stringFMF**(bool, default = false)

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

strings eager check**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**stringIgnNegMembership**(bool, default = false)

internal for strings: ignore negative membership constraints (fragment checking is needed, left to users for now)**stringLazyPreproc**(bool, default = true)

perform string preprocessing lazily**stringLenGeqZ**(bool, default = false)

strings length greater than zero lemmas**stringLenNorm**(bool, default = true)

strings length normalization lemma**stringSplitEmp**(bool, default = true)

strings split on empty string**stringInferSym**(bool, default = true)

strings split on empty string**stringEagerLen**(bool, default = true)

strings eager length lemmas**stringCheckEntailLen**(bool, default = true)

check entailment between length terms to reduce splitting**stringProcessLoop**(bool, default = true)

reduce looping word equations to regular expressions**stringAbortLoop**(bool, default = false)

abort when a looping word equation is encountered**stringInferAsLemmas**(bool, default = false)

always send lemmas out instead of making internal inferences**stringRExplainLemmas**(bool, default = true)

regression explanations for string lemmas**stringMinPrefixExplain**(bool, default = true)

minimize explanations for prefix of normal forms in strings**stringGuessModel**(bool, default = false)

use model guessing to avoid string extended function reductions**stringUfReduct**(bool, default = false)

use uninterpreted functions when applying extended function reductions**stringBinaryCsp**(bool, default = false)

use binary search when splitting strings**stringLenPropCsp**(bool, default = false)

do length propagation based on constant splits*THEORY LAYER OPTIONS***theoryOfMode**(CVC4::theory::TheoryOfMode, default = CVC4::theory::THEORY_OF_TYPE_BASED)

mode for Theory::theoryof() (EXPERTS only)**useTheoryList**(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***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)

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**ufssMode**(CVC4::theory::uf::UfssMode, default = CVC4::theory::uf::UF_SS_FULL)

mode of operation for 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 = true)

use fair strategy for finite model finding multiple sorts**ufssFairnessMonotone**(bool, default = false)

group monotone sorts when enforcing fairness for finite model finding

## Version

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

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