From the Arithmetic Theory module:¶

--approx-branch-depth=N

maximum branch depth the approximate solver is allowed to take (EXPERTS only)

--arith-brab

whether to use simple rounding, similar to a unit-cube test, for integers [*]

--arith-eq-solver

whether to use the equality solver in the theory of arithmetic (EXPERTS only) [*]

--arith-exp

enables non-standard extensions of the arithmetic solver (EXPERTS only) [*]

--arith-prop=MODE

turns on arithmetic propagation (default is 'old', see --arith-prop=help) (EXPERTS only)

--arith-prop-clauses=N rows shorter than this are propagated as clauses

(EXPERTS only)

--arith-rewrite-equalities

turns on the preprocessing rewrite turning equalities into a conjunction of inequalities [*]

--arith-static-learning

do arithmetic static learning for ite terms based on bounds when static learning is enabled [*]

--collect-pivot-stats

collect the pivot history (EXPERTS only) [*]

--cut-all-bounded

turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds (EXPERTS only) [*]

--dio-decomps

let skolem variables for integer divisibility constraints leak from the dio solver (EXPERTS only) [*]

--dio-solver

turns on Linear Diophantine Equation solver (Griggio, JSAT 2012) (EXPERTS only) [*]

--dio-turns=N

turns in a row dio solver cutting gets (EXPERTS only)

--error-selection-rule=RULE

change the pivot rule for the basic variable (default is 'min', see --pivot-rule help) (EXPERTS only)

--fc-penalties

turns on degenerate pivot penalties (EXPERTS only) [*]

--heuristic-pivots=N

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 (EXPERTS only)

--lemmas-on-replay-failure

attempt to use external lemmas if approximate solve integer failed (EXPERTS only) [*]

--maxCutsInContext=N

maximum cuts in a given context before signalling a restart (EXPERTS only)

--miplib-trick

turns on the preprocessing step of attempting to infer bounds on miplib problems (EXPERTS only) [*]

--miplib-trick-subs=N

do substitution for miplib 'tmp' vars if defined in <= N eliminated vars (EXPERTS only)

--new-prop

use the new row propagation system (EXPERTS only) [*]

--nl-cov

whether to use the cylindrical algebraic coverings solver for non-linear arithmetic [*]

--nl-cov-force

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

--nl-cov-lift=MODE

choose the Coverings lifting mode (EXPERTS only)

--nl-cov-linear-model=MODE

whether to use the linear model as initial guess for the cylindrical algebraic coverings solver

--nl-cov-proj=MODE

choose the Coverings projection operator (EXPERTS only)

--nl-cov-prune

whether to prune intervals more aggressively (EXPERTS only) [*]

--nl-cov-var-elim

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

--nl-ext=MODE

incremental linearization approach to non-linear

--nl-ext-ent-conf

check for entailed conflicts in non-linear solver (EXPERTS only) [*]

--nl-ext-factor

use factoring inference in non-linear incremental linearization solver [*]

--nl-ext-flatten-mon

use inference schema based on flattening monomials [*]

--nl-ext-inc-prec

whether to increment the precision for irrational function constraints (EXPERTS only) [*]

--nl-ext-purify

purify non-linear terms at preprocess (EXPERTS only) [*]

--nl-ext-rbound

use resolution-style inference for inferring new bounds in non-linear incremental linearization solver (EXPERTS only) [*]

--nl-ext-rewrite

do context-dependent simplification based on rewrites in non-linear solver [*]

--nl-ext-split-zero

initial splits on zero for all variables (EXPERTS only) [*]

--nl-ext-tf-taylor-deg=N

initial degree of polynomials for Taylor approximation (EXPERTS only)

--nl-ext-tf-tplanes

use non-terminating tangent plane strategy for transcendental functions for non-linear incremental linearization solver [*]

--nl-ext-tplanes

use non-terminating tangent plane strategy for non-linear incremental linearization solver [*]

--nl-ext-tplanes-interleave

interleave tangent plane strategy for non-linear incremental linearization solver [*]

--nl-icp

whether to use ICP-style propagations for non-linear arithmetic (EXPERTS only) [*]

--nl-rlv=MODE

choose mode for using relevance of assertions in non-linear arithmetic (EXPERTS only)

--nl-rlv-assert-bounds use bound inference utility to prune when an assertion

is entailed by another (EXPERTS only) [*]

--pb-rewrites

apply pseudo boolean rewrites (EXPERTS only) [*]

--pivot-threshold=N

sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order (EXPERTS only)

--pp-assert-max-sub-size=N

threshold for substituting an equality in ppAssert (EXPERTS only)

--prop-row-length=N

sets the maximum row length to be used in propagation (EXPERTS only)

--replay-early-close-depth=N

multiples of the depths to try to close the approx log eagerly (EXPERTS only)

--replay-lemma-reject-cut=N

maximum complexity of any coefficient while outputting replaying cut lemmas (EXPERTS only)

--replay-num-err-penalty=N

number of solve integer attempts to skips after a numeric failure (EXPERTS only)

--replay-reject-cut=N

maximum complexity of any coefficient while replaying cuts (EXPERTS only)

--restrict-pivots

have a pivot cap for simplex at effort levels below fullEffort (EXPERTS only) [*]

--revert-arith-models-on-unsat

revert the arithmetic model to a known safe model on unsat if one is cached (EXPERTS only) [*]

--rr-turns=N

round robin turn (EXPERTS only)

--se-solve-int

attempt to use the approximate solve integer method on standard effort (EXPERTS only) [*]

--simplex-check-period=N

the number of pivots to do in simplex before rechecking for a conflict on all variables (EXPERTS only)

--soi-qe

use quick explain to minimize the sum of infeasibility conflicts (EXPERTS only) [*]

