Skip to main content

Parameters

Z3 Options

Global Parameters

ParameterTypeDescriptionDefault
auto_configbooluse heuristics to automatically select solver and configure ittrue
debug_ref_countbooldebug support for AST reference countingfalse
dot_proof_filestringfile in which to output graphical proofsproof.dot
dump_modelsbooldump models whenever check-sat returns satfalse
encodingstringstring encoding used internally: unicodebmp
memory_high_watermarkunsigned intset high watermark for memory consumption (in bytes), if 0 then there is no limit0
memory_high_watermark_mbunsigned intset high watermark for memory consumption (in megabytes), if 0 then there is no limit0
memory_max_alloc_countunsigned intset hard upper limit for memory allocations, if 0 then there is no limit0
memory_max_sizeunsigned intset hard upper limit for memory consumption (in megabytes), if 0 then there is no limit0
modelboolmodel generation for solvers, this parameter can be overwritten when creating a solvertrue
model_validateboolvalidate models produced by solversfalse
proofboolproof generation, it must be enabled when the Z3 context is createdfalse
rlimitunsigned intdefault resource limit used for solvers. Unrestricted when set to 0.0
smtlib2_compliantboolenable/disable SMT-LIB 2.0 compliancefalse
statsboolenable/disable statisticsfalse
timeoutunsigned int(default: infty) timeout in milliseconds.4294967295
tracebooltrace generation for VCCfalse
trace_file_namestringtrace out file name (see option 'trace')z3.log
type_checkbooltype checker (alias for well_sorted_check)true
unsat_coreboolunsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generationfalse
verboseunsigned intbe verbose, where the value is the verbosity level0
warningboolenable/disable warning messagestrue
well_sorted_checkbooltype checkerfalse

pi

pattern inference (heuristics) for universal formulas (without annotation)

ParameterTypeDescriptionDefault
arithunsigned int0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms1
arith_weightunsigned intdefault weight for quantifiers where the only available pattern has nested arithmetic terms5
block_loop_patternsboolblock looping patterns during pattern inferencetrue
max_multi_patternsunsigned intwhen patterns are not provided, the prover uses a heuristic to infer them, this option sets the threshold on the number of extra multi-patterns that can be created; by default, the prover creates at most one multi-pattern when there is no unary pattern0
non_nested_arith_weightunsigned intdefault weight for quantifiers where the only available pattern has non nested arithmetic terms10
pull_quantifiersboolpull nested quantifiers, if no pattern was foundtrue
use_databasebooluse pattern databasefalse
warningsboolenable/disable warning messages in the pattern inference modulefalse

tactic

tactic parameters

ParameterTypeDescriptionDefault
blast_term_ite.max_inflationunsigned intmultiplicative factor of initial term size.4294967295
blast_term_ite.max_stepsunsigned intmaximal number of steps allowed for tactic.4294967295
default_tacticsymboloverwrite default tactic in strategic solver
propagate_values.max_roundsunsigned intmaximal number of rounds to propagate values.4
solve_eqs.context_solveboolsolve equalities within disjunctions.true
solve_eqs.ite_solverbooluse if-then-else solvers.true
solve_eqs.max_occsunsigned intmaximum number of occurrences for considering a variable for Gaussian eliminations.4294967295
solve_eqs.theory_solverbooluse theory solvers.true

pp

pretty printer

