Options
cvc5 can be configured at runtime using a wide range of options. When cvc5 is used as a binary, options can be set on the command line. Also, options can be set and inspected using the respective commands of the input language and the corresponding API functions:

C++ API:
setOption()
,getOption()
,getOptionNames()
,getOptionInfo()

Java API:
setOption()
,getOption()
,getOptionNames()
,getOptionInfo()

Base Python API:
setOption()
,getOption()
,getOptionNames()
,getOptionInfo()

Pythonic API:
setOption()
,getOption()
,getOptionNames()
,getOptionInfo()
Generally, all options are identified by a name
<name>
, and (optionally)
by a short name
<short>
(a single letter).
Additionally, they can have one or more aliases, which can be used instead of
<name>
.
Internally , options are strongly typed and must be either Boolean, (signed or unsigned) integers, floatingpoint numbers, strings, or an enumeration type. Values for options with a numeric type may be restricted to an interval.
Some options have custom types (e.g., err ) which require special treatment internally. The usage of such options is documented as part of the documentation for the corresponding options.
On the command line, a
Boolean
option can be set to
true
via
<name>
or
<short>
.
Most Boolean options can also be set to
false
via
no<name>
.
In cvc5’s APIs, this is done via
setOption("<name>",
"true"

"false")
.
For
all other types
, values are given on the command line using
<name>=<value>
or
<name>
<value>
,
and
setOption("<name>",
"<value>")
in the APIs.
The given value must be convertible to the appropriate type, in particular for
numeric and enumeration types.
Below is an exhaustive list of options supported by cvc5.
Most CommonlyUsed cvc5 Options

i  incremental
[typebool
, defaulttrue
] (alsono*
) 
enable incremental solving

L  lang  inputlanguage
[customLanguage
, defaultLanguage::LANG_AUTO
] 
force input language (default is “auto”; see –lang help)

o  output
[none  inst  oracles  sygus  sygusgrammar  sygusenumerator  sygussolgterm  trigger  rawbenchmark  learnedlits  subs  postasserts  preasserts  deeprestart  incomplete  lemmas  trustedproofsteps  timeoutcorebenchmark  unsatcorebenchmark  portfolio  blockmodel
, defaultnone
] 
Enable output tag.
Output tags.

inst
: 
print instantiations during solving

oracles
: 
print calls to oracles and responses received

sygus
: 
print enumerated terms and candidates generated by the sygus solver

sygusgrammar
: 
print grammars automatically generated by the sygus solver

sygusenumerator
: 
print enumerators generated by the sygus solver

sygussolgterm
: 
print annotations for terms in sygus solutions that indicate the grammar used to generate them

trigger
: 
print selected triggers for quantified formulas

rawbenchmark
: 
print the benchmark back on the output verbatim as it is processed

learnedlits
: 
print input literals that hold globally

subs
: 
print toplevel substitutions learned during preprocessing

postasserts
: 
print a benchmark corresponding to the assertions of the input problem after preprocessing

preasserts
: 
print a benchmark corresponding to the assertions of the input problem before preprocessing

deeprestart
: 
print when cvc5 performs a deep restart along with the literals it has learned

incomplete
: 
print reason why cvc5 answers unknown for any given checksat query

lemmas
: 
print lemmas as they are added to the SAT solver

trustedproofsteps
: 
print formulas corresponding to trusted proof steps in final proofs

timeoutcorebenchmark
: 
print the corresponding benchmark when successfully computing a timeout core.

unsatcorebenchmark
: 
print the corresponding benchmark when successfully computing an unsat core.

portfolio
: 
prints the option strings tried in portfolio mode.

blockmodel
: 
prints the formulas used when blockmodel is run.


parseonly
[typebool
, defaultfalse
] (alsono*
) 
exit after parsing input

preprocessonly
[typebool
, defaultfalse
] (alsono*
) 
exit after preprocessing input

q  quiet
[typebool
] 
decrease verbosity (may be repeated)

rlimit
[typeuint64_t
, default0
] 
set resource limit

rlimitper  reproducibleresourcelimit
[typeuint64_t
, default0
] 
set resource limit per query

safeoptions
[typebool
, defaultfalse
] (alsono*
) 
do not allow setting any option that is not common or regular

stats
[typebool
, defaultfalse
] (alsono*
) 
give statistics on exit

tlimit
[typeuint64_t
, default0
] 
set time limit in milliseconds of wall clock time

tlimitper
[typeuint64_t
, default0
] 
set time limit per query in milliseconds

v  verbose
[typebool
] 
increase verbosity (may be repeated)

verbosity
[typeint64_t
, default0
] 
the verbosity level of cvc5

copyright
[typebool
, defaultfalse
] 
show cvc5 copyright information

h  help
[typebool
, defaultfalse
] 
full command line reference

H  helpregular
[typebool
, defaultfalse
] 
regular command line reference

interactive
[typebool
, defaultfalse
] (alsono*
) 
force interactive shell/noninteractive mode

printsuccess
[typebool
, defaultfalse
] (alsono*
) 
print the “success” output required of SMTLIBv2

s  seed
[typeuint64_t
, default0
] 
seed for random number generator

showconfig
[typebool
, defaultfalse
] 
show cvc5 static configuration

V  version
[typebool
, defaultfalse
] 
identify this cvc5 binary

forcelogic
[typestring
, default""
] 
set the logic, and override all further user attempts to change it

strictparsing
[typebool
, defaultfalse
] (alsono*
) 
be less tolerant of nonconforming inputs

dagthresh
[typeint64_t
,0 <= N
, default1
] 
dagify common subexprs appearing > N times (1 == default, 0 == don’t dagify)

outputlang  outputlanguage
[customLanguage
, defaultLanguage::LANG_AUTO
] 
force output language (default is “auto”; see –outputlang help)

printinst
[list  num
, defaultlist
] 
print format for printing instantiations
Print format for printing instantiations.

list
: 
Print the list of instantiations per quantified formula, when nonempty.

num
: 
Print the total number of instantiations per quantified formula, when nonzero.


checkmodels
[typebool
, defaultfalse
] (alsono*
) 
after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions

m  producemodels
[typebool
, defaultfalse
] (alsono*
) 
support the getvalue and getmodel commands
Additional cvc5 Options
Arithmetic Theory Module

approxbranchdepth
[typeint64_t
, default200
] 
[experts only]
maximum branch depth the approximate solver is allowed to take

arithbrab
[typebool
, defaulttrue
] (alsono*
) 
whether to use simple rounding, similar to a unitcube test, for integers

aritheqsolver
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
whether to use the equality solver in the theory of arithmetic

arithnopartialfun
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
do not use partial function semantics for arithmetic (not SMT LIB compliant)

arithprop
[none  unate  bi  both
, defaultboth
] 
[experts only]
turns on arithmetic propagation (default is ‘old’, see –arithprop=help)
This decides on kind of propagation arithmetic attempts to do during the search.

unate
: 
Use constraints to do unate propagation.

bi
: 
(Bounds Inference) infers bounds on basic variables using the upper and lower bounds of the nonbasic variables in the tableau.

both
: 
Use bounds inference and unate.


arithpropclauses
[typeuint64_t
, default8
] 
[experts only]
rows shorter than this are propagated as clauses

arithrewriteequalities
[typebool
, defaultfalse
] (alsono*
) 
turns on the preprocessing rewrite turning equalities into a conjunction of inequalities

arithstaticlearning
[typebool
, defaulttrue
] (alsono*
) 
do arithmetic static learning for ite terms based on bounds when static learning is enabled

collectpivotstats
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
collect the pivot history

cutallbounded
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds

diodecomps
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
let skolem variables for integer divisibility constraints leak from the dio solver

diosolver
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)

dioturns
[typeint64_t
, default10
] 
[experts only]
turns in a row dio solver cutting gets

errorselectionrule
[min  varord  max  sum
, defaultmin
] 
[experts only]
change the pivot rule for the basic variable (default is ‘min’, see –pivotrule help)
This decides on the rule used by simplex during heuristic rounds for deciding the next basic variable to select.

min
: 
The minimum abs() value of the variable’s violation of its bound.

varord
: 
The variable order.

max
: 
The maximum violation the bound.


fcpenalties
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
turns on degenerate pivot penalties

heuristicpivots
[typeint64_t
, default0
] 
[experts only]
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

lemmasonreplayfailure
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
attempt to use external lemmas if approximate solve integer failed

maxCutsInContext
[typeuint64_t
, default65535
] 
[experts only]
maximum cuts in a given context before signalling a restart

miplibtrick
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
turns on the preprocessing step of attempting to infer bounds on miplib problems

miplibtricksubs
[typeuint64_t
, default1
] 
[experts only]
do substitution for miplib ‘tmp’ vars if defined in <= N eliminated vars

newprop
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
use the new row propagation system

nlcov
[typebool
, defaultfalse
] (alsono*
) 
whether to use the cylindrical algebraic coverings solver for nonlinear arithmetic

nlcovforce
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
forces using the cylindrical algebraic coverings solver, even in cases where it is possibly not safe to do so

nlcovlift
[regular  lazard
, defaultregular
] 
[experts only]
choose the Coverings lifting mode
Modes for the Coverings lifting in nonlinear arithmetic.

regular
: 
Regular lifting.

lazard
: 
Lazard’s lifting scheme.