--standard-effort-variable-order-pivots=N

limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule (EXPERTS only)

--unate-lemmas=MODE

determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help) (EXPERTS only)

--use-approx

attempt to use an approximate solver (EXPERTS only) [*]

--use-fcsimplex

use focusing and converging simplex (FMCAD 2013 submission) (EXPERTS only) [*]

--use-soi

use sum of infeasibility simplex (FMCAD 2013 submission) (EXPERTS only) [*]

From the Arrays Theory module:¶

--arrays-eager-index

turn on eager index splitting for generated array lemmas [*]

--arrays-eager-lemmas

turn on eager lemma generation for arrays (EXPERTS only) [*]

--arrays-exp

enable experimental features in the theory of arrays (EXPERTS only) [*]

--arrays-optimize-linear

turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper) (EXPERTS only) [*]

--arrays-prop=N

propagation effort for arrays: 0 is none, 1 is some, 2 is full (EXPERTS only)

--arrays-reduce-sharing

use model information to reduce size of care graph for arrays (EXPERTS only) [*]

--arrays-weak-equiv

use algorithm from Christ/Hoenicke (SMT 2014) (EXPERTS only) [*]

From the Bags Theory module:¶

--bags

enables the bags solver in applicable logics (EXPERTS only) [*]

From the Base module:¶

--err=erroutput | --diagnostic-output-channel=erroutput

Set the error (or diagnostic) output channel. Writes to stderr for "stderr" or "--", stdout for "stdout" or the given filename otherwise. (EXPERTS only)

--in=input

Set the error (or diagnostic) output channel. Reads from stdin for "stdin" or "--" and the given filename otherwise. (EXPERTS only)

--out=output | --regular-output-channel=output

Set the error (or diagnostic) output channel. Writes to stdout for "stdout" or "--", stderr for "stderr" or the given filename otherwise. (EXPERTS only)

--plugin-notify-sat-clause-in-solve

only inform plugins of SAT clauses when we are in the main solving loop of the SAT solver (EXPERTS only) [*]

--plugin-share-skolems true if we permit sharing theory lemmas and SAT clauses

with skolems (EXPERTS only) [*]

--rweight=VAL=N

set a single resource weight (EXPERTS only)

--safe-mode=MODE

modes for restricting expert options and theories (EXPERTS only)

--stats-every-query

in incremental mode, print stats after every satisfiability or validity query [*]

--trace=TAG | -t TAG

trace something (e.g. -t pushpop), can repeat and may contain wildcards like (e.g. -t theory::*) (EXPERTS only)

From the Bitvector Theory module:¶

--bitblast=MODE

choose bitblasting mode, see --bitblast=help

--bitwise-eq

lift equivalence with one-bit bit-vectors to be boolean operations (EXPERTS only) [*]

--bool-to-bv=MODE

convert booleans to bit-vectors of size 1 at various levels of aggressiveness, see --bool-to-bv=help

--bv-assert-input

assert input assertions on user-level 0 instead of assuming them in the bit-vector SAT solver (EXPERTS only) [*]

--bv-eager-eval

perform eager context-dependent evaluation for applications of bv kinds in the equality engine [*]

--bv-eq-engine

enable equality engine when possible in bitvector theory (EXPERTS only) [*]

--bv-gauss-elim

simplify formula via Gaussian Elimination if applicable (EXPERTS only) [*]

--bv-intro-pow2

introduce bitvector powers of two as a preprocessing pass (EXPERTS only) [*]

--bv-propagate

use bit-vector propagation in the bit-blaster (EXPERTS only) [*]

--bv-rw-extend-eq

enable additional rewrites over zero/sign extend over equalities with constants (useful on BV/2017-Preiner-scholl-smt08) (EXPERTS only) [*]

--bv-sat-solver=MODE

choose which sat solver to use, see --bv-sat-solver=help

--bv-solver=MODE

choose bit-vector solver, see --bv-solver=help

--bv-to-bool

lift bit-vectors of size 1 to booleans when possible [*]

From the Datatypes Theory module:¶

--cdt-bisimilar

do bisimilarity check for co-datatypes (EXPERTS only) [*]

--datatypes-exp

enables reasoning about codatatypes and extended datatype terms (EXPERTS only) [*]

--dt-binary-split

do binary splits for datatype constructor types (EXPERTS only) [*]

--dt-blast-splits

when applicable, blast splitting lemmas for all variables at once (EXPERTS only) [*]

--dt-cyclic

do cyclicity check for datatypes (EXPERTS only) [*]

--dt-infer-as-lemmas

always send lemmas out instead of making internal inferences (EXPERTS only) [*]

--dt-nested-rec

allow nested recursion in datatype definitions (EXPERTS only) [*]

--dt-polite-optimize

turn on optimization for polite combination (EXPERTS only) [*]

--dt-share-sel

internally use shared selectors across multiple constructors (EXPERTS only) [*]

--sygus-abort-size=N

tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)

--sygus-fair=MODE

if and how to apply fairness for sygus

--sygus-fair-max

use max instead of sum for multi-function sygus conjectures (EXPERTS only) [*]

--sygus-rewriter=MODE

if and how to apply rewriting for sygus symmetry breaking

--sygus-simple-sym-break=MODE

if and how to apply simple symmetry breaking based on the grammar for smart enumeration

--sygus-sym-break-lazy lazily add symmetry breaking lemmas for terms (EXPERTS

only) [*]

--sygus-sym-break-pbe

sygus symmetry breaking lemmas based on pbe conjectures [*]

--sygus-sym-break-rlv

add relevancy conditions to symmetry breaking lemmas (EXPERTS only) [*]

From the Decision Heuristics module:¶