ParameterTypeDescriptionDefault
boundedboolignore characters exceeding max widthfalse
bv_literalsbooluse Bit-Vector literals (e.g, #x0F and #b0101) during pretty printingtrue
bv_negbooluse bvneg when displaying Bit-Vector literals where the most significant bit is 1false
decimalboolpretty print real numbers using decimal notation (the output may be truncated). Z3 adds a ? if the value is not precisefalse
decimal_precisionunsigned intmaximum number of decimal places to be used when pp.decimal=true10
fixed_indentbooluse a fixed indentation for applicationsfalse
flat_assocboolflat associative operators (when pretty printing SMT2 terms/formulas)true
fp_real_literalsbooluse real-numbered floating point literals (e.g, +1.0p-1) during pretty printingfalse
max_depthunsigned intmax. term depth (when pretty printing SMT2 terms/formulas)5
max_indentunsigned intmax. indentation in pretty printer4294967295
max_num_linesunsigned intmax. number of lines to be displayed in pretty printer4294967295
max_ribbonunsigned intmax. ribbon (width - indentation) in pretty printer80
max_widthunsigned intmax. width in pretty printer80
min_alias_sizeunsigned intmin. size for creating an alias for a shared term (when pretty printing SMT2 terms/formulas)10
pretty_proofbooluse slower, but prettier, printer for proofsfalse
simplify_impliesboolsimplify nested implications for pretty printingtrue
single_lineboolignore line breaks when truefalse

sat

propositional SAT solver

ParameterTypeDescriptionDefault
abcebooleliminate blocked clauses using asymmetric literalsfalse
accebooleliminate covered clauses using asymmetric added literalsfalse
anfboolenable ANF based simplification in-processingfalse
anf.delayunsigned intdelay ANF simplification by in-processing round2
anf.exlinboolenable extended linear simplificationfalse
asymm_branchboolasymmetric branchingtrue
asymm_branch.allboolasymmetric branching on all literals per clausefalse
asymm_branch.delayunsigned intnumber of simplification rounds to wait until invoking asymmetric branch simplification1
asymm_branch.limitunsigned intapprox. maximum number of literals visited during asymmetric branching100000000
asymm_branch.roundsunsigned intmaximal number of rounds to run asymmetric branch simplifications if progress is made2
asymm_branch.sampledbooluse sampling based asymmetric branching based on binary implication graphtrue
ateboolasymmetric tautology eliminationtrue
backtrack.conflictsunsigned intnumber of conflicts before enabling chronological backtracking4000
backtrack.scopesunsigned intnumber of scopes to enable chronological backtracking100
bcaboolblocked clause addition - add blocked binary clausesfalse
bcebooleliminate blocked clausesfalse
bce_atunsigned inteliminate blocked clauses only once at the given simplification round2
bce_delayunsigned intdelay eliminate blocked clauses until simplification round2
binsprboolenable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates modelsfalse
blocked_clause_limitunsigned intmaximum number of literals visited during blocked clause elimination100000000
branching.anti_explorationboolapply anti-exploration heuristic for branch selectionfalse
branching.heuristicsymbolbranching heuristic vsids, chbvsids
burst_searchunsigned intnumber of conflicts before first global simplification100
cardinality.encodingsymbolencoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuitgrouped
cardinality.solverbooluse cardinality solvertrue
ccebooleliminate covered clausesfalse
core.minimizeboolminimize computed corefalse
core.minimize_partialboolapply partial (cheap) core minimizationfalse
cutboolenable AIG based simplification in-processingfalse
cut.aigboolextract aigs (and ites) from clauses for cut simplificationfalse
cut.delayunsigned intdelay cut simplification by in-processing round2
cut.dont_caresboolintegrate dont cares with cutstrue
cut.forceboolforce redoing cut-enumeration until a fixed-pointfalse
cut.lutboolextract luts from clauses for cut simplificationfalse
cut.npn3boolextract 3 input functions from clauses for cut simplificationfalse
cut.redundanciesboolintegrate redundancy checking of cutstrue
cut.xorboolextract xors from clauses for cut simplificationfalse
ddfw.init_clause_weightunsigned intinitial clause weight for DDFW local search8
ddfw.reinit_baseunsigned intincrement basis for geometric backoff scheme of re-initialization of weights10000
ddfw.restart_baseunsigned intnumber of flips used a starting point for hesitant restart backoff100000
ddfw.threadsunsigned intnumber of ddfw threads to run in parallel with sat solver0
ddfw.use_reward_pctunsigned intpercentage to pick highest reward variable when it has reward 015
ddfw_searchbooluse ddfw local search instead of CDCLfalse
dimacs.coreboolextract core from DIMACS benchmarksfalse
drat.activitybooldump variable activitiesfalse
drat.binarybooluse Binary DRAT output formatfalse
drat.check_satboolbuild up internal trace, check satisfying modelfalse
drat.check_unsatboolbuild up internal proof and checkfalse
drat.disablebooloverride anything that enables DRATfalse
drat.filesymbolfile to dump DRAT proofs
dyn_sub_resbooldynamic subsumption resolution for minimizing learned clausestrue
elim_varsboolenable variable elimination using resolution during simplificationtrue
elim_vars_bddboolenable variable elimination using BDD recompilation during simplificationtrue
elim_vars_bdd_delayunsigned intdelay elimination of variables using BDDs until after simplification round3
enable_pre_simplifyboolenable pre simplifications before the bounded searchfalse
eufboolenable euf solver (this feature is preliminary and not ready for general consumption)false
force_cleanupboolforce cleanup to remove tautologies and simplify clausesfalse
gcsymbolgarbage collection strategy: psm, glue, glue_psm, dyn_psmglue_psm
gc.burstboolperform eager garbage collection during initializationfalse
gc.defragbooldefragment clauses when garbage collectingtrue
gc.incrementunsigned intincrement to the garbage collection threshold500
gc.initialunsigned intlearned clauses garbage collection frequency20000
gc.kunsigned intlearned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)7
gc.small_lbdunsigned intlearned clauses with small LBD are never deleted (only used in dyn_psm)3
inprocess.maxunsigned intmaximal number of inprocessing passes4294967295
inprocess.outsymbolfile to dump result of the first inprocessing step and exit
local_searchbooluse local search instead of CDCLfalse
local_search_dbg_flipsboolwrite debug information for number of flipsfalse
local_search_modesymbollocal search algorithm, either default wsat or qsatwsat
local_search_threadsunsigned intnumber of local search threads to find satisfiable solution0
lookahead.cube.cutoffsymbolcutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psatdepth
lookahead.cube.depthunsigned intcut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.1
lookahead.cube.fractiondoubleadaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat0.4
lookahead.cube.freevarsdoublecube free variable fraction. Used when lookahead.cube.cutoff is freevars0.8
lookahead.cube.psat.clause_basedoubleclause base for PSAT cutoff2
lookahead.cube.psat.triggerdoubletrigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat5
lookahead.cube.psat.var_expdoublefree variable exponent for PSAT cutoff1
lookahead.delta_fractiondoublenumber between 0 and 1, the smaller the more literals are selected for double lookahead1.0
lookahead.doubleboolenable double lookaheadtrue
lookahead.global_autarkyboolprefer to branch on variables that occur in clauses that are reducedfalse
lookahead.preselectbooluse pre-selection of subset of variables for branchingfalse
lookahead.rewardsymbolselect lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cumarch_cu
lookahead.use_learnedbooluse learned clauses when selecting lookahead literalfalse
lookahead_scoresboolextract lookahead scores. A utility that can only be used from the DIMACS front-endfalse
lookahead_simplifybooluse lookahead solver during simplificationfalse
lookahead_simplify.bcabooladd learned binary clauses as part of lookahead simplificationtrue
max_conflictsunsigned intmaximum number of conflicts4294967295
max_memoryunsigned intmaximum amount of memory in megabytes4294967295
minimize_lemmasboolminimize learned clausestrue
override_incrementalbooloverride incremental safety gaps. Enable elimination of blocked clauses and variables even if solver is reusedfalse
pb.lemma_formatsymbolgenerate either cardinality or pb lemmascardinality
pb.min_arityunsigned intminimal arity to compile pb/cardinality constraints to CNF9
pb.resolvesymbolresolution strategy for boolean algebra solver: cardinality, roundingcardinality
pb.solversymbolmethod for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), binary_merge, segmented, solver (use native solver)solver
phasesymbolphase selection strategy: always_false, always_true, basic_caching, random, cachingcaching
phase.stickybooluse sticky phase cachingtrue
prob_searchbooluse probsat local search instead of CDCLfalse
probingboolapply failed literal detection during simplificationtrue
probing_binaryboolprobe binary clausestrue
probing_cachebooladd binary literals as lemmastrue
probing_cache_limitunsigned intcache binaries unless overall memory usage exceeds cache limit1024
probing_limitunsigned intlimit to the number of probe calls5000000
propagate.prefetchboolprefetch watch lists for assigned literalstrue
random_freqdoublefrequency of random case splits0.01
random_seedunsigned intrandom seed0
reorder.activity_scaleunsigned intscaling factor for activity update100
reorder.baseunsigned intnumber of conflicts per random reorder4294967295
reorder.itaudoubleinverse temperature for softmax4.0
rephase.baseunsigned intnumber of conflicts per rephase1000
resolution.cls_cutoff1unsigned intlimit1 - total number of problems clauses for the second cutoff of Boolean variable elimination100000000
resolution.cls_cutoff2unsigned intlimit2 - total number of problems clauses for the second cutoff of Boolean variable elimination700000000
resolution.limitunsigned intapprox. maximum number of literals visited during variable elimination500000000
resolution.lit_cutoff_range1unsigned intsecond cutoff (total number of literals) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses700
resolution.lit_cutoff_range2unsigned intsecond cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2400
resolution.lit_cutoff_range3unsigned intsecond cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff2300
resolution.occ_cutoffunsigned intfirst cutoff (on number of positive/negative occurrences) for Boolean variable elimination10
resolution.occ_cutoff_range1unsigned intsecond cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses8
resolution.occ_cutoff_range2unsigned intsecond cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff25
resolution.occ_cutoff_range3unsigned intsecond cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff23
restartsymbolrestart strategy: static, luby, ema or geometricema
restart.emafastgluedoubleema alpha factor for fast moving average0.03
restart.emaslowgluedoubleema alpha factor for slow moving average1e-05
restart.factordoublerestart increment factor for geometric strategy1.5
restart.fastbooluse fast restart approach only removing less active literals.true
restart.initialunsigned intinitial restart (number of conflicts)2
restart.margindoublemargin between fast and slow restart factors. For ema1.1
restart.maxunsigned intmaximal number of restarts.4294967295
retain_blocked_clausesboolretain blocked clauses as lemmastrue
sccbooleliminate Boolean variables by computing strongly connected componentstrue
scc.trboolapply transitive reduction, eliminate redundant binary clausestrue
search.sat.conflictsunsigned intperiod for solving for sat (in number of conflicts)400
search.unsat.conflictsunsigned intperiod for solving for unsat (in number of conflicts)400
simplify.delayunsigned intset initial delay of simplification by a conflict count0
smtbooluse the SAT solver based incremental SMT corefalse
smt.proof.checkboolcheck SMT proof while it is createdfalse
smt.proof.check_rupboolapply forward RUP proof checkingtrue
subsumptionbooleliminate subsumed clausestrue
subsumption.limitunsigned intapprox. maximum number of literals visited during subsumption (and subsumption resolution)100000000
threadsunsigned intnumber of parallel threads to use1
variable_decayunsigned intmultiplier (divided by 100) for the VSIDS activity increment110