nlcovlinearmodel
[none  initial  persistent
, defaultnone
] 
whether to use the linear model as initial guess for the cylindrical algebraic coverings solver
Modes for the usage of the linear model in nonlinear arithmetic.

none
: 
Do not use linear model to seed nonlinear model

initial
: 
Use linear model to seed nonlinear model initially, discard it when it does not work

persistent
: 
Use linear model to seed nonlinear model whenever possible


nlcovproj
[mccallum  lazard  lazardmod
, defaultmccallum
] 
[experts only]
choose the Coverings projection operator
Modes for the Coverings projection operator in nonlinear arithmetic.

mccallum
: 
McCallum’s projection operator.

lazard
: 
Lazard’s projection operator.

lazardmod
: 
A modification of Lazard’s projection operator.


nlcovprune
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
whether to prune intervals more agressively

nlcovvarelim
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
whether to eliminate variables using equalities before going into the cylindrical algebraic coverings solver. It can not be used when producing proofs right now.

nlext
[none  light  full
, defaultfull
] 
incremental linearization approach to nonlinear
Modes for the nonlinear linearization

none
: 
Disable linearization approach

light
: 
Only use a few lightweight lemma schemes

full
: 
Use all lemma schemes


nlextentconf
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
check for entailed conflicts in nonlinear solver

nlextfactor
[typebool
, defaulttrue
] (alsono*
) 
use factoring inference in nonlinear incremental linearization solver

nlextincprec
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
whether to increment the precision for irrational function constraints

nlextpurify
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
purify nonlinear terms at preprocess

nlextrbound
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use resolutionstyle inference for inferring new bounds in nonlinear incremental linearization solver

nlextrewrite
[typebool
, defaulttrue
] (alsono*
) 
do contextdependent simplification based on rewrites in nonlinear solver

nlextsplitzero
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
initial splits on zero for all variables

nlexttftaylordeg
[typeint64_t
, default4
] 
[experts only]
initial degree of polynomials for Taylor approximation

nlexttftplanes
[typebool
, defaulttrue
] (alsono*
) 
use nonterminating tangent plane strategy for transcendental functions for nonlinear incremental linearization solver

nlexttplanes
[typebool
, defaulttrue
] (alsono*
) 
use nonterminating tangent plane strategy for nonlinear incremental linearization solver

nlexttplanesinterleave
[typebool
, defaultfalse
] (alsono*
) 
interleave tangent plane strategy for nonlinear incremental linearization solver

nlicp
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
whether to use ICPstyle propagations for nonlinear arithmetic

nlrlv
[none  interleave  always
, defaultnone
] 
[experts only]
choose mode for using relevance of assertions in nonlinear arithmetic
Modes for using relevance of assertions in nonlinear arithmetic.

none
: 
Do not use relevance.

interleave
: 
Alternate rounds using relevance.

always
: 
Always use relevance.


nlrlvassertbounds
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use bound inference utility to prune when an assertion is entailed by another

pbrewrites
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
apply pseudo boolean rewrites

pivotthreshold
[typeuint64_t
, default2
] 
[experts only]
sets the number of pivots using –pivotrule per basic variable per simplex instance before using variable order

ppassertmaxsubsize
[typeuint64_t
, default2
] 
[experts only]
threshold for substituting an equality in ppAssert

proprowlength
[typeuint64_t
, default16
] 
[experts only]
sets the maximum row length to be used in propagation

replayearlyclosedepth
[typeint64_t
, default1
] 
[experts only]
multiples of the depths to try to close the approx log eagerly

replaylemmarejectcut
[typeuint64_t
, default25500
] 
[experts only]
maximum complexity of any coefficient while outputting replaying cut lemmas

replaynumerrpenalty
[typeint64_t
, default4194304
] 
[experts only]
number of solve integer attempts to skips after a numeric failure

replayrejectcut
[typeuint64_t
, default25500
] 
[experts only]
maximum complexity of any coefficient while replaying cuts

restrictpivots
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
have a pivot cap for simplex at effort levels below fullEffort

revertarithmodelsonunsat
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
revert the arithmetic model to a known safe model on unsat if one is cached

rrturns
[typeint64_t
, default3
] 
[experts only]
round robin turn

sesolveint
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
attempt to use the approximate solve integer method on standard effort

simplexcheckperiod
[typeuint64_t
, default200
] 
[experts only]
the number of pivots to do in simplex before rechecking for a conflict on all variables

soiqe
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use quick explain to minimize the sum of infeasibility conflicts

standardeffortvariableorderpivots
[typeint64_t
, default1
] 
[experts only]
limits the number of pivots in a single invocation of check() at a nonfull effort level using Bland’s pivot rule

unatelemmas
[all  eqs  ineqs  none
, defaultall
] 
[experts only]
determines which lemmas to add before solving (default is ‘all’, see –unatelemmas=help)
Unate lemmas are generated before SAT search begins using the relationship of constant terms and polynomials.

all
: 
A combination of inequalities and equalities.

eqs
: 
Outputs lemmas of the general forms (= p c) implies (<= p d) for c < d, or (= p c) implies (not (= p d)) for c != d.

ineqs
: 
Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.

none
: 
Do not add unate lemmas.


useapprox
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
attempt to use an approximate solver

usefcsimplex
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use focusing and converging simplex (FMCAD 2013 submission)

usesoi
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use sum of infeasibility simplex (FMCAD 2013 submission)
Arrays Theory Module

arrayseagerindex
[typebool
, defaulttrue
] (alsono*
) 
turn on eager index splitting for generated array lemmas

arrayseagerlemmas
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
turn on eager lemma generation for arrays

arraysexp
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
enable experimental features in the theory of arrays

arraysoptimizelinear
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper)

arraysprop
[typeint64_t
, default2
] 
[experts only]
propagation effort for arrays: 0 is none, 1 is some, 2 is full

arraysreducesharing
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use model information to reduce size of care graph for arrays

arraysweakequiv
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use algorithm from Christ/Hoenicke (SMT 2014)
Base Module

err  diagnosticoutputchannel
[customManagedErr
, default{}
] 
[experts only]
Set the error (or diagnostic) output channel. Writes to stderr for “stderr” or “–”, stdout for “stdout” or the given filename otherwise.

in
[customManagedIn
, default{}
] 
[experts only]
Set the error (or diagnostic) output channel. Reads from stdin for “stdin” or “–” and the given filename otherwise.

out  regularoutputchannel
[customManagedOut
, default{}
] 
[experts only]
Set the error (or diagnostic) output channel. Writes to stdout for “stdout” or “–”, stderr for “stderr” or the given filename otherwise.

rweight
[typestring
] 
[experts only]
set a single resource weight

statsall
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
print unchanged (defaulted) statistics as well

statseveryquery
[typebool
, defaultfalse
] (alsono*
) 
in incremental mode, print stats after every satisfiability or validity query

statsinternal
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
print internal (nonpublic) statistics as well

t  trace
[typestring
] 
trace something (e.g. t pushpop), can repeat and may contain wildcards like (e.g. t theory::*)
Bitvector Theory Module

bitblast
[lazy  eager
, defaultlazy
] 
choose bitblasting mode, see –bitblast=help
Bitblasting modes.

lazy
: 
Separate Boolean structure and term reasoning between the core SAT solver and the bitvector SAT solver.

eager
: 
Bitblast eagerly to bitvector SAT solver.


bitwiseeq
[typebool
, defaulttrue
] (alsono*
) 
lift equivalence with onebit bitvectors to be boolean operations

booltobv
[off  ite  all
, defaultoff
] 
convert booleans to bitvectors of size 1 at various levels of aggressiveness, see –booltobv=help
BoolToBV preprocessing pass modes.

off
: 
Don’t push any booleans to width one bitvectors.

ite
: 
Try to turn ITEs into BITVECTOR_ITE when possible. It can fail performula if not all subformulas can be turned to bitvectors.

all
: 
Force all booleans to be bitvectors of width one except at the top level. Most aggressive mode.


bvassertinput
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
assert input assertions on userlevel 0 instead of assuming them in the bitvector SAT solver

bveagereval
[typebool
, defaultfalse
] (alsono*
) 
perform eager contextdependent evaluation for applications of bv kinds in the equality engine

bveqengine
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
enable equality engine when possible in bitvector theory

bvgausselim
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
simplify formula via Gaussian Elimination if applicable

bvintropow2
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
introduce bitvector powers of two as a preprocessing pass

bvpropagate
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
use bitvector propagation in the bitblaster

bvrwextendeq
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
enable additional rewrites over zero/sign extend over equalities with constants (useful on BV/2017Preinerschollsmt08)

bvsatsolver
[minisat  cryptominisat  cadical  kissat
, defaultcadical
] 
choose which sat solver to use, see –bvsatsolver=help
SAT solver for bitblasting backend.

bvsolver
[bitblast  bitblastinternal
, defaultbitblast
] 
choose bitvector solver, see –bvsolver=help
Bitvector solvers.

bitblast
: 
Enables bitblasting solver.

bitblastinternal
: 
Enables bitblasting to internal SAT solver with proof support.


bvtobool
[typebool
, defaultfalse
] (alsono*
) 
lift bitvectors of size 1 to booleans when possible
Datatypes Theory Module

cdtbisimilar
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
do bisimilarity check for codatatypes

dtbinarysplit
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
do binary splits for datatype constructor types

dtblastsplits
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
when applicable, blast splitting lemmas for all variables at once