--jh-rlv-order

maintain activity-based ordering for decision justification heuristic (EXPERTS only) [*]

--jh-skolem=MODE

policy for when to satisfy skolem definitions in justification heuristic (EXPERTS only)

--jh-skolem-rlv=MODE

policy for when to consider skolem definitions relevant in justification heuristic (EXPERTS only)

From the Expression module:¶

--type-checking

type check expressions (EXPERTS only) [*]

--wf-checking

check that terms passed to API methods are well formed (default false for text interface) (EXPERTS only) [*]

From the Finite Field Theory module:¶

--ff

enables the finite field solver in applicable logics (EXPERTS only) [*]

--ff-bitsum

parse bitsums (EXPERTS only) [*]

--ff-elim-disjunctive-bit

rewrite disjunctive bit constraints (or (= x 1) (= x 0)) as (= (* x x) x) (EXPERTS only) [*]

--ff-field-polys

include field polynomials in Groebner basis computation; don't do this (EXPERTS only) [*]

--ff-solver=MODE

which field solver (default: 'gb'; see --ff-solver=help) (EXPERTS only)

--ff-trace-gb

use a traced groebner basis engine (EXPERTS only) [*]

From the Floating-Point module:¶

--fp

enables the floating point theory in applicable logics (EXPERTS only) [*]

--fp-exp

Allow floating-point sorts of all sizes, rather than only Float32 (8/24) or Float64 (11/53) (experimental) (EXPERTS only) [*]

--fp-lazy-wb

Enable lazier word-blasting (on preNotifyFact instead of registerTerm) (EXPERTS only) [*]

From the Driver module:¶

--dump-difficulty

dump the difficulty measure after every response to check-sat [*]

--dump-instantiations

output instantiations of quantified formulas after every UNSAT/VALID response [*]

--dump-instantiations-debug

output instantiations of quantified formulas after every UNSAT/VALID response, with debug information (EXPERTS only) [*]

--dump-models

output models after every SAT/INVALID/UNKNOWN response [*]

--dump-proofs

output proofs after every UNSAT/VALID response [*]

--dump-unsat-cores

output unsat cores after every UNSAT/VALID response [*]

--dump-unsat-cores-lemmas

output lemmas in unsat cores after every UNSAT/VALID response [*]

--force-no-limit-cpu-while-dump

Force no CPU limit when dumping models and proofs (EXPERTS only) [*]

--portfolio-dry-run

Print the strategies that would be run with --use-portfolio, without executing them (EXPERTS only) [*]

--portfolio-jobs=n

Number of parallel jobs the portfolio engine can run (EXPERTS only)

--segv-spin

spin on segfault/other crash waiting for gdb (EXPERTS only) [*]

--show-trace-tags

show all available tags for tracing (EXPERTS only)

--use-portfolio

Use internal portfolio mode based on the logic (EXPERTS only) [*]

From the Parallel module:¶

--append-learned-literals-to-cubes

emit learned literals with the cubes (EXPERTS only) [*]

--checks-before-partition=N

number of standard or full effort checks until partitioning (EXPERTS only)

--checks-between-partitions=N

number of checks between partitions (EXPERTS only)

--compute-partitions=N make n partitions. n <2 disables computing partitions

entirely (EXPERTS only)

--partition-check=MODE | --check=MODE

select whether partitioning happens at full or standard check (EXPERTS only)

--partition-conflict-size=N

number of literals in a cube; if no partition size is set, then the partition conflict size is chosen to be log2(number of requested partitions) (EXPERTS only)

--partition-start-time=N

time to start creating partitions in seconds (EXPERTS only)

--partition-strategy=MODE | --partition=MODE

choose partition strategy mode (EXPERTS only)

--partition-time-interval=N

time to wait between scatter partitions (EXPERTS only)

--partition-tlimit=N

time limit for partitioning in seconds (EXPERTS only)

--partition-when=MODE

choose when to partition (EXPERTS only)

--random-partitioning

create random partitions (EXPERTS only) [*]

--write-partitions-to=output | --partitions-out=output

set the output channel for writing partitions (EXPERTS only)

From the Parser module:¶

--filesystem-access

limits the file system access if set to false (EXPERTS only) [*]

--fresh-binders

construct fresh variables always when parsing binders (EXPERTS only) [*]

--fresh-declarations

use API interface for fresh constants when parsing declarations and definitions [*]

--global-declarations

force all declarations and definitions to be global when parsing [*]

--parse-skolem-definitions

allows the parsing of skolems in the input file (EXPERTS only) [*]

--parsing-mode=MODE

choose parsing mode, see --parsing-mode=help (EXPERTS only)

--semantic-checks

enable semantic checks, including type checks (EXPERTS only) [*]

--term-sort-overload

allow overloading of terms and sorts (EXPERTS only) [*]

From the Printing module:¶

--bv-print-consts-as-indexed-symbols

print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x [*]

--flatten-ho-chains

print (binary) application chains in a flattened way, e.g. (a b c) rather than ((a b) c) (EXPERTS only) [*]

--model-u-print=MODE

determines how to print uninterpreted elements in models

--print-arith-lit-token

print rationals and negative arithmetic literals as lexed tokens, e.g. 1/4, -1.5 (EXPERTS only) [*]

--print-skolem-definitions

print skolems based on their definitions e.g. @ARRAY_DIFF_N prints instead as (@array.diff A B) (EXPERTS only) [*]

From the Proof module:¶

--check-proof-steps

Check proof steps for satisfiability, for refutation soundness testing. Note this checks only steps for non-core proof rules (EXPERTS only) [*]

--check-proofs-complete

treat an incomplete proof as a failure (enabled by default in safe builds) (EXPERTS only) [*]

--drat-binary-format