solver

solver parameters

ParameterTypeDescriptionDefault
axioms2filesboolprint negated theory axioms to separate files during searchfalse
cancel_backup_filesymbolfile to save partial search state if search is canceled
instantiations2consoleboolprint quantifier instantiations to the consolefalse
lemmas2consoleboolprint lemmas during searchfalse
proof.checkboolcheck proof logstrue
proof.logsymbollog clause proof trail into a file
proof.saveboolsave proof log into a proof object that can be extracted using (get-proof)false
proof.trimbooltrim and save proof into a proof object that an be extracted using (get-proof)false
smtlib2_logsymbolfile to save solver interaction
timeoutunsigned inttimeout on the solver object; overwrites a global timeout4294967295

opt

optimization parameters

ParameterTypeDescriptionDefault
dump_benchmarksbooldump benchmarks for profilingfalse
dump_modelsbooldisplay intermediary models to stdoutfalse
elim_01booleliminate 01 variablestrue
enable_core_rotateboolenable core rotation to both sample cores and correction setsfalse
enable_lnsboolenable LNS during weighted maxsatfalse
enable_satboolenable the new SAT core for propositional constraintstrue
enable_slsboolenable SLS tuning during weighted maxsatfalse
incrementalboolset incremental mode. It disables pre-processing and enables adding constraints in model event handlerfalse
lns_conflictsunsigned intinitial conflict count for LNS search1000
maxlex.enableboolenable maxlex heuristic for lexicographic MaxSAT problemstrue
maxres.add_upper_bound_blockboolrestrict upper bound with constraintfalse
maxres.hill_climbboolgive preference for large weight corestrue
maxres.max_core_sizeunsigned intbreak batch of generated cores if size reaches this number3
maxres.max_correction_set_sizeunsigned intallow generating correction set constraints up to maximal size3
maxres.max_num_coresunsigned intmaximal number of cores per round200
maxres.maximize_assignmentboolfind an MSS/MCS to improve current assignmentfalse
maxres.pivot_on_correction_setboolreduce soft constraints if the current correction set is smaller than current coretrue
maxres.wmaxbooluse weighted theory solver to constrain upper boundsfalse
maxsat_enginesymbolselect engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'maxres-bin', 'rc2'maxres
optsmt_enginesymbolselect optimization engine: 'basic', 'symba'basic
pb.compile_equalityboolcompile arithmetical equalities into pseudo-Boolean equality (instead of two inequalities)false
pp.neatbooluse neat (as opposed to less readable, but faster) pretty printer when displaying contexttrue
pp.wcnfboolprint maxsat benchmark into wcnf formatfalse
prioritysymbolselect how to prioritize objectives: 'lex' (lexicographic), 'pareto', 'box'lex
rc2.totalizerbooluse totalizer for rc2 encodingtrue
rlimitunsigned intresource limit (0 means no limit)0
solution_prefixsymbolpath prefix to dump intermediary, but non-optimal, solutions
timeoutunsigned inttimeout (in milliseconds) (UINT_MAX and 0 mean no timeout)4294967295