dtcyclic
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
do cyclicity check for datatypes

dtinferaslemmas
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
always send lemmas out instead of making internal inferences

dtnestedrec
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
allow nested recursion in datatype definitions

dtpoliteoptimize
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
turn on optimization for polite combination

sygusabortsize
[typeint64_t
, default1
] 
tells enumerative sygus to only consider solutions up to term size N (1 == no limit, default)

sygusfair
[direct  dtsize  dtheightbound  dtsizebound  none
, defaultdtsize
] 
if and how to apply fairness for sygus
Modes for enforcing fairness for counterexample guided quantifier instantion.

direct
: 
Enforce fairness using direct conflict lemmas.

dtsize
: 
Enforce fairness using size operator.

dtheightbound
: 
Enforce fairness by height bound predicate.

dtsizebound
: 
Enforce fairness by size bound predicate.

none
: 
Do not enforce fairness.


sygusfairmax
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
use max instead of sum for multifunction sygus conjectures

sygusrewriter
[none  basic  extended
, defaultextended
] 
if and how to apply rewriting for sygus symmetry breaking
Modes for applying rewriting for sygus symmetry breaking.

none
: 
Do not use the rewriter.

basic
: 
Use the basic rewriter.

extended
: 
Use the extended rewriter.


sygussimplesymbreak
[none  basic  agg
, defaultagg
] 
if and how to apply simple symmetry breaking based on the grammar for smart enumeration
Modes for applying simple symmetry breaking based on the grammar for smart enumeration.

none
: 
Do not apply simple symmetry breaking.

basic
: 
Apply basic simple symmetry breaking.

agg
: 
Apply aggressive simple symmetry breaking.


sygussymbreaklazy
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
lazily add symmetry breaking lemmas for terms

sygussymbreakpbe
[typebool
, defaulttrue
] (alsono*
) 
sygus symmetry breaking lemmas based on pbe conjectures

sygussymbreakrlv
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
add relevancy conditions to symmetry breaking lemmas
Decision Heuristics Module

decision  decisionmode
[internal  justification  stoponly
, defaultinternal
] 
choose decision mode, see –decision=help
Decision modes.

internal
: 
Use the internal decision heuristics of the SAT solver.

justification
: 
An ATGPinspired justification heuristic.

stoponly
: 
Use the justification heuristic only to stop early, not for decisions.


jhrlvorder
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
maintain activitybased ordering for decision justification heuristic

jhskolem
[first  last
, defaultfirst
] 
[experts only]
policy for when to satisfy skolem definitions in justification heuristic
Policy for when to satisfy skolem definitions in justification heuristic

first
: 
satisfy pending relevant skolem definitions before input assertions

last
: 
satisfy pending relevant skolem definitions after input assertions


jhskolemrlv
[assert  always
, defaultassert
] 
[experts only]
policy for when to consider skolem definitions relevant in justification heuristic
Policy for when to consider skolem definitions relevant in justification heuristic

assert
: 
skolems are relevant when they occur in an asserted literal

always
: 
skolems are always relevant

Expression Module

typechecking
[typebool
, defaultDO_SEMANTIC_CHECKS_BY_DEFAULT
] (alsono*
) 
[experts only]
type check expressions

wfchecking
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
check that terms passed to API methods are well formed (default false for text interface)
Finite Field Theory Module

ffbitsum
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
parse bitsums

ffdisjunctivebit
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
leave disjunctive bit constraints (or (= x 1) (= x 0)) alone; otherwise, preprocess to (= (* x x) x)

fffieldpolys
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
include field polynomials in Groebner basis computation; don’t do this

ffsolver
[gb  split
, defaultgb
] 
[experts only]
which field solver (default: ‘gb’; see –ffsolver=help)
Which field solver

gb
: 
use a groebner basis for the whole system

split
: 
use multiple groebner bases for partitions of the system


fftracegb
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
use a traced groebner basis engine
FloatingPoint Module

fpexp
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Allow floatingpoint sorts of all sizes, rather than only Float32 (8/24) or Float64 (11/53) (experimental)

fplazywb
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Enable lazier wordblasting (on preNotifyFact instead of registerTerm)
Driver Module

dumpdifficulty
[typebool
, defaultfalse
] (alsono*
) 
dump the difficulty measure after every response to checksat

dumpinstantiations
[typebool
, defaultfalse
] (alsono*
) 
output instantiations of quantified formulas after every UNSAT/VALID response

dumpinstantiationsdebug
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
output instantiations of quantified formulas after every UNSAT/VALID response, with debug information

dumpmodels
[typebool
, defaultfalse
] (alsono*
) 
output models after every SAT/INVALID/UNKNOWN response

dumpproofs
[typebool
, defaultfalse
] (alsono*
) 
output proofs after every UNSAT/VALID response

dumpunsatcores
[typebool
, defaultfalse
] (alsono*
) 
output unsat cores after every UNSAT/VALID response

dumpunsatcoreslemmas
[typebool
, defaultfalse
] (alsono*
) 
output lemmas in unsat cores after every UNSAT/VALID response

earlyexit
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
do not run destructors at exit; default on except in debug builds

forcenolimitcpuwhiledump
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Force no CPU limit when dumping models and proofs

portfoliojobs
[typeuint64_t
, default1
] 
[experts only]
Number of parallel jobs the portfolio engine can run

segvspin
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
spin on segfault/other crash waiting for gdb

showtracetags
[typebool
, defaultfalse
] 
[experts only]
show all available tags for tracing

useportfolio
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Use internal portfolio mode based on the logic
Parallel Module

appendlearnedliteralstocubes
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
emit learned literals with the cubes

checksbeforepartition
[typeuint64_t
, default1
] 
[experts only]
number of standard or full effort checks until partitioning

checksbetweenpartitions
[typeuint64_t
, default1
] 
[experts only]
number of checks between partitions

computepartitions
[typeuint64_t
, default0
] 
[experts only]
make n partitions. n <2 disables computing partitions entirely

partitioncheck  check
[standard  full
, defaultstandard
] 
[experts only]
select whether partitioning happens at full or standard check
Partition check modes.

standard
: 
create partitions at standard checks

full
: 
create partitions at full checks


partitionconflictsize
[typeuint64_t
, default0
] 
[experts only]
number of literals in a cube; if no partition size is set, then the partition conflict size is chosen to be log2(number of requested partitions)

partitionstarttime
[typeuint64_t
, default30
] 
[experts only]
time to start creating partitions in seconds

partitionstrategy  partition
[decisionscatter  heapscatter  lemmascatter  decisioncube  heapcube  lemmacube
, defaultdecisionscatter
] 
[experts only]
choose partition strategy mode
Partition strategy modes.

decisionscatter
: 
For 4 partitions, creates partitions C1, !C1 & C2, !C1 & !C2 & C3, !C1 & !C2 & !C3, from decisions

heapscatter
: 
For 4 partitions, creates partitions C1, !C1 & C2, !C1 & !C2 & C3, !C1 & !C2 & !C3, from heap

lemmascatter
: 
For 4 partitions, creates partitions C1, !C1 & C2, !C1 & !C2 & C3, !C1 & !C2 & !C3, from lemmas

decisioncube
: 
Creates mutually exclusive cubes from the decisions in the SAT solver.

heapcube
: 
Creates mutually exclusive cubes from the order heap in the SAT solver.

lemmacube
: 
Creates mutually exclusive cubes from the lemmas sent to the SAT solver.


partitiontimeinterval
[typedouble
, default1.0
] 
[experts only]
time to wait between scatter partitions

partitiontlimit
[typeuint64_t
, default60
] 
[experts only]
time limit for partitioning in seconds

partitionwhen
[tlimit  climit
, defaulttlimit
] 
[experts only]
choose when to partition
PartitionWhen modes.

tlimit
: 
Partition when the time limit is exceeded.

climit
: 
Partition when number of checks is exceeded.


randompartitioning
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
create random partitions

writepartitionsto  partitionsout
[customManagedOut
, defaultManagedOut()
] 
[experts only]
set the output channel for writing partitions
Parser Module

filesystemaccess
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
limits the file system access if set to false

freshdeclarations
[typebool
, defaulttrue
] (alsono*
) 
use API interface for fresh constants when parsing declarations and definitions

globaldeclarations
[typebool
, defaultfalse
] (alsono*
) 
force all declarations and definitions to be global when parsing

semanticchecks
[typebool
, defaultDO_SEMANTIC_CHECKS_BY_DEFAULT
] (alsono*
) 
[experts only]
enable semantic checks, including type checks
Printing Module

bvprintconstsasindexedsymbols
[typebool
, defaultfalse
] (alsono*
) 
print bitvector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMTLIB 2.x

exprdepth
[typeint64_t
,1 <= N
, default1
] 
[experts only]
print exprs to depth N (0 == default, 1 == no limit)

flattenhochains
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
print (binary) application chains in a flattened way, e.g. (a b c) rather than ((a b) c)

modeluprint
[declsortandfun  declfun  none
, defaultnone
] 
determines how to print uninterpreted elements in models
uninterpreted elements in models printing modes.

declsortandfun
: 
print uninterpreted elements declarefun, and also include a declaresort for the sort

declfun
: 
print uninterpreted elements declarefun, but don’t include a declaresort for the sort

none
: 
(default) do not print declarations of uninterpreted elements in models.

Proof Module