Print the DRAT proof in binary format (EXPERTS only) [*]

--lfsc-expand-trust

Print the children of trusted proof steps (EXPERTS only) [*]

--lfsc-flatten

Flatten steps in the LFSC proof (EXPERTS only) [*]

--opt-res-reconstruction-size

Optimize resolution reconstruction to reduce proof size [*]

--print-dot-clusters

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

--proof-alethe-define-skolems

In Alethe proofs, use define-funs in proof preamble for Skolemization terms (EXPERTS only) [*]

--proof-alethe-res-pivots

Add pivots to Alethe resolution steps (EXPERTS only) [*]

--proof-allow-trust

Whether to allow trust in the proof printer (when applicable) (EXPERTS only) [*]

--proof-chain-m-res

Use chain multiset resolution [*]

--proof-dag-global

Dagify terms in proofs using global definitions (EXPERTS only) [*]

--proof-dot-dag

Indicates if the dot proof will be printed as a DAG or as a tree (EXPERTS only) [*]

--proof-elim-subtypes

Eliminate subtypes (mixed arithmetic) in proofs (EXPERTS only) [*]

--proof-format-mode=MODE

select language of proof output (EXPERTS only)

--proof-log

Proof logging mode (EXPERTS only) [*]

--proof-pedantic=N

assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof (EXPERTS only)

--proof-pp-merge

merge subproofs in final proof post-processor (EXPERTS only) [*]

--proof-pre-simp-lookahead=N

the lookahead depth for merging proofs at previsit (EXPERTS only)

--proof-prune-input

Prune unused input assumptions from final scope (EXPERTS only) [*]

--proof-rewrite-rcons-rec-limit=N

the matching recursion limit for reconstructing proofs of theory rewrites

--proof-rewrite-rcons-step-limit=N

the limit of steps considered for reconstructing proofs of theory rewrites

--prop-proof-mode=MODE modes for the type of proof generated by the SAT solver

--sat-proof-min-dimacs Minimize the DIMACs emitted when prop-proof-mode is set

to sat-external-prove (EXPERTS only) [*]

From the SAT Layer module:¶

--minisat-dump-dimacs

instead of solving minisat dumps the asserted clauses in Dimacs format (EXPERTS only) [*]

--minisat-simplification=MODE

Simplifications to be performed by Minisat. (EXPERTS only)

--preregister-mode=MODE

Modes for when to preregister literals.

--random-freq=P | --random-frequency=P

sets the frequency of random decisions in the sat solver (P=0.0 by default) (EXPERTS only)

--restart-int-base=N

sets the base restart interval for the sat solver (N=25 by default) (EXPERTS only)

--restart-int-inc=F

sets the restart interval increase factor for the sat solver (F=3.0 by default) (EXPERTS only)

--sat-random-seed=N

sets the random seed for the sat solver

--sat-solver=MODE

choose which sat solver to use, see --sat-solver=help (EXPERTS only)

From the Quantifiers module:¶

--cbqi

enable conflict-based quantifier instantiation [*]

--cbqi-all-conflict

add all available conflicting instances during conflict-based instantiation [*]

--cbqi-mode=MODE

what effort to apply conflict find mechanism

--cbqi-skip-rd

optimization, skip instances based on possibly irrelevant portions of quantified formulas (EXPERTS only) [*]

--cbqi-tconstraint

enable entailment checks for t-constraints in cbqi algorithm (EXPERTS only) [*]

--cbqi-vo-exp

cbqi experimental variable ordering (EXPERTS only) [*]

--cegis-sample=MODE

mode for using samples in the counterexample-guided inductive synthesis loop

--cegqi

turns on counterexample-based quantifier instantiation [*]

--cegqi-all

apply counterexample-based instantiation to all quantified formulas (EXPERTS only) [*]

--cegqi-bv

use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors [*]

--cegqi-bv-ineq=MODE

choose mode for handling bit-vector inequalities with counterexample-guided instantiation (EXPERTS only)

--cegqi-bv-interleave-value

interleave model value instantiation with word-level inversion approach (EXPERTS only) [*]

--cegqi-bv-linear

linearize adder chains for variables (EXPERTS only) [*]

--cegqi-bv-rm-extract

replaces extract terms with variables for counterexample-guided instantiation for bit-vectors (EXPERTS only) [*]

--cegqi-bv-solve-nl

try to solve non-linear bv literals using model value projections (EXPERTS only) [*]

--cegqi-full

turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation (EXPERTS only) [*]

--cegqi-inf-int

use integer infinity for vts in counterexample-based quantifier instantiation (EXPERTS only) [*]

--cegqi-inf-real

use real infinity for vts in counterexample-based quantifier instantiation (EXPERTS only) [*]

--cegqi-innermost

only process innermost quantified formulas in counterexample-based quantifier instantiation [*]

--cegqi-midpoint

choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation [*]

--cegqi-min-bounds

use minimally constrained lower/upper bound for counterexample-based quantifier instantiation (EXPERTS only) [*]

--cegqi-multi-inst

when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation (EXPERTS only) [*]

--cegqi-nested-qe

process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation [*]

--cegqi-nopt

non-optimal bounds for counterexample-based quantifier instantiation (EXPERTS only) [*]

--cegqi-round-up-lia

round up integer lower bounds in substitutions for counterexample-based quantifier instantiation (EXPERTS only) [*]

--cond-var-split-quant=MODE

split quantified formulas that lead to variable eliminations (EXPERTS only)

--conjecture-gen

generate candidate conjectures for inductive proofs (EXPERTS only) [*]

--conjecture-gen-gt-enum=N

number of ground terms to generate for model filtering (EXPERTS only)

--conjecture-gen-max-depth=N