parallel

parameters for parallel solver

ParameterTypeDescriptionDefault
conquer.backtrack_frequencyunsigned intfrequency to apply core minimization during conquer10
conquer.batch_sizeunsigned intnumber of cubes to batch together for fast conquer100
conquer.delayunsigned intdelay of cubes until applying conquer10
conquer.restart.maxunsigned intmaximal number of restarts during conquer phase5
enableboolenable parallel solver by default on selected tactics (for QF_BV)false
simplify.expdoublerestart and inprocess max is multiplied by simplify.exp ^ depth1
simplify.inprocess.maxunsigned intmaximal number of inprocessing steps during simplification2
simplify.max_conflictsunsigned intmaximal number of conflicts during simplification phase4294967295
simplify.restart.maxunsigned intmaximal number of restarts during simplification phase5000
threads.maxunsigned intcaps maximal number of threads below the number of processors10000

nnf

negation normal form

ParameterTypeDescriptionDefault
ignore_labelsboolremove/ignore labels in the input formula, this option is ignored if proofs are enabledfalse
max_memoryunsigned intmaximum amount of memory in megabytes4294967295
modesymbolNNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), fullskolem
sk_hackboolhack for VCCfalse

algebraic

real algebraic number package. Non-default parameter settings are not supported

ParameterTypeDescriptionDefault
factorbooluse polynomial factorization to simplify polynomials representing algebraic numberstrue
factor_max_primeunsigned intparameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step31
factor_num_primesunsigned intparameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifting and searching1
factor_search_sizeunsigned intparameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space5000
min_magunsigned intZ3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^1616
zero_accuracyunsigned intone of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k)0

combined_solver

combines two solvers: non-incremental (solver1) and incremental (solver2)

ParameterTypeDescriptionDefault
ignore_solver1boolif true, solver 2 is always usedfalse
solver2_timeoutunsigned intfallback to solver 1 after timeout even when in incremental model4294967295
solver2_unknownunsigned intwhat should be done when solver 2 returns unknown: 0 - just return unknown, 1 - execute solver 1 if quantifier free problem, 2 - execute solver 11

rcf

real closed fields

ParameterTypeDescriptionDefault
clean_denominatorsboolclean denominators before root isolationtrue
inf_precisionunsigned inta value k that is the initial interval size (i.e., (0, 1/2^l)) used as an approximation for infinitesimal values24
initial_precisionunsigned inta value k that is the initial interval size (as 1/2^k) when creating transcendentals and approximated division24
lazy_algebraic_normalizationboolduring sturm-seq and square-free polynomial computations, only normalize algebraic polynomial expressions when the defining polynomial is monictrue
max_precisionunsigned intduring sign determination we switch from interval arithmetic to complete methods when the interval size is less than 1/2^k, where k is the max_precision128
use_prembooluse pseudo-remainder instead of remainder when computing GCDs and Sturm-Tarski sequencestrue

ackermannization

solving UF via ackermannization

ParameterTypeDescriptionDefault
eagerbooleagerly instantiate all congruence rulestrue
inc_sat_backendbooluse incremental SATfalse
sat_backendbooluse SAT rather than SMT in qfufbv_ackr_tacticfalse

nlsat

nonlinear solver

ParameterTypeDescriptionDefault
check_lemmasboolcheck lemmas on the fly using an independent nlsat solverfalse
factorboolfactor polynomials produced during conflict resolution.true
inline_varsboolinline variables that can be isolated from equations (not supported in incremental mode)false
lazyunsigned inthow lazy the solver is.0
log_lemmasbooldisplay lemmas as self-contained SMT formulasfalse
max_conflictsunsigned intmaximum number of conflicts.4294967295
max_memoryunsigned intmaximum amount of memory in megabytes4294967295
minimize_conflictsboolminimize conflictsfalse
randomizeboolrandomize selection of a witness in nlsat.true
reorderboolreorder variables.true
seedunsigned intrandom seed.0
shuffle_varsbooluse a random variable order.false
simplify_conflictsboolsimplify conflicts using equalities before resolving them in nlsat solver.true

