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, and they can additionally have one or more aliases (that can be used instead of their name anywhere) and a short name (a single letter). 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. A few options have custom types (for example err ) that 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 by
<name>
or
<short>
.
Most Boolean options can also be set to false by
no<name>
.
In the different APIs, this is done via
setOption("<name>",
"true"

"false")
.
For all other types, values can be given on the command line using
<name>=<value>
or
<name>
<value>
and
setOption("<name>",
"<value>")
in the different 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  sygus  sygusgrammar  trigger  rawbenchmark  learnedlits  subs  postasserts  preasserts
, defaultnone
] 
Enable output tag.
Output tags.

inst

print instantiations during solving

sygus

print enumerated terms and candidates generated by the sygus solver

sygusgrammar

print grammars automatically generated by the sygus solver

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


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

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

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

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

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

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

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

copyright
[typebool
, defaultfalse
] 
show cvc5 copyright information

h  help
[typebool
, defaultfalse
] 
full command line reference

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

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

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

arithcongman
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
(experimental) whether to use the congruence manager when the equality solver is enabled

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

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

d  debug
[typestring
] 
debug something (e.g. d arith), can repeat

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

bvextractarith
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
enable rewrite pushing extract [i:0] over arithmetic operations (can blow up)

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

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

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

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

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

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

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

showdebugtags
[typebool
, defaultfalse
] 
[experts only]
show all available tags for debugging

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

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

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

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

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.


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

printunsatcoresfull
[typebool
, defaultfalse
] (alsono*
) 
when printing unsat cores, include unlabeled assertions

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.

Proof Module

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
, defaultlazy
] 
[experts only]
select proof checking mode
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


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

proofformatmode
[none  dot  lfsc  alethe  tptp
, defaultnone
] 
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

tptp

Output TPTP proof (work in progress)


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


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
Quantifiers Module

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

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

cbqieagercheckrd
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
optimization, eagerly check relevant domain of matched position

cbqieagertest
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
optimization, test cbqi instances eagerly

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.


conjecturefilteractiveterms
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
filter based on active terms

conjecturefiltercanonical
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
filter based on canonicity

conjecturefiltermodel
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
filter based on model

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

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

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

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
[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).


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

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

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

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
, defaultfalse
] (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)

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

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
[none  basic  samplesat  unsat
, defaultnone
] 
[experts only]
mode for generating interesting satisfiability queries using SyGuS, for internal fuzzing
Modes for generating interesting satisfiability queries using SyGuS.

none

Do not generate queries with 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.


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
, defaultfalse
] (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

sygusrrsynth
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use sygus to enumerate candidate rewrite rules

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

sygusrrsynthinput
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
synthesize rewrite rules based on the input formula

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

sygusrrsynthinputusebool
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
synthesize Boolean rewrite rules based on the input formula

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

sygusrrverify
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
use sygus to verify the correctness of rewrite rules via sampling

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)

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
, default3
] 
[experts only]
maximum number of instantiation rounds for sygus verification calls (1 == no limit, default is 3)

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

termdbcd
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
register terms in term database based on the SAT context

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.


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

bvandintegergranularity
[typeuint64_t
, 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

difficultymode
[lemmaliteral  lemmaliteralall  modelcheck
, defaultlemmaliteral
] 
[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

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


solvebvasint
[off  sum  iand  bv  bitwise
, defaultoff
] 
[experts only]
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 –solbvbvasintgranularity

iand

Translate bvand to the iand operator (experimental)

bv

Translate bvand back to bitvectors

bitwise

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


solveintasbv
[typeuint64_t
, 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)

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
, defaultconstant
] 
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

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

stringseager
[typebool
, defaultfalse
] (alsono*
) 
[experts only]
strings eager check

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

stringseagerlen
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
strings eager length lemmas

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

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

stringsminprefixexplain
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
minimize explanations for prefix of normal forms in strings

stringsmodelmaxlen
[typeuint64_t
, 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.


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

stringsunifiedvspt
[typebool
, defaulttrue
] (alsono*
) 
[experts only]
use a single skolem for the variable splitting rule
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.


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

symmetrybreaker
[typebool
, defaulttrue
] (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
, defaultfalse
] (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