maximum depth of terms to consider for conjectures (EXPERTS only)

--conjecture-gen-per-round=N

number of conjectures to generate per instantiation round (EXPERTS only)

--cons-exp-triggers

use constructor expansion for single constructor datatypes triggers (EXPERTS only) [*]

--dt-stc-ind

apply strengthening for existential quantification over datatypes based on structural induction (EXPERTS only) [*]

--dt-var-exp-quant

expand datatype variables bound to one constructor in quantifiers (EXPERTS only) [*]

--e-matching

whether to do heuristic E-matching [*]

--elim-taut-quant

eliminate tautological disjuncts of quantified formulas [*]

--enum-inst-interleave interleave enumerative instantiation with other

techniques [*]

--enum-inst-limit=N

maximum number of rounds of enumerative instantiation to apply (-1 means no limit) (EXPERTS only)

--enum-inst-rd

whether to use relevant domain first for enumerative instantiation strategy (EXPERTS only) [*]

--enum-inst-stratify

stratify effort levels in enumerative instantiation, which favors speed over fairness (EXPERTS only) [*]

--enum-inst-sum

enumerating tuples of quantifiers by increasing the sum of indices, rather than the maximum [*]

--ext-rewrite-quant

apply extended rewriting to bodies of quantified formulas [*]

--finite-model-find

use finite model finding heuristic for quantifier instantiation [*]

--fmf-bound

finite model finding on bounded quantification [*]

--fmf-bound-blast

send all instantiations for bounded ranges in a single round (EXPERTS only) [*]

--fmf-bound-lazy

enforce bounds for bounded quantification lazily via use of proxy variables (EXPERTS only) [*]

--fmf-fun

find models for recursively defined functions, assumes functions are admissible (EXPERTS only) [*]

--fmf-fun-rlv

find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant (EXPERTS only) [*]

--fmf-mbqi=MODE

choose mode for model-based quantifier instantiation (EXPERTS only)

--fmf-type-completion-thresh=N

the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted

--full-sygus-verify

resort to full effort techniques instead of answering unknown when checking sygus candidates (EXPERTS only) [*]

--global-negate

do global negation of input formula (EXPERTS only) [*]

--ho-elim

eagerly eliminate higher-order constraints (EXPERTS only) [*]

--ho-elim-store-ax

use store axiom during ho-elim (EXPERTS only) [*]

--ho-matching

do higher-order matching algorithm for triggers with variable operators (EXPERTS only) [*]

--ho-merge-term-db

merge term indices modulo equality (EXPERTS only) [*]

--ieval=MODE

mode for using instantiation evaluation

--increment-triggers

generate additional triggers as needed during search (EXPERTS only) [*]

--inst-local

Instantiations are local to the SAT context [*]

--inst-max-level=N

maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) (EXPERTS only)

--inst-max-rounds=N

maximum number of instantiation rounds (-1 == no limit, default)

--inst-no-entail

do not consider instances of quantified formulas that are currently entailed [*]

--inst-when=MODE

when to apply instantiation

--inst-when-phase=N

instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen (EXPERTS only)

--int-wf-ind

apply strengthening for integers based on well-founded induction (EXPERTS only) [*]

--ite-dtt-split-quant

split ites with dt testers as conditions (EXPERTS only) [*]

--ite-lift-quant=MODE

ite lifting mode for quantified formulas

--literal-matching=MODE

choose literal matching mode (EXPERTS only)

--macros-quant

perform quantifiers macro expansion [*]

--macros-quant-mode=MODE

mode for quantifiers macro expansion

--mbqi

use model-based quantifier instantiation [*]

--mbqi-check-timeout=N timeout (in milliseconds) for verifying subcalls for

model-based instantiation (0 == no limit)

--mbqi-enum

use fast enumeration to augment instantiations from MBQI [*]

--mbqi-enum-ext-vars-grammar

include variables defined in terms of others in grammars for fast enumerative mbqi (EXPERTS only) [*]

--mbqi-enum-free-syms-grammar

include free symbols from the body of the quantified formula in grammars for fast enumerative mbqi (EXPERTS only) [*]

--mbqi-enum-global-syms-grammar

include global symbols from all available assertions in grammars for fast enumerative mbqi (EXPERTS only) [*]

--mbqi-interleave

interleave model-based quantifier instantiation with other techniques (EXPERTS only) [*]

--mbqi-nested-check

check nested quantified formulas in MBQI (EXPERTS only) [*]

--mbqi-one-inst-per-round

only add one instantiation per quantifier per round for mbqi [*]

--miniscope-quant=MODE miniscope mode for quantified formulas

--miniscope-quant-user miniscope quantified formulas with user patterns [*]

--multi-trigger-cache

caching version of multi triggers [*]

--multi-trigger-linear implementation of multi triggers where maximum number

of instantiations is linear wrt number of ground terms [*]

--multi-trigger-priority

only try multi triggers if single triggers give no instantiations [*]

--multi-trigger-when-single

select multi triggers when single triggers exist [*]

--oracles

Enable interface to external oracles (EXPERTS only) [*]

--partial-triggers

use triggers that do not contain all free variables (EXPERTS only) [*]

--pool-inst

pool-based instantiation: instantiate with ground terms occurring in user-specified pools (EXPERTS only) [*]

--pre-skolem-quant=MODE

modes to apply skolemization eagerly to bodies of quantified formulas

--pre-skolem-quant-nested

apply skolemization to nested quantified formulas (EXPERTS only) [*]

--prenex-quant=MODE

prenex mode for quantified formulas (EXPERTS only)

--prenex-quant-user

prenex quantified formulas with user patterns [*]

--print-inst-full

print instantiations for formulas that do not have given identifiers [*]

--purify-triggers

purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1 (EXPERTS only) [*]

--quant-alpha-equiv

infer alpha equivalence between quantified formulas [*]

--quant-dsplit=MODE

mode for dynamic quantifiers splitting

--quant-fun-wd

assume that function defined by quantifiers are well defined (EXPERTS only) [*]

--quant-ind

use all available techniques for inductive reasoning (EXPERTS only) [*]

--quant-rep-mode=MODE

selection mode for representatives in quantifiers engine (EXPERTS only)

--register-quant-body-terms

consider ground terms within bodies of quantified formulas for matching (EXPERTS only) [*]

--relational-triggers

choose relational triggers such as x = f(y), x >= f(y) (EXPERTS only) [*]

--relevant-triggers

prefer triggers that are more relevant based on SInE style analysis [*]

--sub-cbqi

Enable conflict-based instantiation subsolver strategy [*]

--sub-cbqi-timeout=N

Timeout (in milliseconds) for subsolver calls for sub-cbqi (EXPERTS only)

--sygus

support SyGuS commands [*]

--sygus-add-const-grammar

statically add constants appearing in conjecture to grammars [*]

--sygus-arg-relevant

static inference techniques for computing whether arguments of functions-to-synthesize are relevant (EXPERTS only) [*]

--sygus-auto-unfold

enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems (EXPERTS only) [*]

--sygus-bool-ite-return-const

Only use Boolean constants for return values in unification-based function synthesis (EXPERTS only) [*]

--sygus-core-connective

use unsat core analysis to construct Boolean connective to sygus conjectures [*]

--sygus-crepair-abort

abort if constant repair techniques are not applicable (EXPERTS only) [*]

--sygus-enum=MODE

mode for sygus enumeration

--sygus-enum-fast-num-consts=N

the branching factor for the number of interpreted constants to consider for each size when using --sygus-enum=fast (EXPERTS only)

--sygus-enum-random-p=P

the parameter of the geometric distribution used to determine the size of terms generated by --sygus-enum=random (EXPERTS only)

--sygus-eval-unfold=MODE

modes for sygus evaluation unfolding

--sygus-expr-miner-check-timeout=N

timeout (in milliseconds) for satisfiability checks in expression miners (EXPERTS only)

--sygus-filter-sol=MODE

mode for filtering sygus solutions (EXPERTS only)

--sygus-filter-sol-rev compute backwards filtering to compute whether previous

solutions are filtered based on later ones (EXPERTS only) [*]

--sygus-grammar-cons=MODE

mode for SyGuS grammar construction

--sygus-grammar-ho-partial

add partial function applications to the grammar (EXPERTS only) [*]

--sygus-grammar-norm

statically normalize sygus grammars based on flattening (linearization) (EXPERTS only) [*]

--sygus-grammar-use-disj

use disjunctions in internally generated grammars. this is set to false when solving abduction queries. (EXPERTS only) [*]

--sygus-inference=MODE mode for preprocessing arbitrary inputs to sygus

conjectures (EXPERTS only)

--sygus-inst

Enable SyGuS instantiation quantifiers module [*]

--sygus-inst-mode=MODE select instantiation lemma mode (EXPERTS only)

--sygus-inst-scope=MODE

select scope of ground terms (EXPERTS only)

--sygus-inst-term-sel=MODE

granularity for ground terms (EXPERTS only)

--sygus-inv-templ=MODE template mode for sygus invariant synthesis (weaken

pre-condition, strengthen post-condition, or none)

--sygus-inv-templ-when-sg

use invariant templates (with solution reconstruction) for syntax guided problems (EXPERTS only) [*]

--sygus-min-grammar

statically minimize sygus grammars [*]

--sygus-out=MODE

output mode for sygus

--sygus-pbe

enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures [*]

--sygus-pbe-multi-fair when using multiple enumerators, ensure that we only

register value of minimial term size (EXPERTS only) [*]

--sygus-pbe-multi-fair-diff=N

when using multiple enumerators, ensure that we only register values of minimial term size plus this value (default 0) (EXPERTS only)

--sygus-qe-preproc

use quantifier elimination as a preprocessing step for sygus (EXPERTS only) [*]

--sygus-query-gen=MODE mode for generating interesting satisfiability queries

using SyGuS, for internal fuzzing (EXPERTS only)

--sygus-query-gen-dump-files=MODE

mode for dumping external files corresponding to interesting satisfiability queries with sygus-query-gen (EXPERTS only)

--sygus-query-gen-filter-solved

do not print queries that are solved (EXPERTS only) [*]

--sygus-query-gen-thresh=N

number of points that we allow to be equal for enumerating satisfiable queries with sygus-query-gen (EXPERTS only)

--sygus-rec-fun

enable efficient support for recursive functions in sygus (EXPERTS only) [*]

--sygus-rec-fun-eval-limit=N

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) (EXPERTS only)

--sygus-rec-fun-infer

automatically infer recursive definitions for sygus (EXPERTS only) [*]

--sygus-repair-const

use approach to repair constants in sygus candidate solutions [*]

--sygus-repair-const-timeout=N

timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions (EXPERTS only)

--sygus-rr-synth-accel add dynamic symmetry breaking clauses based on

candidate rewrites (EXPERTS only) [*]

--sygus-rr-synth-check use satisfiability check to verify correctness of

candidate rewrites (EXPERTS only) [*]

--sygus-rr-synth-filter-cong

filter candidate rewrites based on congruence (EXPERTS only) [*]

--sygus-rr-synth-filter-match

filter candidate rewrites based on matching (EXPERTS only) [*]

--sygus-rr-synth-filter-nl

filter non-linear candidate rewrites (EXPERTS only) [*]

--sygus-rr-synth-filter-order