fp

fixedpoint parameters

ParameterTypeDescriptionDefault
bmc.linear_unrolling_depthunsigned intMaximal level to explore4294967295
datalog.all_or_nothing_deltasboolcompile rules so that it is enough for the delta relation in union and widening operations to determine only whether the updated relation was modified or notfalse
datalog.check_relationsymbolname of default relation to check. operations on the default relation will be verified using SMT solvingnull
datalog.compile_with_wideningboolwidening will be used to compile recursive rulesfalse
datalog.dbg_fpr_nonempty_relation_signatureboolif true, finite_product_relation will attempt to avoid creating inner relation with empty signature by putting in half of the table columns, if it would have been empty otherwisefalse
datalog.default_relationsymboldefault relation implementation: external_relation, pentagonpentagon
datalog.default_tablesymboldefault table implementation: sparse, hashtable, bitvector, intervalsparse
datalog.default_table_checkedboolif true, the default table will be default_table inside a wrapper that checks that its results are the same as of default_table_checker tablefalse
datalog.default_table_checkersymbolsee default_table_checkednull
datalog.explanations_on_relation_levelboolif true, explanations are generated as history of each relation, rather than per fact (generate_explanations must be set to true for this option to have any effect)false
datalog.generate_explanationsboolproduce explanations for produced facts when using the datalog enginefalse
datalog.initial_restart_timeoutunsigned intlength of saturation run before the first restart (in ms), zero means no restarts0
datalog.magic_sets_for_queriesboolmagic set transformation will be used for queriesfalse
datalog.output_profilebooldetermines whether profile information should be output when outputting Datalog rules or instructionsfalse
datalog.print.tuplesbooldetermines whether tuples for output predicates should be outputtrue
datalog.profile_timeout_millisecondsunsigned intinstructions and rules that took less than the threshold will not be printed when printed the instruction/rule list0
datalog.similarity_compressorboolrules that differ only in values of constants will be merged into a single ruletrue
datalog.similarity_compressor_thresholdunsigned intif similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged11
datalog.subsumptionboolif true, removes/filters predicates with total transitionstrue
datalog.timeoutunsigned intTime limit used for saturation0
datalog.unbound_compressorboolauxiliary relations will be introduced to avoid unbound variables in rule headstrue
datalog.use_map_namesbooluse names from map files when displaying tuplestrue
enginesymbolSelect: auto-config, datalog, bmc, spacerauto-config
generate_proof_tracebooltrace for 'sat' answer as proof objectfalse
print_aigsymbolDump clauses in AIG text format (AAG) to the given file name
print_answerboolprint answer instance(s) to queryfalse
print_boogie_certificateboolprint certificate for reachability or non-reachability using a format understood by Boogiefalse
print_certificateboolprint certificate for reachability or non-reachabilityfalse
print_fixedpoint_extensionsbooluse SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rulestrue
print_low_level_smt2booluse (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)false
print_statisticsboolprint statisticsfalse
print_with_variable_declarationsbooluse variable declarations when displaying rules (instead of attempting to use original names)true
spacer.arith.solverunsigned intarithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver2
spacer.blast_term_ite_inflationunsigned intMaximum inflation for non-Boolean ite-terms expansion: 0 (none), k (multiplicative)3
spacer.ctpboolEnable counterexample-to-pushingtrue
spacer.dump_benchmarksboolDump SMT queries as benchmarksfalse
spacer.dump_thresholddoubleThreshold in seconds on dumping benchmarks5.0
spacer.elim_auxboolEliminate auxiliary variables in reachability factstrue
spacer.eq_propboolEnable equality and bound propagation in arithmetictrue
spacer.expand_bndboolEnable expand-bound lemma generalizationfalse
spacer.gg.concretizeboolEnable global guidance concretizetrue
spacer.gg.conjectureboolEnable global guidance conjecturetrue
spacer.gg.subsumeboolEnable global guidance subsumetrue
spacer.globalboolEnable global guidancefalse
spacer.gpdrboolUse GPDR solving strategy for non-linear CHCfalse
spacer.gpdr.bfsboolUse BFS exploration strategy for expanding model searchtrue
spacer.ground_pobsboolGround pobs by using values from a modeltrue
spacer.iucunsigned int0 = use old implementation of unsat-core-generation, 1 = use new implementation of IUC generation, 2 = use new implementation of IUC + min-cut optimization1
spacer.iuc.arithunsigned int0 = use simple Farkas plugin, 1 = use simple Farkas plugin with constant from other partition (like old unsat-core-generation),2 = use Gaussian elimination optimization (broken), 3 = use additive IUC plugin1
spacer.iuc.debug_proofboolprints proof used by unsat-core-learner for debugging purposes (debugging)false
spacer.iuc.old_hyp_reducerbooluse old hyp reducer instead of new implementation, for debugging onlyfalse
spacer.iuc.print_farkas_statsboolprints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging)false
spacer.iuc.split_farkas_literalsboolSplit Farkas literalsfalse
spacer.keep_proxyboolkeep proxy variables (internal parameter)true
spacer.logicsymbolSMT-LIB logic to configure internal SMT solvers
spacer.max_levelunsigned intMaximum level to explore4294967295
spacer.max_num_contextsunsigned intmaximal number of contexts to create500
spacer.mbqiboolEnable mbqitrue
spacer.min_levelunsigned intMinimal level to explore0
spacer.native_mbpboolUse native mbp of Z3true
spacer.order_childrenunsigned intSPACER: order of enqueuing children in non-linear rules : 0 (original), 1 (reverse), 2 (random)0
spacer.p3.share_invariantsboolShare invariants lemmasfalse
spacer.p3.share_lemmasboolShare frame lemmasfalse
spacer.propagateboolEnable propagate/pushing phasetrue
spacer.push_pobboolpush blocked pobs to higher levelfalse
spacer.push_pob_max_depthunsigned intMaximum depth at which push_pob is enabled4294967295
spacer.q3boolAllow quantified lemmas in framestrue
spacer.q3.instantiateboolInstantiate quantified lemmastrue
spacer.q3.qgen.normalizeboolnormalize cube before quantified generalizationtrue
spacer.q3.use_qgenbooluse quantified lemma generalizerfalse
spacer.random_seedunsigned intRandom seed to be used by SMT solver0
spacer.reach_dnfboolRestrict reachability facts to DNFtrue
spacer.reset_pob_queueboolSPACER: reset pob obligation queue when entering a new leveltrue
spacer.restart_initial_thresholdunsigned intInitial threshold for restarts10
spacer.restartsboolEnable resetting obligation queuefalse
spacer.simplify_lemmas_postboolsimplify derived lemmas after inductive propagationfalse
spacer.simplify_lemmas_preboolsimplify derived lemmas before inductive propagationfalse
spacer.simplify_pobboolsimplify pobs by removing redundant constraintsfalse
spacer.trace_filesymbolLog file for progress events
spacer.use_array_eq_generalizerboolSPACER: attempt to generalize lemmas with array equalitiestrue
spacer.use_bg_invsboolEnable external background invariantsfalse
spacer.use_derivationsboolSPACER: using derivation mechanism to cache intermediate results for non-linear rulestrue
spacer.use_euf_genboolGeneralize lemmas and pobs using implied equalitiesfalse
spacer.use_inc_clauseboolUse incremental clause to represent transtrue
spacer.use_inductive_generalizerboolgeneralize lemmas using induction strengtheningtrue
spacer.use_iucboolEnable Interpolating Unsat Core(IUC) for lemma generalizationtrue
spacer.use_lemma_as_ctiboolSPACER: use a lemma instead of a CTI in flexible_tracefalse
spacer.use_lim_num_genboolEnable limit numbers generalizer to get smaller numbersfalse
spacer.validate_lemmasboolValidate each lemma after generalizationfalse
spacer.weak_absboolWeak abstractiontrue
tab.selectionsymbolselection method for tabular strategy: weight (default), first, var-useweight
validateboolvalidate result (by proof checking or model checking)false
xform.array_blastbooltry to eliminate local array terms using Ackermannization -- some array terms may remainfalse
xform.array_blast_fullbooleliminate all local array variables by QEfalse
xform.bit_blastboolbit-blast bit-vectorsfalse
xform.coalesce_rulesboolcoalesce rulesfalse
xform.coibooluse cone of influence simplificationtrue
xform.compress_unboundboolcompress tails with unbound variablestrue
xform.elim_term_iteboolEliminate term-ite expressionsfalse
xform.elim_term_ite.inflationunsigned intMaximum inflation for non-Boolean ite-terms blasting: 0 (none), k (multiplicative)3
xform.fix_unbound_varsboolfix unbound variables in tailfalse
xform.inline_eagerbooltry eager inlining of rulestrue
xform.inline_linearbooltry linear inlining methodtrue
xform.inline_linear_branchbooltry linear inlining method with potential expansionfalse
xform.instantiate_arraysboolTransforms P(a) into P(i, a[i] a)false
xform.instantiate_arrays.enforceboolTransforms P(a) into P(i, a[i]), discards a from predicatefalse
xform.instantiate_arrays.nb_quantifierunsigned intGives the number of quantifiers per array1
xform.instantiate_arrays.slice_techniquesymbol<no-slicing>=> GetId(i) = i, <smash> => GetId(i) = trueno-slicing
xform.instantiate_quantifiersboolinstantiate quantified Horn clauses using E-matching heuristicfalse
xform.magicboolperform symbolic magic set transformationfalse
xform.quantify_arraysboolcreate quantified Horn clauses from clauses with arraysfalse
xform.scalebooladd scaling variable to linear real arithmetic clausesfalse
xform.sliceboolsimplify clause set using slicingtrue
xform.subsumption_checkerboolEnable subsumption checker (no support for model conversion)true
xform.tail_simplifier_pveboolpropagate_variable_equivalencestrue
xform.transform_arraysboolRewrites arrays equalities and applies select over storefalse
xform.unfold_rulesunsigned intunfold rules statically using iterative squaring0