alfprintreference
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Print reference to original file instead of redeclaring

checkproofsteps
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Check proof steps for satisfiability, for refutation soundness testing. Note this checks only steps for noncore proof rules

lfscexpandtrust
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Print the children of trusted proof steps

lfscflatten
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Flatten steps in the LFSC proof

optresreconstructionsize
[typebool
, defaulttrue
] (alsono*
) 
Optimize resolution reconstruction to reduce proof size

printdotclusters
[typebool
, defaultfalse
] (alsono*
) 
Whether the proof node clusters (e.g. SAT, CNF, INPUT) will be printed when using the dot format or not.

proofaletherespivots
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Add pivots to Alethe resolution steps

proofannotate
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
add optional annotations to proofs, which enables statistics for inference ids for lemmas and conflicts appearing in final proof

proofcheck
[eager  eagersimple  lazy  none
, defaultnone
] 
[experts only]
select internal proof checking mode
Internal proof checking modes.

eager
: 
check rule applications and proofs from generators eagerly for local debugging

eagersimple
: 
check rule applications during construction

lazy
: 
check rule applications only during final proof construction

none
: 
do not check rule applications


proofdagglobal
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
Dagify terms in proofs using global definitions

proofdotdag
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Indicates if the dot proof will be printed as a DAG or as a tree

proofelimsubtypes
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Eliminate subtypes (mixed arithmetic) in proofs

proofformatmode
[none  dot  lfsc  alethe  alf
, defaultalf
] 
select language of proof output
Proof format modes.

none
: 
Do not translate proof output

dot
: 
Output DOT proof

lfsc
: 
Output LFSC proof

alethe
: 
Output Alethe proof

alf
: 
Output AletheLF proof


proofgranularity
[macro  rewrite  theoryrewrite  dslrewrite
, defaultmacro
] 
modes for proof granularity
Modes for proof granularity.

macro
: 
Allow macros. Do not improve the granularity of proofs.

rewrite
: 
Allow rewrite or substitution steps, expand macros.

theoryrewrite
: 
Allow theory rewrite steps, expand macros, rewrite and substitution steps.

dslrewrite
: 
Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps.


proofpedantic
[typeuint64_t
,N <= 100
, default0
] 
[experts only]
assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof

proofppmerge
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
merge subproofs in final proof postprocessor

proofprintconclusion
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Print conclusion of proof steps when printing AST

proofpruneinput
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Prune unused input assumptions from final scope

proofrewriterconsreclimit
[typeuint64_t
, default15
] 
the matching recursion limit for reconstructing proofs of theory rewrites

proofrewriterconssteplimit
[typeuint64_t
, default200
] 
the limit of steps considered for reconstructing proofs of theory rewrites
SAT Layer Module

minisatdumpdimacs
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
instead of solving minisat dumps the asserted clauses in Dimacs format

minisatsimplification
[all  clauseelim  none
, defaultall
] 
[experts only]
Simplifications to be performed by Minisat.
Modes for Minisat simplifications.

all
: 
Variable and clause elimination, plus other simplifications.

clauseelim
: 
Caluse elimination and other simplifications, except variable elimination.

none
: 
No simplifications.


preregistermode
[eager  lazy
, defaulteager
] 
[experts only]
Modes for when to preregister literals.
Modes for when to preregister literals.

eager
: 
Preregister literals when they are registered as literals in the SAT solver.

lazy
: 
Preregister literals when they are asserted by the SAT solver.


randomfreq  randomfrequency
[typedouble
,0.0 <= P <= 1.0
, default0.0
] 
[experts only]
sets the frequency of random decisions in the sat solver (P=0.0 by default)

restartintbase
[typeuint64_t
, default25
] 
[experts only]
sets the base restart interval for the sat solver (N=25 by default)

restartintinc
[typedouble
,0.0 <= F
, default3.0
] 
[experts only]
sets the restart interval increase factor for the sat solver (F=3.0 by default)

satrandomseed
[typeuint64_t
, default0
] 
sets the random seed for the sat solver

satsolver
[minisat  cadical
, defaultminisat
] 
[experts only]
choose which sat solver to use, see –satsolver=help
CDCL(T) SAT solver backend.
Quantifiers Module

cbqi
[typebool
, defaulttrue
] (alsono*
) 
enable conflictbased quantifier instantiation

cbqiallconflict
[typebool
, defaultfalse
] (alsono*
) 
add all available conflicting instances during conflictbased instantiation

cbqimode
[conflict  propeq
, defaultpropeq
] 
what effort to apply conflict find mechanism
Quantifier conflict find modes.

conflict
: 
Apply QCF algorithm to find conflicts only.

propeq
: 
Apply QCF algorithm to propagate equalities as well as conflicts.


cbqiskiprd
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
optimization, skip instances based on possibly irrelevant portions of quantified formulas

cbqitconstraint
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
enable entailment checks for tconstraints in cbqi algorithm

cbqivoexp
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
cbqi experimental variable ordering

cegissample
[none  use  trust
, defaultnone
] 
mode for using samples in the counterexampleguided inductive synthesis loop
Modes for sampling with counterexampleguided inductive synthesis (CEGIS).

none
: 
Do not use sampling with CEGIS.

use
: 
Use sampling to accelerate CEGIS. This will rule out solutions for a conjecture when they are not satisfied by a sample point.

trust
: 
Trust that when a solution for a conjecture is always true under sampling, then it is indeed a solution. Note this option may print out spurious solutions for synthesis conjectures.


cegqi
[typebool
, defaultfalse
] (alsono*
) 
turns on counterexamplebased quantifier instantiation

cegqiall
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
apply counterexamplebased instantiation to all quantified formulas

cegqibv
[typebool
, defaulttrue
] (alsono*
) 
use wordlevel inversion approach for counterexampleguided quantifier instantiation for bitvectors

cegqibvconcatinv
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
compute inverse for concat over equalities rather than producing an invertibility condition

cegqibvineq
[eqslack  eqboundary  keep
, defaulteqboundary
] 
choose mode for handling bitvector inequalities with counterexampleguided instantiation
Modes for handling bitvector inequalities in counterexampleguided instantiation.

eqslack
: 
Solve for the inequality using the slack value in the model, e.g., t > s becomes t = s + ( ts )^M.

eqboundary
: 
Solve for the boundary point of the inequality, e.g., t > s becomes t = s+1.

keep
: 
Solve for the inequality directly using side conditions for invertibility.


cegqibvinterleavevalue
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
interleave model value instantiation with wordlevel inversion approach

cegqibvlinear
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
linearize adder chains for variables

cegqibvrmextract
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
replaces extract terms with variables for counterexampleguided instantiation for bitvectors

cegqibvsolvenl
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
try to solve nonlinear bv literals using model value projections

cegqifull
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
turns on full effort counterexamplebased quantifier instantiation, which may resort to modelvalue instantiation

cegqiinfint
[typebool
, defaultfalse
] (alsono*
) 
use integer infinity for vts in counterexamplebased quantifier instantiation

cegqiinfreal
[typebool
, defaultfalse
] (alsono*
) 
use real infinity for vts in counterexamplebased quantifier instantiation

cegqiinnermost
[typebool
, defaulttrue
] (alsono*
) 
only process innermost quantified formulas in counterexamplebased quantifier instantiation

cegqimidpoint
[typebool
, defaultfalse
] (alsono*
) 
choose substitutions based on midpoints of lower and upper bounds for counterexamplebased quantifier instantiation

cegqiminbounds
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use minimally constrained lower/upper bound for counterexamplebased quantifier instantiation

cegqimultiinst
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
when applicable, do multi instantiations per quantifier per round in counterexamplebased quantifier instantiation

cegqinestedqe
[typebool
, defaultfalse
] (alsono*
) 
process nested quantified formulas with quantifier elimination in counterexamplebased quantifier instantiation

cegqinopt
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
nonoptimal bounds for counterexamplebased quantifier instantiation

cegqirounduplia
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
round up integer lower bounds in substitutions for counterexamplebased quantifier instantiation

condvarsplitquant
[off  on  agg
, defaulton
] 
[experts only]
split quantified formulas that lead to variable eliminations
Modes for splitting quantified formulas that lead to variable eliminations.

off
: 
Do not split quantified formulas.

on
: 
Split quantified formulas that lead to variable eliminations.

agg
: 
Aggressively split quantified formulas that lead to variable eliminations.


conjecturegen
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
generate candidate conjectures for inductive proofs

conjecturegengtenum
[typeint64_t
, default50
] 
[experts only]
number of ground terms to generate for model filtering

conjecturegenmaxdepth
[typeint64_t
, default3
] 
[experts only]
maximum depth of terms to consider for conjectures

conjecturegenperround
[typeint64_t
, default1
] 
[experts only]
number of conjectures to generate per instantiation round

consexptriggers
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use constructor expansion for single constructor datatypes triggers

dtstcind
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
apply strengthening for existential quantification over datatypes based on structural induction

dtvarexpquant
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
expand datatype variables bound to one constructor in quantifiers

ematching
[typebool
, defaulttrue
] (alsono*
) 
whether to do heuristic Ematching

elimtautquant
[typebool
, defaulttrue
] (alsono*
) 
eliminate tautological disjuncts of quantified formulas

enuminst
[typebool
, defaultfalse
] (alsono*
) 
enumerative instantiation: instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown

enuminstinterleave
[typebool
, defaultfalse
] (alsono*
) 
interleave enumerative instantiation with other techniques

enuminstlimit
[typeint64_t
, default1
] 
[experts only]
maximum number of rounds of enumerative instantiation to apply (1 means no limit)

enuminstrd
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
whether to use relevant domain first for enumerative instantiation strategy

enuminststratify
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
stratify effort levels in enumerative instantiation, which favors speed over fairness

enuminstsum
[typebool
, defaultfalse
] (alsono*
) 
enumerating tuples of quantifiers by increasing the sum of indices, rather than the maximum

extrewritequant
[typebool
, defaultfalse
] (alsono*
) 
apply extended rewriting to bodies of quantified formulas

finitemodelfind
[typebool
, defaultfalse
] (alsono*
) 
use finite model finding heuristic for quantifier instantiation

fmfbound
[typebool
, defaultfalse
] (alsono*
) 
finite model finding on bounded quantification

fmfboundblast
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
send all instantiations for bounded ranges in a single round

fmfboundlazy
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
enforce bounds for bounded quantification lazily via use of proxy variables

fmffun
[typebool
, defaultfalse
] (alsono*
) 
find models for recursively defined functions, assumes functions are admissible

fmffunrlv
[typebool
, defaultfalse
] (alsono*
) 
find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant

fmfmbqi
[none  fmc  trust
, defaultfmc
] 
[experts only]
choose mode for modelbased quantifier instantiation
Modelbased quantifier instantiation modes.

none
: 
Disable modelbased quantifier instantiation.

fmc
: 
Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability Modulo Theories.

trust
: 
Do not instantiate quantified formulas (incomplete technique).


fmftypecompletionthresh
[typeint64_t
, default1000
] 
the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted

fullsaturatequant
[typebool
, defaultfalse
] (alsono*
) 
resort to full effort techniques instead of answering unknown due to limited quantifier reasoning. Currently enables enumerative instantiation

globalnegate
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
do global negation of input formula

hoelim
[typebool
, defaultfalse
] (alsono*
) 
eagerly eliminate higherorder constraints

hoelimstoreax
[typebool
, defaulttrue
] (alsono*
) 
use store axiom during hoelim

homatching
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
do higherorder matching algorithm for triggers with variable operators

homergetermdb
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
merge term indices modulo equality

ieval
[off  use  uselearn
, defaultuse
] 
mode for using instantiation evaluation
Mode for using instantiation evaluation.

off
: 
Do not use instantiation evaluation.

use
: 
Use instantiation evaluation.

uselearn
: 
Use instantiation evaluation, and generalize learning.


incrementtriggers
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
generate additional triggers as needed during search

instmaxlevel
[typeint64_t
, default1
] 
[experts only]
maximum inst level of terms used to instantiate quantified formulas with (1 == no limit, default)

instmaxrounds
[typeint64_t
, default1
] 
maximum number of instantiation rounds (1 == no limit, default)

instnoentail
[typebool
, defaulttrue
] (alsono*
) 
do not consider instances of quantified formulas that are currently entailed

instwhen
[full  fulldelay  fulllastcall  fulldelaylastcall  lastcall
, defaultfulllastcall
] 
when to apply instantiation
Instantiation modes.

full
: 
Run instantiation round at full effort, before theory combination.

fulldelay
: 
Run instantiation round at full effort, before theory combination, after all other theories have finished.

fulllastcall
: 
Alternate running instantiation rounds at full effort and last call. In other words, interleave instantiation and theory combination.

fulldelaylastcall
: 
Alternate running instantiation rounds at full effort after all other theories have finished, and last call.

lastcall
: 
Run instantiation at last call effort, after theory combination and and theories report sat.


instwhenphase
[typeint64_t
, default2
] 
[experts only]
instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen

intwfind
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
apply strengthening for integers based on wellfounded induction

itedttsplitquant
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
split ites with dt testers as conditions

iteliftquant
[none  simple  all
, defaultsimple
] 
ite lifting mode for quantified formulas
ITE lifting modes for quantified formulas.

none
: 
Do not lift ifthenelse in quantified formulas.

simple
: 
Lift ifthenelse in quantified formulas if results in smaller term size.

all
: 
Lift ifthenelse in quantified formulas.


literalmatching
[none  use  aggpredicate  agg
, defaultuse
] 
[experts only]
choose literal matching mode
Literal match modes.

none
: 
Do not use literal matching.

use
: 
Consider phase requirements of triggers conservatively. For example, the trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with terms in the equivalence class of true, and likewise Q( x ) will not be matched terms in the equivalence class of false. Extends to equality.

aggpredicate
: 
Consider phase requirements aggressively for predicates. In the above example, only match P( x ) with terms that are in the equivalence class of false.

agg
: 
Consider the phase requirements aggressively for all triggers.


macrosquant
[typebool
, defaultfalse
] (alsono*
) 
perform quantifiers macro expansion

macrosquantmode
[all  ground  grounduf
, defaultgrounduf
] 
mode for quantifiers macro expansion
Modes for quantifiers macro expansion.

all
: 
Infer definitions for functions, including those containing quantified formulas.

ground
: 
Only infer ground definitions for functions.

grounduf
: 
Only infer ground definitions for functions that result in triggers for all free variables.


mbqi
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use modelbased quantifier instantiation

mbqiinterleave
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
interleave modelbased quantifier instantiation with other techniques

mbqioneinstperround
[typebool
, defaultfalse
] (alsono*
) 
only add one instantiation per quantifier per round for mbqi

miniscopequant
[off  conj  fv  conjandfv  agg
, defaultconjandfv
] 
miniscope mode for quantified formulas
Miniscope quantifiers modes.

off
: 
Do not miniscope quantifiers.

conj
: 
Use miniscoping of conjunctions only.

fv
: 
Use free variable miniscoping only.

conjandfv
: 
Enable both conjunction and free variable miniscoping.

agg
: 
Enable aggressive miniscope, which further may rewrite quantified formulas into a form where miniscoping is possible.


multitriggercache
[typebool
, defaultfalse
] (alsono*
) 
caching version of multi triggers

multitriggerlinear
[typebool
, defaulttrue
] (alsono*
) 
implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms

multitriggerpriority
[typebool
, defaultfalse
] (alsono*
) 
only try multi triggers if single triggers give no instantiations

multitriggerwhensingle
[typebool
, defaultfalse
] (alsono*
) 
select multi triggers when single triggers exist

oracles
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Enable interface to external oracles

partialtriggers
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use triggers that do not contain all free variables

poolinst
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
poolbased instantiation: instantiate with ground terms occurring in userspecified pools

preskolemquant
[off  on  agg
, defaultoff
] 
modes to apply skolemization eagerly to bodies of quantified formulas
Modes to apply skolemization eagerly to bodies of quantified formulas.

off
: 
Do not apply Skolemization eagerly.

on
: 
Apply Skolemization eagerly to toplevel (negatively asserted) quantified formulas.

agg
: 
Apply Skolemization eagerly and aggressively during preprocessing.


preskolemquantnested
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
apply skolemization to nested quantified formulas

prenexquant
[none  simple  norm
, defaultsimple
] 
prenex mode for quantified formulas
Prenex quantifiers modes.

none
: 
Do not prenex nested quantifiers.

simple
: 
Do simple prenexing of same sign quantifiers.

norm
: 
Prenex to prenex normal form.


prenexquantuser
[typebool
, defaultfalse
] (alsono*
) 
prenex quantified formulas with user patterns

printinstfull
[typebool
, defaulttrue
] (alsono*
) 
print instantiations for formulas that do not have given identifiers

purifytriggers
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y1

quantalphaequiv
[typebool
, defaulttrue
] (alsono*
) 
infer alpha equivalence between quantified formulas

quantdsplit
[none  default  agg
, defaultdefault
] 
mode for dynamic quantifiers splitting
Modes for quantifiers splitting.

none
: 
Never split quantified formulas.

default
: 
Split quantified formulas over some finite datatypes when finite model finding is enabled.

agg
: 
Aggressively split quantified formulas.


quantfunwd
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
assume that function defined by quantifiers are well defined

quantind
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use all available techniques for inductive reasoning

quantrepmode
[ee  first  depth
, defaultfirst
] 
[experts only]
selection mode for representatives in quantifiers engine
Modes for quantifiers representative selection.

ee
: 
Let equality engine choose representatives.

first
: 
Choose terms that appear first.

depth
: 
Choose terms that are of minimal depth.


registerquantbodyterms
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
consider ground terms within bodies of quantified formulas for matching

relationaltriggers
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
choose relational triggers such as x = f(y), x >= f(y)

relevanttriggers
[typebool
, defaultfalse
] (alsono*
) 
prefer triggers that are more relevant based on SInE style analysis

subcbqi
[typebool
, defaultfalse
] (alsono*
) 
Enable conflictbased instantiation subsolver strategy

subcbqitimeout
[typeuint64_t
, default0
] 
Timeout (in milliseconds) for subsolver calls for subcbqi

sygus
[typebool
, defaultfalse
] (alsono*
) 
support SyGuS commands

sygusaddconstgrammar
[typebool
, defaulttrue
] (alsono*
) 
statically add constants appearing in conjecture to grammars

sygusargrelevant
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
static inference techniques for computing whether arguments of functionstosynthesize are relevant

sygusautounfold
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems

sygusboolitereturnconst
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
Only use Boolean constants for return values in unificationbased function synthesis

syguscoreconnective
[typebool
, defaulttrue
] (alsono*
) 
use unsat core analysis to construct Boolean connective to sygus conjectures

syguscrepairabort
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
abort if constant repair techniques are not applicable

sygusenum
[smart  fast  random  varagnostic  auto
, defaultauto
] 
mode for sygus enumeration
Modes for sygus enumeration.

smart
: 
Use smart enumeration based on datatype constraints.

fast
: 
Use optimized enumerator for sygus enumeration.

random
: 
Use basic random enumerator for sygus enumeration.

varagnostic
: 
Use sygus solver to enumerate terms that are agnostic to variables.

auto
: 
Internally decide the best policy for each enumerator.


sygusenumfastnumconsts
[typeuint64_t
, default5
] 
[experts only]
the branching factor for the number of interpreted constants to consider for each size when using –sygusenum=fast

sygusenumrandomp
[typedouble
,0.0 <= P <= 1.0
, default0.5
] 
[experts only]
the parameter of the geometric distribution used to determine the size of terms generated by –sygusenum=random

sygusevalunfold
[none  single  singlebool  multi
, defaultsinglebool
] 
modes for sygus evaluation unfolding
Modes for sygus evaluation unfolding.

none
: 
Do not use sygus evaluation unfolding.

single
: 
Do singlestep unfolding for all evaluation functions.

singlebool
: 
Do singlestep unfolding for Boolean functions and ITEs, and multistep unfolding for all others.

multi
: 
Do multistep unfolding for all evaluation functions.


sygusexprminerchecktimeout
[typeuint64_t
, default0
] 
[experts only]
timeout (in milliseconds) for satisfiability checks in expression miners

sygusfiltersol
[none  strong  weak
, defaultnone
] 
[experts only]
mode for filtering sygus solutions
Modes for filtering sygus solutions.

none
: 
Do not filter sygus solutions.

strong
: 
Filter solutions that are logically stronger than others.

weak
: 
Filter solutions that are logically weaker than others.


sygusfiltersolrev
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
compute backwards filtering to compute whether previous solutions are filtered based on later ones

sygusgrammarcons
[simple  anyconst  anyterm  anytermconcise
, defaultsimple
] 
mode for SyGuS grammar construction
Modes for default SyGuS grammars.

simple
: 
Use simple grammar construction (no symbolic terms or constants).

anyconst
: 
Use symoblic constant constructors.

anyterm
: 
When applicable, use constructors corresponding to any symbolic term. This option enables a sumofmonomials grammar for arithmetic. For all other types, it enables symbolic constant constructors.

anytermconcise
: 
When applicable, use constructors corresponding to any symbolic term, favoring conciseness over generality. This option is equivalent to anyterm but enables a polynomial grammar for arithmetic when not in a combined theory.


sygusgrammarnorm
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
statically normalize sygus grammars based on flattening (linearization)

sygusgrammarusedisj
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
use disjunctions in internally generated grammars. this is set to false when solving abduction queries.

sygusinference
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
attempt to preprocess arbitrary inputs to sygus conjectures

sygusinst
[typebool
, defaultfalse
] (alsono*
) 
Enable SyGuS instantiation quantifiers module

sygusinstmode
[priorityinst  priorityeval  interleave
, defaultpriorityinst
] 
[experts only]
select instantiation lemma mode
SyGuS instantiation lemma modes.

priorityinst
: 
add instantiation lemmas first, add evaluation unfolding if instantiation fails.

priorityeval
: 
add evaluation unfolding lemma first, add instantiation lemma if unfolding lemmas already added.

interleave
: 
add instantiation and evaluation unfolding lemmas in the same step.


sygusinstscope
[in  out  both
, defaultin
] 
[experts only]
select scope of ground terms
scope for collecting ground terms for the grammar.

in
: 
use ground terms inside given quantified formula only.

out
: 
use ground terms outside of quantified formulas only.

both
: 
combines inside and outside.


sygusinsttermsel
[min  max  both
, defaultmin
] 
[experts only]
granularity for ground terms
Ground term selection modes.

min
: 
collect minimal ground terms only.

max
: 
collect maximal ground terms only.

both
: 
combines minimal and maximal .


sygusinvtempl
[none  pre  post
, defaultpost
] 
template mode for sygus invariant synthesis (weaken precondition, strengthen postcondition, or none)
Template modes for sygus invariant synthesis.

none
: 
Synthesize invariant directly.

pre
: 
Synthesize invariant based on weakening of precondition.

post
: 
Synthesize invariant based on strengthening of postcondition.


sygusinvtemplwhensg
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use invariant templates (with solution reconstruction) for syntax guided problems

sygusmingrammar
[typebool
, defaulttrue
] (alsono*
) 
statically minimize sygus grammars

sygusout
[status  statusanddef  sygusstandard
, defaultsygusstandard
] 
output mode for sygus
Modes for sygus solution output.

status
: 
Print only status for checksynth calls.

statusanddef
: 
Print status followed by definition corresponding to solution.

sygusstandard
: 
Print based on SyGuS standard.


syguspbe
[typebool
, defaulttrue
] (alsono*
) 
enable approach which unifies conditional solutions, specialized for programmingbyexamples (pbe) conjectures

syguspbemultifair
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
when using multiple enumerators, ensure that we only register value of minimial term size

syguspbemultifairdiff
[typeint64_t
, default0
] 
[experts only]
when using multiple enumerators, ensure that we only register values of minimial term size plus this value (default 0)

sygusqepreproc
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use quantifier elimination as a preprocessing step for sygus

sygusquerygen
[basic  samplesat  unsat
, defaultbasic
] 
[experts only]
mode for generating interesting satisfiability queries using SyGuS, for internal fuzzing
Modes for generating interesting satisfiability queries using SyGuS.

basic
: 
Generate all queries using SyGuS enumeration of the given grammar

samplesat
: 
Generate interesting SAT queries based on sampling, for e.g. soundness testing.

unsat
: 
Generate interesting UNSAT queries, for e.g. proof testing.


sygusquerygendumpfiles
[none  all  unsolved
, defaultnone
] 
[experts only]
mode for dumping external files corresponding to interesting satisfiability queries with sygusquerygen
Query file options.

none
: 
Do not dump query files when using –sygusquerygen.

all
: 
Dump all query files.

unsolved
: 
Dump query files that the subsolver did not solve.


sygusquerygenfiltersolved
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
do not print queries that are solved

sygusquerygenthresh
[typeuint64_t
, default5
] 
[experts only]
number of points that we allow to be equal for enumerating satisfiable queries with sygusquerygen

sygusrecfun
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
enable efficient support for recursive functions in sygus grammars

sygusrecfunevallimit
[typeuint64_t
, default1000
] 
[experts only]
use a hard limit for how many times in a given evaluator call a recursive function can be evaluated (so infinite loops can be avoided)

sygusrepairconst
[typebool
, defaulttrue
] (alsono*
) 
use approach to repair constants in sygus candidate solutions

sygusrepairconsttimeout
[typeuint64_t
, default0
] 
[experts only]
timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions

sygusrrsynthaccel
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
add dynamic symmetry breaking clauses based on candidate rewrites

sygusrrsynthcheck
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
use satisfiability check to verify correctness of candidate rewrites

sygusrrsynthfiltercong
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
filter candidate rewrites based on congruence

sygusrrsynthfiltermatch
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
filter candidate rewrites based on matching

sygusrrsynthfilternl
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
filter nonlinear candidate rewrites

sygusrrsynthfilterorder
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
filter candidate rewrites based on variable ordering

sygusrrsynthinputnvars
[typeint64_t
, default3
] 
[experts only]
the maximum number of variables per type that appear in rewrites from sygusrrsynthinput

sygusrrsynthrec
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
synthesize rewrite rules over all sygus grammar types recursively

sygussamplefpuniform
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
sample floatingpoint values uniformly instead of in a biased fashion

sygussamplegrammar
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
when applicable, use grammar for choosing sample points

sygussamples
[typeint64_t
, default1000
] 
[experts only]
number of points to consider when doing sygus rewriter sample testing

sygussi
[none  use  all
, defaultnone
] 
mode for processing single invocation synthesis conjectures
Modes for single invocation techniques.

none
: 
Do not use single invocation techniques.

use
: 
Use single invocation techniques only if grammar is not restrictive.

all
: 
Always use single invocation techniques.


sygussiabort
[typebool
, defaultfalse
] (alsono*
) 
abort if synthesis conjecture is not single invocation

sygussircons
[none  try  alllimit  all
, defaultall
] 
policy for reconstructing solutions for single invocation conjectures
Modes for reconstruction solutions while using single invocation techniques.

none
: 
Do not try to reconstruct solutions in the original (userprovided) grammar when using single invocation techniques. In this mode, solutions produced by cvc5 may violate grammar restrictions.

try
: 
Try to reconstruct solutions in the original grammar when using single invocation techniques in an incomplete (failfast) manner.

alllimit
: 
Try to reconstruct solutions in the original grammar, but terminate if a maximum number of rounds for reconstruction is exceeded.

all
: 
Try to reconstruct solutions in the original grammar. In this mode, we do not terminate until a solution is successfully reconstructed.


sygussirconslimit
[typeint64_t
, default10000
] 
[experts only]
number of rounds of enumeration to use during solution reconstruction (negative means unlimited)