filter candidate rewrites based on variable ordering (EXPERTS only) [*]

--sygus-rr-synth-input-nvars=N

the maximum number of variables per type that appear in rewrites from sygus-rr-synth-input (EXPERTS only)

--sygus-rr-synth-rec

synthesize rewrite rules over all sygus grammar types recursively (EXPERTS only) [*]

--sygus-sample-fp-uniform

sample floating-point values uniformly instead of in a biased fashion (EXPERTS only) [*]

--sygus-sample-grammar when applicable, use grammar for choosing sample points

(EXPERTS only) [*]

--sygus-samples=N

number of points to consider when doing sygus rewriter sample testing (EXPERTS only)

--sygus-si=MODE

mode for processing single invocation synthesis conjectures

--sygus-si-abort

abort if synthesis conjecture is not single invocation [*]

--sygus-si-rcons=MODE

policy for reconstructing solutions for single invocation conjectures

--sygus-si-rcons-limit=N

number of rounds of enumeration to use during solution reconstruction (negative means unlimited) (EXPERTS only)

--sygus-si-rcons-p=P

the parameter of the geometric distribution used to determine the number of unification patterns generated by single invocation techniques. (EXPERTS only)

--sygus-stream

enumerate a stream of solutions instead of terminating after the first one [*]

--sygus-unif-cond-independent-no-repeat-sol

Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis (EXPERTS only) [*]

--sygus-unif-pi=MODE

mode for synthesis via piecewise-indepedent unification

--sygus-unif-shuffle-cond

Shuffle condition pool when building solutions (may change solutions sizes) (EXPERTS only) [*]

--sygus-verify-inst-max-rounds=N

maximum number of instantiation rounds for sygus verification calls (-1 == no limit, default is 10) (EXPERTS only)

--sygus-verify-timeout=N

timeout (in milliseconds) for verifying satisfiability of synthesized terms (0 == no limit)

--term-db-mode=MODE

which ground terms to consider for instantiation

--trigger-active-sel=MODE

selection mode to activate triggers (EXPERTS only)

--trigger-sel=MODE

selection mode for triggers

--user-pat=MODE

policy for handling user-provided patterns for quantifier instantiation

--user-pool=MODE

policy for handling user-provided pools for quantifier instantiation (EXPERTS only)

--var-elim-quant

enable simple variable elimination for quantified formulas [*]

--var-ent-eq-elim-quant

enable variable elimination for quantified formulas that infers entailed equalities corresponding to eliminations [*]

--var-ineq-elim-quant

enable variable elimination based on infinite projection of unbound arithmetic variables [*]

From the Separation Logic Theory module:¶

--sep

enables the separation logic solver in applicable logics (EXPERTS only) [*]

--sep-min-refine

only add refinement lemmas for minimal (innermost) assertions (EXPERTS only) [*]

--sep-pre-skolem-emp

eliminate emp constraint at preprocess time (EXPERTS only) [*]

From the Sets Theory module:¶

--rels-exp

enable the relations extension of the theory of sets (EXPERTS only) [*]

--sets-card-exp

enable the cardinality extension of the theory of sets (EXPERTS only) [*]

--sets-exp

enable extended symbols such as complement and universe in theory of sets (EXPERTS only) [*]

--sets-proxy-lemmas

introduce proxy variables eagerly to shorten lemmas (EXPERTS only) [*]

From the SMT Layer module:¶

--abstract-values

in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard (EXPERTS only) [*]

--ackermann

eliminate functions by ackermannization (EXPERTS only) [*]

--bv-to-int-use-pow2

use internal pow2 operator when translating shift notes (EXPERTS only) [*]

--bvand-integer-granularity=N

granularity to use in --solve-bv-as-int mode and for iand operator (experimental) (EXPERTS only)

--deep-restart=MODE

mode for deep restarts (EXPERTS only)

--deep-restart-factor=F

sets the threshold for average assertions per literal before a deep restart (EXPERTS only)

--difficulty-mode=MODE choose output mode for get-difficulty, see

--difficulty-mode=help (EXPERTS only)

--early-ite-removal

remove ITEs early in preprocessing (EXPERTS only) [*]

--ext-rew-prep=MODE

mode for using extended rewriter as a preprocessing pass, see --ext-rew-prep=help (EXPERTS only)

--foreign-theory-rewrite

Cross-theory rewrites (EXPERTS only) [*]

--iand-mode=mode

Set the refinement scheme for integer AND (EXPERTS only)

--interpolants-mode=MODE

choose interpolants production mode, see --interpolants-mode=help

--ite-simp

turn on ite simplification (Kim (and Somenzi) et al., SAT 2009) (EXPERTS only) [*]

--learned-rewrite

rewrite the input based on learned literals [*]

--minimal-unsat-cores

if an unsat core is produced, it is reduced to a minimal unsat core (EXPERTS only) [*]

--model-cores=MODE

mode for producing model cores

--model-var-elim-uneval

allow variable elimination based on unevaluatable terms to variables (EXPERTS only) [*]

--on-repeat-ite-simp

do the ite simplification pass again if repeating simplification (EXPERTS only) [*]

--print-cores-full

print all formulas regardless of whether they are named, e.g. in unsat cores [*]

--produce-abducts

support the get-abduct command [*]

--produce-assertions | --interactive-mode

keep an assertions list. Note this option is always enabled. [*]

--produce-assignments

support the get-assignment command [*]

--produce-difficulty

enable tracking of difficulty. [*]

--produce-interpolants turn on interpolation generation. [*]

--produce-learned-literals

produce learned literals, support get-learned-literals [*]

--produce-unsat-assumptions

turn on unsat assumptions generation [*]

--proof-mode=MODE