smt

smt solver based on lazy smt

ParameterTypeDescriptionDefault
arith.auto_config_simplexboolforce simplex solver in auto_configfalse
arith.bprop_on_pivoted_rowsboolpropagate bounds on rows changed by the pivot operationtrue
arith.branch_cut_ratiounsigned intbranch/cut ratio for linear integer arithmetic2
arith.dump_lemmasbooldump arithmetic theory lemmas to filesfalse
arith.eager_eq_axiomsbooleager equality axiomstrue
arith.enable_hnfboolenable hnf (Hermite Normal Form) cutstrue
arith.greatest_error_pivotboolPivoting strategyfalse
arith.ignore_intbooltreat integer variables as realfalse
arith.int_eq_branchboolbranching using derived integer equationsfalse
arith.minboolminimize costfalse
arith.nlbool(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2true
arith.nl.branchingboolbranching on integer variables in non linear clusters, relevant only if smt.arith.solver=2true
arith.nl.delayunsigned intnumber of calls to final check before invoking bounded nlsat check500
arith.nl.exppboolexpensive patchingfalse
arith.nl.gr_qunsigned intgrobner's quota10
arith.nl.grobnerboolrun grobner's basis heuristictrue
arith.nl.grobner_cnfl_to_reportunsigned intgrobner's maximum number of conflicts to report1
arith.nl.grobner_eqs_growthunsigned intgrobner's number of equalities growth10
arith.nl.grobner_expr_degree_growthunsigned intgrobner's maximum expr degree growth2
arith.nl.grobner_expr_size_growthunsigned intgrobner's maximum expr size growth2
arith.nl.grobner_frequencyunsigned intgrobner's call frequency4
arith.nl.grobner_max_simplifiedunsigned intgrobner's maximum number of simplifications10000
arith.nl.grobner_subs_fixedunsigned int0 - no subs, 1 - substitute, 2 - substitute fixed zeros only1
arith.nl.hornerboolrun horner's heuristictrue
arith.nl.horner_frequencyunsigned inthorner's call frequency4
arith.nl.horner_row_length_limitunsigned introw is disregarded by the heuristic if its length is longer than the value10
arith.nl.horner_subs_fixedunsigned int0 - no subs, 1 - substitute, 2 - substitute fixed zeros only2
arith.nl.nraboolcall nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6true
arith.nl.orderboolrun order lemmastrue
arith.nl.roundsunsigned intthreshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=21024
arith.nl.tangentsboolrun tangent lemmastrue
arith.print_ext_var_namesboolprint external variable namesfalse
arith.print_statsboolprint statisticfalse
arith.propagate_eqsboolpropagate (cheap) equalitiestrue
arith.propagation_modeunsigned int0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds1
arith.random_initial_valuebooluse random initial values in the simplex-based procedure for linear arithmeticfalse
arith.rep_frequnsigned intthe report frequency, in how many iterations print the cost and other info0
arith.simplex_strategyunsigned intsimplex strategy for the solver0
arith.solverunsigned intarithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver6
array.extensionalboolextensional array theorytrue
array.weakboolweak array theoryfalse
auto_configboolautomatically configure solvertrue
bv.delaybooldelay internalize expensive bit-vector operationsfalse
bv.enable_int2bvboolenable support for int2bv and bv2int operatorstrue
bv.eq_axiomsboolenable redundant equality axioms for bit-vectorstrue
bv.reflectboolcreate enode for every bit-vector termtrue
bv.size_reduceboolpre-processing; turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constantfalse
bv.watch_diseqbooluse watch lists instead of eager axioms for bit-vectorsfalse
candidate_modelsboolcreate candidate models even when quantifier or theory reasoning is incompletefalse
case_splitunsigned int0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity1
clause_proofboolrecord a clausal prooffalse
core.extend_nonlocal_patternsboolextend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier's bodyfalse
core.extend_patternsboolextend unsat core with literals that trigger (potential) quantifier instancesfalse
core.extend_patterns.max_distanceunsigned intlimits the distance of a pattern-extended unsat core4294967295
core.minimizeboolminimize unsat core produced by SMT contextfalse
core.validatebool[internal] validate unsat core produced by SMT context. This option is intended for debuggingfalse
cube_depthunsigned intcube depth.1
dackunsigned int0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution1
dack.eqboolenable dynamic ackermannization for transitivity of equalitiesfalse
dack.factordoublenumber of instance per conflict0.1
dack.gcunsigned intDynamic ackermannization garbage collection frequency (per conflict)2000
dack.gc_inv_decaydoubleDynamic ackermannization garbage collection decay0.8
dack.thresholdunsigned intnumber of times the congruence rule must be used before Leibniz's axiom is expanded10
delay_unitsboolif true then z3 will not restart when a unit clause is learnedfalse
delay_units_thresholdunsigned intmaximum number of learned unit clauses before restarting, ignored if delay_units is false32
dt_lazy_splitsunsigned intHow lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy1
elim_unconstrainedboolpre-processing: eliminate unconstrained subtermstrue
ematchingboolE-Matching based quantifier instantiationtrue
inductionboolenable generation of induction lemmasfalse
lemma_gc_strategyunsigned intlemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none0
logicsymbollogic used to setup the SMT solver
macro_finderbooltry to find universally quantified formulas that can be viewed as macrosfalse
max_conflictsunsigned intmaximum number of conflicts before giving up.4294967295
mbqiboolmodel based quantifier instantiation (MBQI)true
mbqi.force_templateunsigned intsome quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template10
mbqi.idstringOnly use model-based instantiation for quantifiers with id's beginning with string
mbqi.max_cexsunsigned intinitial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation1
mbqi.max_cexs_incrunsigned intincrement for MBQI_MAX_CEXS, the increment is performed after each round of MBQI0
mbqi.max_iterationsunsigned intmaximum number of rounds of MBQI1000
mbqi.traceboolgenerate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfiedfalse
pb.conflict_frequencyunsigned intconflict frequency for Pseudo-Boolean theory1000
pb.learn_complementsboollearn complement literals for Pseudo-Boolean theorytrue
phase_caching_offunsigned intnumber of conflicts while phase caching is off100
phase_caching_onunsigned intnumber of conflicts while phase caching is on400
phase_selectionunsigned intphase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences, 7 - theory3
propagate_valuesboolpre-processing: propagate valuestrue
pull_nested_quantifiersboolpre-processing: pull nested quantifiersfalse
q.lift_iteunsigned int0 - don not lift non-ground if-then-else, 1 - use conservative ite lifting, 2 - use full lifting of if-then-else under quantifiers0
q.liteboolUse cheap quantifier elimination during pre-processingfalse
qi.coststringexpression specifying what is the cost of a given quantifier instantiation(+ weight generation)
qi.eager_thresholddoublethreshold for eager quantifier instantiation10.0
qi.lazy_thresholddoublethreshold for lazy quantifier instantiation20.0
qi.max_instancesunsigned intmaximum number of quantifier instantiations4294967295
qi.max_multi_patternsunsigned intspecify the number of extra multi patterns0
qi.profileboolprofile quantifier instantiationfalse
qi.profile_frequnsigned inthow frequent results are reported by qi.profile4294967295
qi.quick_checkerunsigned intspecify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances0
quasi_macrosbooltry to find universally quantified formulas that are quasi-macrosfalse
random_seedunsigned intrandom seed for the smt solver0
refine_inj_axiomsboolpre-processing: refine injectivity axiomstrue
relevancyunsigned intrelevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant2
restart.maxunsigned intmaximal number of restarts.4294967295
restart_factordoublewhen using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the current restart threshold1.1
restart_strategyunsigned int0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic1
restricted_quasi_macrosbooltry to find universally quantified formulas that are restricted quasi-macrosfalse
seq.max_unfoldingunsigned intmaximal unfolding depth for checking string equations and regular expressions1000000000
seq.min_unfoldingunsigned intinitial bound for strings whose lengths are bounded by iterative deepening. Set this to a higher value if there are only models with larger string lengths1
seq.split_w_lenboolenable splitting guided by length constraintstrue
seq.validateboolenable self-validation of theory axioms created by seq theoryfalse
solve_eqsboolpre-processing: solve equalitiestrue
str.aggressive_length_testingboolprioritize testing concrete length values over generating more optionsfalse
str.aggressive_unroll_testingboolprioritize testing concrete regex unroll counts over generating more optionstrue
str.aggressive_value_testingboolprioritize testing concrete string constant values over generating more optionsfalse
str.fast_length_tester_cacheboolcache length tester constants instead of regenerating themfalse
str.fast_value_tester_cacheboolcache value tester constants instead of regenerating themtrue
str.fixed_length_naive_cexboolconstruct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only)true
str.fixed_length_refinementbooluse abstraction refinement in fixed-length equation solver (Z3str3 only)false
str.overlap_prioritydoubletheory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true-0.1
str.regex_automata_difficulty_thresholdunsigned intdifficulty threshold for regex automata heuristics1000
str.regex_automata_failed_automaton_thresholdunsigned intnumber of failed automaton construction attempts after which a full automaton is automatically built10
str.regex_automata_failed_intersection_thresholdunsigned intnumber of failed automaton intersection attempts after which intersection is always computed10
str.regex_automata_intersection_difficulty_thresholdunsigned intdifficulty threshold for regex intersection heuristics1000
str.regex_automata_length_attempt_thresholdunsigned intnumber of length/path constraint attempts before checking unsatisfiability of regex terms10
str.string_constant_cacheboolcache all generated string constants generated from anywhere in theory_strtrue
str.strong_arrangementsboolassert equivalences instead of implications when generating string arrangement axiomstrue
string_solversymbolsolver for string/sequence theories. options are: 'z3str3' (specialized string solver), 'seq' (sequence solver), 'auto' (use static features to choose best solver), 'empty' (a no-op solver that forces an answer unknown if strings were used), 'none' (no solver)seq
theory_aware_branchingboolAllow the context to use extra information from theory solvers regarding literal branching prioritization.false
theory_case_splitboolAllow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.false
threadsunsigned intmaximal number of parallel threads.1
threads.cube_frequencyunsigned intfrequency for using cubing2
threads.max_conflictsunsigned intmaximal number of conflicts between rounds of cubing for parallel SMT400