sygussirconsp
[typedouble
,0.0 <= P <= 1.0
, default0.5
] 
[experts only]
the parameter of the geometric distribution used to determine the number of unification patterns generated by single invocation techniques.

sygusstream
[typebool
, defaultfalse
] (alsono*
) 
enumerate a stream of solutions instead of terminating after the first one

sygusunifcondindependentnorepeatsol
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
Do not try repeated solutions when using independent synthesis of conditions in unificationbased function synthesis

sygusunifpi
[none  complete  condenum  condenumigain
, defaultnone
] 
mode for synthesis via piecewiseindepedent unification
Modes for piecewiseindependent unification.

none
: 
Do not use piecewiseindependent unification.

complete
: 
Use complete approach for piecewiseindependent unification (see Section 3 of Barbosa et al FMCAD 2019)

condenum
: 
Use unconstrained condition enumeration for piecewiseindependent unification (see Section 4 of Barbosa et al FMCAD 2019).

condenumigain
: 
Same as condenum, but additionally uses an information gain heuristic when doing decision tree learning.


sygusunifshufflecond
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Shuffle condition pool when building solutions (may change solutions sizes)

sygusverifyinstmaxrounds
[typeint64_t
, default10
] 
[experts only]
maximum number of instantiation rounds for sygus verification calls (1 == no limit, default is 10)

sygusverifytimeout
[typeuint64_t
, default0
] 
timeout (in milliseconds) for verifying satisfiability of synthesized terms

termdbmode
[all  relevant
, defaultall
] 
which ground terms to consider for instantiation
Modes for terms included in the quantifiers term database.

all
: 
Quantifiers module considers all ground terms.

relevant
: 
Quantifiers module considers only ground terms connected to current assertions.


triggeractivesel
[all  min  max
, defaultall
] 
[experts only]
selection mode to activate triggers
Trigger active selection modes.

all
: 
Make all triggers active.

min
: 
Activate triggers with minimal ground terms.

max
: 
Activate triggers with maximal ground terms.


triggersel
[min  max  minsmax  minsall  all
, defaultmin
] 
selection mode for triggers
Trigger selection modes.

min
: 
Consider only minimal subterms that meet criteria for triggers.

max
: 
Consider only maximal subterms that meet criteria for triggers.

minsmax
: 
Consider only minimal subterms that meet criteria for single triggers, maximal otherwise.

minsall
: 
Consider only minimal subterms that meet criteria for single triggers, all otherwise.

all
: 
Consider all subterms that meet criteria for triggers.


userpat
[use  trust  strict  resort  ignore  interleave
, defaulttrust
] 
policy for handling userprovided patterns for quantifier instantiation
These modes determine how user provided patterns (triggers) are used during Ematching. The modes vary on when instantiation based on userprovided triggers is combined with instantiation based on automatically selected triggers.

use
: 
Use both userprovided and autogenerated patterns when patterns are provided for a quantified formula.

trust
: 
When provided, use only userprovided patterns for a quantified formula.

strict
: 
When provided, use only userprovided patterns for a quantified formula, and do not use any other instantiation techniques.

resort
: 
Use userprovided patterns only after autogenerated patterns saturate.

ignore
: 
Ignore userprovided patterns.

interleave
: 
Alternate between use/resort.


userpool
[use  trust  ignore
, defaulttrust
] 
[experts only]
policy for handling userprovided pools for quantifier instantiation
These modes determine how user provided pools are used in combination with other instantiation techniques.

use
: 
Use both userprovided pool and other instantiation strategies when pools are provided for a quantified formula.

trust
: 
When provided, use only userprovided pool for a quantified formula.

ignore
: 
Ignore userprovided pool.


varelimquant
[typebool
, defaulttrue
] (alsono*
) 
enable simple variable elimination for quantified formulas

varineqelimquant
[typebool
, defaulttrue
] (alsono*
) 
enable variable elimination based on infinite projection of unbound arithmetic variables
Separation Logic Theory Module

sepminrefine
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
only add refinement lemmas for minimal (innermost) assertions

seppreskolememp
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
eliminate emp constraint at preprocess time
Sets Theory Module

setsext
[typebool
, defaultfalse
] (alsono*
) 
enable extended symbols such as complement and universe in theory of sets

setsinferaslemmas
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
send inferences as lemmas

setsproxylemmas
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
introduce proxy variables eagerly to shorten lemmas
SMT Layer Module

abstractvalues
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
in models, output arrays (and in future, maybe others) using abstract values, as required by the SMTLIB standard

ackermann
[typebool
, defaultfalse
] (alsono*
) 
eliminate functions by ackermannization

bvtointusepow2
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use internal pow2 operator when translating shift notes

bvandintegergranularity
[typeuint64_t
,1 <= N <= 8
, default1
] 
[experts only]
granularity to use in –solvebvasint mode and for iand operator (experimental)

checkabducts
[typebool
, defaultfalse
] (alsono*
) 
checks whether produced solutions to getabduct are correct

checkinterpolants
[typebool
, defaultfalse
] (alsono*
) 
checks whether produced solutions to getinterpolant are correct

checkproofs
[typebool
, defaultfalse
] (alsono*
) 
after UNSAT/VALID, check the generated proof (with proof)

checksynthsol
[typebool
, defaultfalse
] (alsono*
) 
checks whether produced solutions to functionstosynthesize satisfy the conjecture

checkunsatcores
[typebool
, defaultfalse
] (alsono*
) 
after UNSAT/VALID, produce and check an unsat core (expensive)

debugcheckmodels
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions

deeprestart
[none  input  inputandsolvable  inputandprop  all
, defaultnone
] 
[experts only]
mode for deep restarts
Mode for deep restarts

none
: 
do not use deep restart

input
: 
learn literals that appear in the input

inputandsolvable
: 
learn literals that appear in the input and those that can be solved for variables that appear in the input

inputandprop
: 
learn literals that appear in the input and those that can be solved for variables, or correspond to constant propagations for terms that appear in the input

all
: 
learn all literals


deeprestartfactor
[typedouble
,0.0 <= F <= 1000.0
, default3.0
] 
[experts only]
sets the threshold for average assertions per literal before a deep restart

difficultymode
[lemmaliteral  lemmaliteralall  modelcheck
, defaultlemmaliteralall
] 
[experts only]
choose output mode for getdifficulty, see –difficultymode=help
difficulty output modes.

lemmaliteral
: 
Difficulty of an assertion is how many lemmas (at full effort) use a literal that the assertion depends on to be satisfied.

lemmaliteralall
: 
Difficulty of an assertion is how many lemmas use a literal that the assertion depends on to be satisfied.

modelcheck
: 
Difficulty of an assertion is how many times it was not satisfied in a candidate model.


earlyiteremoval
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
remove ITEs early in preprocessing

extrewprep
[off  use  agg
, defaultoff
] 
mode for using extended rewriter as a preprocessing pass, see –extrewprep=help
extended rewriter preprocessing pass modes.

off
: 
do not use extended rewriter as a preprocessing pass.

use
: 
use extended rewriter as a preprocessing pass.

agg
: 
use aggressive extended rewriter as a preprocessing pass.


foreigntheoryrewrite
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Crosstheory rewrites

iandmode
[value  sum  bitwise
, defaultvalue
] 
[experts only]
Set the refinement scheme for integer AND
Refinement modes for integer AND

value
: 
valuebased refinement

sum
: 
use sum to represent integer AND in refinement

bitwise
: 
use bitwise comparisons on binary representation of integer for refinement (experimental)


interpolantsmode
[default  assumptions  conjecture  shared  all
, defaultdefault
] 
choose interpolants production mode, see –interpolantsmode=help
Interpolants grammar mode

default
: 
use the default grammar for the theory or the userdefined grammar if given

assumptions
: 
use only operators that occur in the assumptions

conjecture
: 
use only operators that occur in the conjecture

shared
: 
use only operators that occur both in the assumptions and the conjecture

all
: 
use only operators that occur either in the assumptions or the conjecture


itesimp
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)

learnedrewrite
[typebool
, defaultfalse
] (alsono*
) 
rewrite the input based on learned literals

minimalunsatcores
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
if an unsat core is produced, it is reduced to a minimal unsat core

modelcores
[none  simple  nonimplied
, defaultnone
] 
mode for producing model cores
Model cores modes.

none
: 
Do not compute model cores.

simple
: 
Only include a subset of variables whose values are sufficient to show the input formula is satisfied by the given model.

nonimplied
: 
Only include a subset of variables whose values, in addition to the values of variables whose values are implied, are sufficient to show the input formula is satisfied by the given model.


modelvarelimuneval
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
allow variable elimination based on unevaluatable terms to variables

onrepeatitesimp
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
do the ite simplification pass again if repeating simplification

printcoresfull
[typebool
, defaultfalse
] (alsono*
) 
print all formulas regardless of whether they are named, e.g. in unsat cores

produceabducts
[typebool
, defaultfalse
] (alsono*
) 
support the getabduct command

produceassertions  interactivemode
[typebool
, defaulttrue
] (alsono*
) 
keep an assertions list. Note this option is always enabled.

produceassignments
[typebool
, defaultfalse
] (alsono*
) 
support the getassignment command

producedifficulty
[typebool
, defaultfalse
] (alsono*
) 
enable tracking of difficulty.