choose proof mode, see --proof-mode=help (EXPERTS only)

--repeat-simp

make multiple passes with nonclausal simplifier (EXPERTS only) [*]

--simp-ite-compress

enables compressing ites after ite simplification (EXPERTS only) [*]

--simp-with-care

enables simplifyWithCare in ite simplificiation (EXPERTS only) [*]

--simplification=MODE | --simplification-mode=MODE

choose simplification mode, see --simplification=help

--simplification-bcp

apply Boolean constant propagation as a substitution during simplification (EXPERTS only) [*]

--solve-bv-as-int=MODE mode for translating BVAnd to integer

--solve-int-as-bv=N

attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)

--solve-real-as-int

attempt to solve a pure real satisfiable problem as an integer problem (for non-linear) [*]

--sort-inference

calculate sort inference of input problem, convert the input based on monotonic sorts (EXPERTS only) [*]

--static-learning

use static learning (on by default) [*]

--timeout-core-timeout=N

timeout (in milliseconds) for satisfiability checks for timeout cores (EXPERTS only)

--unconstrained-simp

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

--unsat-cores-mode=MODE

choose unsat core mode, see --unsat-cores-mode=help (EXPERTS only)

From the Strings Theory module:¶

--re-elim=MODE

regular expression elimination mode

--re-first-class

allow regular expressions as first class terms (EXPERTS only) [*]

--re-inter-mode=MODE

determines which regular expressions intersections to compute (EXPERTS only)

--seq-array=MODE

use array-inspired solver for sequence updates in eager or lazy mode (EXPERTS only)

--strings-alpha-card=N the assumed cardinality of the alphabet of characters

for strings, which is a prefix of the interval of unicode code points in the SMT-LIB standard (EXPERTS only)

--strings-check-entail-len

check entailment between length terms to reduce splitting [*]

--strings-deq-ext

use extensionality for string disequalities [*]

--strings-eager-eval

perform eager context-dependent evaluation for applications of string kinds in the equality engine [*]

--strings-eager-len-re use regular expressions for eager length conflicts [*]

--strings-eager-reg

do registration lemmas for terms during preregistration. If false, do registration lemmas for terms when they appear in asserted literals (EXPERTS only) [*]

--strings-eager-solver use the eager solver [*]

--strings-exp

experimental features in the theory of strings [*]

--strings-ff

do flat form inferences (EXPERTS only) [*]

--strings-fmf

the finite model finding used by the theory of strings [*]

--strings-infer-as-lemmas

always send lemmas out instead of making internal inferences (EXPERTS only) [*]

--strings-infer-sym

generalized inferences in strings based on proxy symbols (EXPERTS only) [*]

--strings-lazy-pp

perform string preprocessing lazily [*]

--strings-len-norm

strings length normalization lemma (EXPERTS only) [*]

--strings-mbr

use models to avoid reductions for extended functions that introduce quantified formulas [*]

--strings-model-max-len=N

The maximum size of string values in models (EXPERTS only)

--strings-process-loop-mode=MODE

determines how to process looping string equations

--strings-re-derive-conf

use regular expression derive for conflict finding (EXPERTS only) [*]

--strings-re-posc-eager

eager reduction of positive membership into concatenation (EXPERTS only) [*]

--strings-rec-arith-approx

use possibly recursive reasoning when finding approximations for arithmetic string terms (EXPERTS only) [*]

--strings-regexp-inclusion

use regular expression inclusion for finding conflicts and avoiding regular expression unfolding [*]

--strings-rexplain-lemmas

regression explanations for string lemmas (EXPERTS only) [*]

From the Theory Layer module:¶

--assign-function-values

assign values for uninterpreted functions in models (EXPERTS only) [*]

--conflict-process=MODE

mode for processing theory conflicts (EXPERTS only)

--ee-mode=MODE

mode for managing equalities across theory solvers

--lemma-inprocess=MODE Modes for inprocessing lemmas. (EXPERTS only)

--lemma-inprocess-infer-eq-lit

Infer equivalent literals when using lemma inprocess (EXPERTS only) [*]

--lemma-inprocess-subs=MODE

Modes for substitutions for inprocessing lemmas. (EXPERTS only)

--relevance-filter

enable analysis of relevance of asserted literals with respect to the input formula (EXPERTS only) [*]

--tc-mode=MODE

mode for theory combination (EXPERTS only)

--theoryof-mode=MODE

mode for Theory::theoryof() (EXPERTS only)

From the Uninterpreted Functions Theory module:¶

--eager-arith-bv-conv

eagerly expand bit-vector to arithmetic conversions during preprocessing [*]

--model-based-arith-bv-conv

model-based inferences for bit-vector to arithmetic conversions (EXPERTS only) [*]

--symmetry-breaker

use UF symmetry breaker (Deharbe et al., CADE 2011) [*]

--uf-card-exp

allows logics with UF+cardinality (EXPERTS only) [*]

--uf-ho-exp

enables the higher-order logic solver in applicable logics (EXPERTS only) [*]

--uf-ho-ext

apply extensionality on function symbols (EXPERTS only) [*]

--uf-lambda-qe

apply quantifier elimination eagerly when two lambdas are equated (EXPERTS only) [*]

--uf-lazy-ll

do lambda lifting lazily [*]

--uf-ss=MODE

mode of operation for uf with cardinality solver.

--uf-ss-abort-card=N

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

--uf-ss-fair

use fair strategy for finite model finding multiple sorts [*]

--uf-ss-fair-monotone

group monotone sorts when enforcing fairness for finite model finding (EXPERTS only) [*]

[*] Each of these options has a --no-OPTIONNAME variant, which reverses the

sense of the option.

compiled with GCC version 15.2.0 on Dec 24 2025 00:41:53