sls

Experimental Stochastic Local Search Solver (for QFBV only).

ParameterTypeDescriptionDefault
early_prunebooluse early pruning for score predictiontrue
max_memoryunsigned intmaximum amount of memory in megabytes4294967295
max_restartsunsigned intmaximum number of restarts4294967295
paws_initunsigned intinitial/minimum assertion weights40
paws_spunsigned intsmooth assertion weights with probability paws_sp / 102452
random_offsetbooluse random offset for candidate evaluationtrue
random_seedunsigned intrandom seed0
rescoreboolrescore/normalize top-level score every base restart intervaltrue
restart_baseunsigned intbase restart interval given by moves per run100
restart_initboolinitialize to 0 or random value (= 1) after restartfalse
scale_unsatdoublescale score of unsat expressions by this factor0.5
track_unsatboolkeep a list of unsat assertions as done in SAT - currently disabled internallyfalse
vns_mcunsigned intin local minima, try Monte Carlo sampling vns_mc many 2-bit-flips per bit0
vns_repickboolin local minima, try picking a different assertion (only for walksat)false
walksatbooluse walksat assertion selection (instead of gsat)true
walksat_repickboolrepick assertion if randomizing in local minimatrue
walksat_ucbbooluse bandit heuristic for walksat assertion selection (instead of random)true
walksat_ucb_constantdoublethe ucb constant c in the term score + c * f(touched)20.0
walksat_ucb_forgetdoublescale touched by this factor every base restart interval1.0
walksat_ucb_initboolinitialize total ucb touched to formula sizefalse
walksat_ucb_noisedoubleadd noise 0 <= 256 * ucb_noise to ucb score for assertion selection0.0002
wpunsigned intrandom walk with probability wp / 1024100