produceinterpolants
[typebool
, defaultfalse
] (alsono*
) 
turn on interpolation generation.

producelearnedliterals
[typebool
, defaultfalse
] (alsono*
) 
produce learned literals, support getlearnedliterals

produceproofs
[typebool
, defaultfalse
] (alsono*
) 
produce proofs, support checkproofs and getproof

produceunsatassumptions
[typebool
, defaultfalse
] (alsono*
) 
turn on unsat assumptions generation

produceunsatcores
[typebool
, defaultfalse
] (alsono*
) 
turn on unsat core generation. Unless otherwise specified, cores will be produced using SAT soving under assumptions and preprocessing proofs.

proofmode
[off  pponly  satproof  fullproof
, defaultoff
] 
[experts only]
choose proof mode, see –proofmode=help
proof modes.

repeatsimp
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
make multiple passes with nonclausal simplifier

simpitecompress
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
enables compressing ites after ite simplification

simpwithcare
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
enables simplifyWithCare in ite simplificiation

simplification  simplificationmode
[none  batch
, defaultbatch
] 
choose simplification mode, see –simplification=help
Simplification modes.

none
: 
Do not perform nonclausal simplification.

batch
: 
Save up all ASSERTions; run nonclausal simplification and clausal (MiniSat) propagation for all of them only after reaching a querying command (CHECKSAT or QUERY or predicate SUBTYPE declaration).


simplificationbcp
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
apply Boolean constant propagation as a substituion during simplification

solvebvasint
[off  sum  iand  bv  bitwise
, defaultoff
] 
mode for translating BVAnd to integer
solvebvasint modes.

off
: 
Do not translate bitvectors to integers

sum
: 
Generate a sum expression for each bvand instance, based on the value in –solvebvasintgranularity

iand
: 
Translate bvand to the iand operator

bv
: 
Translate bvand back to bitvectors

bitwise
: 
Introduce a UF operator for bvand, and eagerly add bitwise lemmas


solveintasbv
[typeuint64_t
,N <= 4294967295
, default0
] 
attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)

solverealasint
[typebool
, defaultfalse
] (alsono*
) 
attempt to solve a pure real satisfiable problem as an integer problem (for nonlinear)

sortinference
[typebool
, defaultfalse
] (alsono*
) 
calculate sort inference of input problem, convert the input based on monotonic sorts

staticlearning
[typebool
, defaulttrue
] (alsono*
) 
use static learning (on by default)

timeoutcoretimeout
[typeuint64_t
, default10000
] 
[experts only]
timeout (in milliseconds) for satisfiability checks for timeout cores

unconstrainedsimp
[typebool
, defaultfalse
] (alsono*
) 
turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis). Fully supported only in (subsets of) the logic QF_ABV.

unsatcoresmode
[off  satproof  assumptions
, defaultoff
] 
[experts only]
choose unsat core mode, see –unsatcoresmode=help
unsat cores modes.

off
: 
Do not produce unsat cores.

satproof
: 
Produce unsat cores from the SAT proof and prepocessing proofs.

assumptions
: 
Produce unsat cores using solving under assumptions and preprocessing proofs.

Strings Theory Module

reelim
[off  on  agg
, defaultoff
] 
regular expression elimination mode
Regular expression elimination modes.

off
: 
Do not use regular expression elimination.

on
: 
Use regular expression elimination.

agg
: 
Use aggressive regular expression elimination.


reintermode
[all  constant  oneconstant  none
, defaultnone
] 
[experts only]
determines which regular expressions intersections to compute
Regular expression intersection modes.

all
: 
Compute intersections for all regular expressions.

constant
: 
Compute intersections only between regular expressions that do not contain re.allchar or re.range.

oneconstant
: 
Compute intersections only between regular expressions such that at least one side does not contain re.allchar or re.range.

none
: 
Do not compute intersections for regular expressions.


seqarray
[lazy  eager  none
, defaultnone
] 
[experts only]
use arrayinspired solver for sequence updates in eager or lazy mode
use arrayinspired solver for sequence updates in eager or lazy mode

lazy
: 
use arrayinspired solver for sequence updates in lazy mode

eager
: 
use arrayinspired solver for sequence updates in eager mode

none
: 
do not use arrayinspired solver for sequence updates


stringsalphacard
[typeuint64_t
,N <= 196608
, default196608
] 
[experts only]
the assumed cardinality of the alphabet of characters for strings, which is a prefix of the interval of unicode code points in the SMTLIB standard

stringscheckentaillen
[typebool
, defaulttrue
] (alsono*
) 
check entailment between length terms to reduce splitting

stringscodeelim
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
eliminate code points during preprocessing

stringsdeqext
[typebool
, defaultfalse
] (alsono*
) 
use extensionality for string disequalities

stringseagereval
[typebool
, defaulttrue
] (alsono*
) 
perform eager contextdependent evaluation for applications of string kinds in the equality engine

stringseagerlenre
[typebool
, defaultfalse
] (alsono*
) 
use regular expressions for eager length conflicts

stringseagerreg
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
do registration lemmas for terms during preregistration. If false, do registration lemmas for terms when they appear in asserted literals

stringseagersolver
[typebool
, defaulttrue
] (alsono*
) 
use the eager solver

stringsexp
[typebool
, defaultfalse
] (alsono*
) 
experimental features in the theory of strings

stringsff
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
do flat form inferences

stringsfmf
[typebool
, defaultfalse
] (alsono*
) 
the finite model finding used by the theory of strings

stringsinferaslemmas
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
always send lemmas out instead of making internal inferences

stringsinfersym
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
generalized inferences in strings based on proxy symbols

stringslazypp
[typebool
, defaulttrue
] (alsono*
) 
perform string preprocessing lazily

stringslennorm
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
strings length normalization lemma

stringsmbr
[typebool
, defaulttrue
] (alsono*
) 
use models to avoid reductions for extended functions that introduce quantified formulas

stringsmodelmaxlen
[typeuint64_t
,N <= 2147483647
, default65536
] 
[experts only]
The maximum size of string values in models

stringsprocessloopmode
[full  simple  simpleabort  none  abort
, defaultfull
] 
determines how to process looping string equations
Loop processing modes.

full
: 
Perform full processing of looping word equations.

simple
: 
Omit normal loop breaking (default with –stringsfmf).

simpleabort
: 
Abort when normal loop breaking is required.

none
: 
Omit loop processing.

abort
: 
Abort if looping word equations are encountered.


stringsreposceager
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
eager reduction of positive membership into concatentation

stringsregexpinclusion
[typebool
, defaulttrue
] (alsono*
) 
use regular expression inclusion for finding conflicts and avoiding regular expression unfolding

stringsrexplainlemmas
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
regression explanations for string lemmas
Theory Layer Module

assignfunctionvalues
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
assign values for uninterpreted functions in models

condensefunctionvalues
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
condense values for functions in models rather than explicitly representing them

eemode
[distributed  central
, defaultdistributed
] 
[experts only]
mode for managing equalities across theory solvers
Defines mode for managing equalities across theory solvers.

distributed
: 
Each theory maintains its own equality engine.

central
: 
All applicable theories use the central equality engine.


lemmainprocess
[full  light  none
, defaultnone
] 
[experts only]
Modes for inprocessing lemmas.
Modes for inprocessing lemmas.

full
: 
Full inprocessing.

light
: 
Light inprocessing.

none
: 
No inprocessing.


lemmainprocessinfereqlit
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
Infer equivalent literals when using lemma inprocess

lemmainprocesssubs
[all  simple
, defaultsimple
] 
[experts only]
Modes for substitutions for inprocessing lemmas.
Modes for substitutions for inprocessing lemmas.

all
: 
All substitutions.

simple
: 
Simple substitutions.


relevancefilter
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
enable analysis of relevance of asserted literals with respect to the input formula

tcmode
[caregraph
, defaultcaregraph
] 
[experts only]
mode for theory combination
Defines mode for theory combination.

caregraph
: 
Use care graphs for theory combination.


theoryofmode
[type  term
, defaulttype
] 
[experts only]
mode for Theory::theoryof()
Defines how we associate theories with terms.

type
: 
Type variables, constants and equalities by type.

term
: 
Type variables as uninterpreted, type constants by theory, equalities by the parametric theory.

Uninterpreted Functions Theory Module

eagerarithbvconv
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
eagerly expand bitvector to arithmetic conversions during preprocessing

symmetrybreaker
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use UF symmetry breaker (Deharbe et al., CADE 2011)

ufhoext
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
apply extensionality on function symbols

uflazyll
[typebool
, defaulttrue
] (alsono*
) 
do lambda lifting lazily

ufss
[full  nominimal  none
, defaultfull
] 
mode of operation for uf with cardinality solver.
UF with cardinality options currently supported by the –ufss option when combined with finite model finding.

full
: 
Default, use UF with cardinality to find minimal models for uninterpreted sorts.

nominimal
: 
Use UF with cardinality to shrink models, but do no enforce minimality.

none
: 
Do not use UF with cardinality to shrink model sizes.


ufssabortcard
[typeint64_t
, default1
] 
tells the uf with cardinality to only consider models that interpret uninterpreted sorts of cardinality at most N (1 == no limit, default)

ufssfair
[typebool
, defaulttrue
] (alsono*
) 
use fair strategy for finite model finding multiple sorts

ufssfairmonotone
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
group monotone sorts when enforcing fairness for finite model finding