# Tactics Summary

## Tactic ackernannize_bv​

### Short Description​

A tactic for performing Ackermann reduction for bit-vector formulas

### Long Description​

The Ackermann reduction replaces uninterpreted functions $f(t_1), f(t_2)$ by fresh variables $f_1, f_2$ and addes axioms $t_1 \simeq t_2 \implies f_1 \simeq f_2$. The reduction has the effect of eliminating uninterpreted functions. When the reduction produces a pure bit-vector benchmark, it allows Z3 to use a specialized SAT solver.

### Notes​

• does not support proofs, does not support unsatisfiable cores

### Short Description​

Tactic for bounding unbounded variables.

### Long Description​

The tactic creates a stronger sub-goal by adding bounds to variables. The new goal may not be satisfiable even if the original goal is.

### Parameters​

ParameterTypeDescriptionDefault
add_bound_lowerrational(default: -2) lower bound to be added to unbounded variables.
add_bound_upperrational(default: 2) upper bound to be added to unbounded variables.

## Tactic aig​

### Short Description​

Simplify Boolean structure using AIGs (And-inverter graphs).

### Long Description​

And-inverter graphs (AIGs) uses just the Boolean connectives and and not to encode Boolean formulas. The circuit representation using AIGs first converts formulas using other connectives to this normal form, then performs local simplification steps to minimize the circuit representation. Note that the simplification steps used by this tactic are heuristic, trading speed for power, and do not represent a high-quality circuit minimization approach.

### Parameters​

ParameterTypeDescriptionDefault
max_memoryunsigned int(default: infty) maximum amount of memory in megabytes.4294967295

## Tactic bit-blast​

### Short Description​

Apply bit-blasting to a given goal.

### Parameters​

ParameterTypeDescriptionDefault
blast_fullboolbit-blast any term with bit-vector sort, this option will make E-matching ineffective in any pattern containing bit-vector terms.false
blast_mulboolbit-blast multipliers (and dividers, remainders).true
blast_quantboolbit-blast quantified variables.false
max_memoryunsigned int(default: infty) maximum amount of memory in megabytes.4294967295
max_stepsunsigned int(default: infty) maximum number of steps.4294967295

## Tactic blast-term-ite​

### Short Description:​

Blast term if-then-else by hoisting them up. This is expensive but useful in some cases, such as for enforcing constraints being in difference logic. Use elim-term-ite elsewhere when possible.

### Parameters​

ParameterTypeDescriptionDefault
max_inflationunsigned int(default: infinity) multiplicative factor of initial term size.4294967295
max_memoryunsigned int(default: infty) maximum amount of memory in megabytes.4294967295
max_stepsunsigned int(default: infty) maximum number of steps.4294967295

## Tactic bv-slice​

### Short Description​

Slices bit-vectors into sub-ranges to allow simplifying sub-ranges.

### Long Description​

It rewrites a state using bit-vector slices. Slices are extracted from bit-vector equality assertions. An equality assertion may equate a sub-range of a bit-vector with a constant. The tactic ensures that all occurrences of the subrange are replaced by the constants to allow additional simplification

## Tactic bv1-blast​

### Short Description​

Reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported).

### Long Description​

Rewriter for "blasting" bit-vectors of size n into bit-vectors of size 1. This rewriter only supports concat and extract operators. This transformation is useful for handling benchmarks that contain many BV equalities.

Remark: other operators can be mapped into concat/extract by using the simplifiers.

### Parameters​

ParameterTypeDescriptionDefault
max_memoryunsigned int(default: infty) maximum amount of memory in megabytes.4294967295
max_stepsunsigned int(default: infty) maximum number of steps.4294967295

## Tactic bv_bound_chk​

### Short Description​

Attempts to detect inconsistencies of bounds on bv expressions.

### Notes​

• does not support proofs, does not support cores

## Tactic bvarray2uf​

### Short Description​

Tactic that rewrites bit-vector arrays into bit-vector (uninterpreted) functions.

### Parameters​

ParameterTypeDescriptionDefault
produce_modelsboolmodel generation.false

## Tactic card2bv​

### Short Description​

Tactic for converting Pseudo-Boolean constraints to bit-vectors.

### Long Description​

The tactic implements a set of standard methods for converting cardinality and Pseudo-Boolean constraints into bit-vector or propositional formulas (using basic logical connectives, conjunction, disjunction, negation). The conversions from cardinality constraints are controlled separately from the conversions from Pseudo-Boolean constraints using different parameters.

### Notes​

• supports cores
• does not support proofs

### Parameters​

ParameterTypeDescriptionDefault
cardinality.encodingsymbolencoding used for cardinality constraints: grouped, bimander, ordered, unate, circuitnone
keep_cardinality_constraintsboolretain cardinality constraints for solvertrue
pb.solversymbolencoding used for Pseudo-Boolean constraints: totalizer, sorting, binary_merge, bv, solver. PB constraints are retained if set to 'solver'solver

## Tactic cofactor-term-ite​

### Short Description​

Eliminate (ground) term if-then-else's using cofactors. It hoists nested if-then-else expressions inside terms into the top level of the formula.

### Notes​

• does not support proofs, does not support cores

### Parameters​

ParameterTypeDescriptionDefault
cofactor_equalitiesbool(default: true) use equalities to rewrite bodies of ite-expressions. This is potentially expensive.

## Tactic ctx-simplify​

### Short Description:​

The tactic performs simplifies sub-formulas using context built up by walking assertions and sub-formulas.

### Notes​

• supports proof terms with limited features

### Parameters​

ParameterTypeDescriptionDefault
max_depthunsigned intmaximum term depth.1024
max_memoryunsigned int(default: infty) maximum amount of memory in megabytes.4294967295
max_stepsunsigned int(default: infty) maximum number of steps.4294967295
propagate_eqboolenable equality propagation from bounds.false

## Tactic ctx-solver-simplify​

### Short Description​

A heavy handed version of ctx-simplify. It applies SMT checks on sub-formulas to check if they can be simplified to true or false within their context. Note that a sub-formula may occur within multiple contexts due to shared sub-terms. In this case the tactic is partial and simplifies a limited number of context occurrences.

### Parameters​

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
bound_simplifierboolapply bounds simplification during pre-processingtrue
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 transtivity 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
threads.cube_frequencyunsigned intfrequency for using cubing2
threads.max_conflictsunsigned intmaximal number of conflicts between rounds of cubing for parallel SMT400

## Tactic degree-shift​

### Short Description​

The procedure reduces the degrees of variables.

### Long Description​

Basic idea: if goal $G$ contains a real variable $x$, $x$ occurs with degrees $d_1, ..., d_k$ in $G$, and $n = \gcd(d_1, ..., d_k) > 1$. Then, replace $x^n$ with a new fresh variable $y$.

### Notes​

• supports proofs and cores

### Parameters​

ParameterTypeDescriptionDefault
algebraic_number_evaluatorboolsimplify/evaluate expressions containing (algebraic) irrational numbers.true
arith_ineq_lhsboolrewrite inequalities so that right-hand-side is a constant.false
arith_lhsboolall monomials are moved to the left-hand-side, and the right-hand-side is just a constant.false
bit2boolbooltry to convert bit-vector terms of size 1 into Boolean termstrue
blast_distinctboolexpand a distinct predicate into a quadratic number of disequalitiesfalse
blast_distinct_thresholdunsigned intwhen blast_distinct is true, only distinct expressions with less than this number of arguments are blasted4294967295
blast_eq_valueboolblast (some) Bit-vector equalities into bitsfalse
blast_select_storebooleagerly replace all (select (store ..) ..) term by an if-then-else termfalse
bv_extract_propboolattempt to partially propagate extraction inwardsfalse
bv_ineq_consistency_test_maxunsigned intmax size of conjunctions on which to perform consistency test based on inequalities on bitvectors.0
bv_ite2idboolrewrite ite that can be simplified to identityfalse
bv_le2extractbooldisassemble bvule to extracttrue
bv_not_simplboolapply simplifications for bvnotfalse
bv_sort_acboolsort the arguments of all AC operatorsfalse
cache_allboolcache all intermediate results.false
elim_andboolconjunctions are rewritten using negation and disjunctionsfalse
elim_itebooleliminate ite in favor of and/ortrue
elim_remboolreplace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).false
elim_sign_extboolexpand sign-ext operator using concat and extracttrue
elim_to_realbooleliminate to_real from arithmetic predicates that contain only integers.false
eq2ineqboolexpand equalities into two inequalitiesfalse
expand_nested_storesboolreplace nested stores by a lambda expressionfalse
expand_powerboolexpand (^ t k) into (* t ... t) if 1 < k <= max_degree.false
expand_select_iteboolexpand select over ite expressionsfalse
expand_select_storeboolconservatively replace a (select (store ...) ...) term by an if-then-else termfalse
expand_store_eqboolreduce (store ...) = (store ...) with a common base into selectsfalse
expand_tanboolreplace (tan x) with (/ (sin x) (cos x)).false
flatboolcreate nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxortrue
flat_and_orboolcreate nary applications for and,ortrue
gcd_roundingbooluse gcd rounding on integer arithmetic atoms.false
hi_div0booluse the 'hardware interpretation' for division by zero (for bit-vector terms)true
hoist_iteboolhoist shared summands under ite expressionsfalse
hoist_mulboolhoist multiplication over summation to minimize number of multiplicationsfalse
ignore_patterns_on_ground_qbodyboolignores patterns on quantifiers that don't mention their bound variables.true
ite_extra_rulesboolextra ite simplifications, these additional simplifications may reduce size locally but increase globallytrue
local_ctxboolperform local (i.e., cheap) context simplificationsfalse
local_ctx_limitunsigned intlimit for applying local context simplifier4294967295
max_degreeunsigned intmax degree of algebraic numbers (and power operators) processed by simplifier.64
max_memoryunsigned intmaximum amount of memory in megabytes4294967295
max_stepsunsigned intmaximum number of steps4294967295
mul2concatboolreplace multiplication by a power of two into a concatenationfalse
mul_to_powerboolcollpase (* t ... t) into (^ t k), it is ignored if expand_power is true.false
pull_cheap_iteboolpull if-then-else terms when cheap.false
push_ite_arithboolpush if-then-else over arithmetic terms.false
push_ite_bvboolpush if-then-else over bit-vector terms.false
push_to_realbooldistribute to_real over * and +.true
rewrite_patternsboolrewrite patterns.false
somboolput polynomials in sum-of-monomials formfalse
som_blowupunsigned intmaximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form10
sort_storeboolsort nested stores when the indices are known to be differentfalse
sort_sumsboolsort the arguments of + application.false
split_concat_eqboolsplit equalities of the form (= (concat t1 t2) t3)false

## Tactic demodulator​

### Short Description:​

Extracts equalities from quantifiers and applies them for simplification

### Long Description​

In first-order theorem proving (FOTP), a demodulator is a universally quantified formula of the form:

Forall X1, ..., Xn. L[X1, ..., Xn] = R[X1, ..., Xn] Where L[X1, ..., Xn] contains all variables in R[X1, ..., Xn], and L[X1, ..., Xn] is "bigger" than R[X1, ...,Xn].

The idea is to replace something big L[X1, ..., Xn] with something smaller R[X1, ..., Xn].

After selecting the demodulators, we traverse the rest of the formula looking for instances of L[X1, ..., Xn]. Whenever we find an instance, we replace it with the associated instance of R[X1, ..., Xn].

For example, suppose we have

Forall x, y.  f(x+y, y) = yandf(g(b) + h(c), h(c)) <= 0

The term f(g(b) + h(c), h(c)) is an instance of f(x+y, y) if we replace x <- g(b) and y <- h(c). So, we can replace it with y which is bound to h(c) in this example. So, the result of the transformation is:

Forall x, y.  f(x+y, y) = yandh(c) <= 0

### Example​

  (declare-sort S 0)  (declare-sort S1 0)  (declare-sort S2 0)  (declare-fun f () S)  (declare-fun f1 () S)  (declare-fun f2 (S1 S) S)  (declare-fun f3 (S2 S) S1)  (declare-fun f4 () S)  (declare-fun f5 () S2)  (assert (not (= f1 (f2 (f3 f5 f4) f))))  (assert (forall ((q S) (v S)) (or (= q v) (= f1 (f2 (f3 f5 q) v)) (= (f2 (f3 f5 v) q) f1))))  (assert (forall ((q S) (x S)) (not (= (f2 (f3 f5 q) x) f1))))  (apply demodulator)

It generates

  (goals  (goal    (forall ((q S) (v S)) (= q v))    (forall ((q S) (x S)) (not (= (f2 (f3 f5 q) x) f1)))    :precision precise :depth 1)  )

### Notes​

• supports unsat cores
• does not support fine-grained proofs

## Tactic der​

### Short Description:​

The tactic performs destructive equality resolution.

### Long Description​

Destructive equality resolution replaces bound variables that are solved by their solutions in formulas. In short, the destructive equality resolution rule takes the form:

   (forall (X Y) (or X /= s C[X])) --> (forall (Y) C[Y])

### Notes​

• supports unsat cores, proof terms

## Tactic diff-neq​

### Short Description​

A specialized solver for integer problems using only constant bounds and differences to constants.

### Long Description​

Solver for integer problems that contains literals of the form

       k <= x       x <= k       x - y != k

### Notes​

• The tactic works only when the lower bounds are 0 and disequalities use multiplication with -1. Use normalize-bounds to ensure all lower bounds are 0.

### Parameters​

ParameterTypeDescriptionDefault
diff_neq_max_kunsigned intmaximum variable upper bound for diff neq solver.1024

## Tactic distribute-forall​

### Short Description:​

Distribute $\forall$ over conjunctions (and distribute $\exists$ over disjunctions)

### Notes​

• supports unsat cores, proof terms

## Tactic dom-simplify​

### Short Description​

Apply dominator simplification rules

### Long Description​

Dominator-based simplification is a context dependent simplification function that uses a dominator tree to control the number of paths it visits during simplification. The expression DAG may have an exponential number of paths, but only paths corresponding to a dominator tree are visited. Since the paths selected by the dominator trees are limited, the simplifier may easily fail to simplify within a context.

## Tactic dt2bv​

### Short Description​

Tactic that eliminates finite domain data-types.

## Tactic elim-predicates​

### Short Description​

Eliminates predicates and macros from a formula.

### Long Description​

The tactic subsumes the functionality of macro-finder and quasi-macros. Besides finding macros, it eliminates predicates using Davis-Putnam resolution.

### Example​

the predicate p occurs once positively. All negative occurrences of p are resolved against this positive occurrence. The result of resolution is a set of equalities between arguments to p. The function f is replaced by a partial solution.

### Notes​

• support unsat cores
• does not support proofs

## Tactic elim-small-bv​

### Short Description​

Eliminate small, quantified bit-vectors by expansion

### Parameters​

ParameterTypeDescriptionDefault
max_bitsunsigned int(default: 4) maximum bit-vector size of quantified bit-vectors to be eliminated.
max_memoryunsigned int(default: infty) maximum amount of memory in megabytes.4294967295
max_stepsunsigned int(default: infty) maximum number of steps.4294967295

## Tactic elim-term-ite​

### Short Description:​

Eliminate term if-then-else by adding new fresh auxiliary variables.

### Notes​

• supports proof terms and unsat cores

### Parameters​

ParameterTypeDescriptionDefault
max_argsunsigned int(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic.
max_memoryunsigned int(default: infty) maximum amount of memory in megabytes.4294967295
max_stepsunsigned int(default: infty) maximum number of steps.4294967295

## Tactic elim-uncnstr​

### Short Description​

Eliminate Unconstrained uninterpreted constants

### Long Description​

The tactic eliminates uninterpreted constants that occur only once in a goal and such that the immediate context where they occur can be replaced by a fresh constant. We call these occurrences invertible. It relies on a series of theory specific invertibility transformations. In the following assume x and x' occur in a unique subterm and y is a fresh uninterpreted constant.

#### Boolean Connectives​

Original ContextNew TermUpdated solution
(if c x x')yx = x' = y
(if x x' e)yx = true, x' = y
(if x t x')yx = false, x' = y
(not x)yx = (not y)
(and x x')yx = y, x' = true
(or x x')yx = y, x' = false
(= x t)yx = (if y t (diff t))

where diff is a diagnonalization function available in domains of size > 1.

#### Arithmetic​

Original ContextNew TermUpdated solution
(+ x t)yx = y - t
(* x x')yx = y, x' = 1
(* -1 x)yx = -y
(<= x t)yx = (if y t (+ t 1))
(<= t x)yx = (if y t (- t 1))

#### Bit-vectors​

Original ContextNew TermUpdated solution
(bvadd x t)yx = y - t
(bvmul x x')yx = y, x' = 1
(bvmul odd x)yx = inv(odd)*y
((extract sz-1 0) x)yx = y
((extract hi lo) x)yx = (concat y1 y y2)
(udiv x x')yx = y, x' = 1
(concat x x')yx = (extract hi1 lo1 y)
(bvule x t)(or y (= t MAX))x = (if y t (bvadd t 1))
(bvule t x)(or y (= t MIN))x = (if y t (bvsub t 1))
(bvnot x)yx = (bvnot y)
(bvand x x')yx = y, x' = MAX

In addition there are conversions for shift and bit-wise or and signed comparison.

#### Arrays​

Original ContextNew TermUpdated solution
(select x t)yx = (const y)
(store x x1 x2)yx2 = (select x x1), x = y, x1 = arb

#### Algebraic Datatypes​

Original ContextNew TermUpdated solution
(head x)yx = (cons y arb)

### Notes​

• supports unsat cores
• does not support fine-grained proofs

### Parameters​

ParameterTypeDescriptionDefault
max_memoryunsigned int(default: infty) maximum amount of memory in megabytes.4294967295
max_stepsunsigned int(default: infty) maximum number of steps.4294967295

## Tactic eq2bv​

### Short Description​

Extract integer variables that are used as finite domain indicators. The integer variables can only occur in equalities.

### Notes​

• does not support proofs

## Tactic euf-completion​

### Short Description​

Uses the ground equalities as a rewrite system. The formulas are simplified using the rewrite system.

### Long Description​

The tactic uses congruence closure to represent and orient the rewrite system. Equalities from the formula are inserted in the an E-graph (congruence closure structure) and then a representative that is most shallow is extracted.

## Tactic factor​

### Short Description​

Factor polynomials in equalities and inequalities.

### Parameters​

ParameterTypeDescriptionDefault
max_primeunsigned int(default: infty) 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 step.
max_search_sizeunsigned int(default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space.
num_primesunsigned int(default: 1) 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 lifiting and searching.
split_factorsboolapply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0)).true

## Tactic fix-dl-var​

### Short Description​

Fix a difference logic variable to 0. If the problem is in the difference logic fragment, that is, all arithmetic terms are of the form (x + k), and the arithmetic atoms are of the form x - y <= k or x - y = k. Then, we can set one variable to 0.

This is useful because, many bounds can be exposed after this operation is performed.

### Parameters​

ParameterTypeDescriptionDefault
algebraic_number_evaluatorboolsimplify/evaluate expressions containing (algebraic) irrational numbers.true
arith_ineq_lhsboolrewrite inequalities so that right-hand-side is a constant.false
arith_lhsboolall monomials are moved to the left-hand-side, and the right-hand-side is just a constant.false
bit2boolbooltry to convert bit-vector terms of size 1 into Boolean termstrue
blast_distinctboolexpand a distinct predicate into a quadratic number of disequalitiesfalse
blast_distinct_thresholdunsigned intwhen blast_distinct is true, only distinct expressions with less than this number of arguments are blasted4294967295
blast_eq_valueboolblast (some) Bit-vector equalities into bitsfalse
blast_select_storebooleagerly replace all (select (store ..) ..) term by an if-then-else termfalse
bv_extract_propboolattempt to partially propagate extraction inwardsfalse
bv_ineq_consistency_test_maxunsigned intmax size of conjunctions on which to perform consistency test based on inequalities on bitvectors.0
bv_ite2idboolrewrite ite that can be simplified to identityfalse
bv_le2extractbooldisassemble bvule to extracttrue
bv_not_simplboolapply simplifications for bvnotfalse
bv_sort_acboolsort the arguments of all AC operatorsfalse
cache_allboolcache all intermediate results.false
elim_andboolconjunctions are rewritten using negation and disjunctionsfalse
elim_itebooleliminate ite in favor of and/ortrue
elim_remboolreplace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).false
elim_sign_extboolexpand sign-ext operator using concat and extracttrue
elim_to_realbooleliminate to_real from arithmetic predicates that contain only integers.false
eq2ineqboolexpand equalities into two inequalitiesfalse
expand_nested_storesboolreplace nested stores by a lambda expressionfalse
expand_powerboolexpand (^ t k) into (* t ... t) if 1 < k <= max_degree.false
expand_select_iteboolexpand select over ite expressionsfalse
expand_select_storeboolconservatively replace a (select (store ...) ...) term by an if-then-else termfalse
expand_store_eqboolreduce (store ...) = (store ...) with a common base into selectsfalse
expand_tanboolreplace (tan x) with (/ (sin x) (cos x)).false
flatboolcreate nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxortrue
flat_and_orboolcreate nary applications for and,ortrue
gcd_roundingbooluse gcd rounding on integer arithmetic atoms.false
hi_div0booluse the 'hardware interpretation' for division by zero (for bit-vector terms)true
hoist_iteboolhoist shared summands under ite expressionsfalse
hoist_mulboolhoist multiplication over summation to minimize number of multiplicationsfalse
ignore_patterns_on_ground_qbodyboolignores patterns on quantifiers that don't mention their bound variables.true
ite_extra_rulesboolextra ite simplifications, these additional simplifications may reduce size locally but increase globallytrue
local_ctxboolperform local (i.e., cheap) context simplificationsfalse
local_ctx_limitunsigned intlimit for applying local context simplifier4294967295
max_degreeunsigned intmax degree of algebraic numbers (and power operators) processed by simplifier.64
max_memoryunsigned intmaximum amount of memory in megabytes4294967295
max_stepsunsigned intmaximum number of steps4294967295
mul2concatboolreplace multiplication by a power of two into a concatenationfalse
mul_to_powerboolcollpase (* t ... t) into (^ t k), it is ignored if expand_power is true.false
pull_cheap_iteboolpull if-then-else terms when cheap.false
push_ite_arithboolpush if-then-else over arithmetic terms.false
push_ite_bvboolpush if-then-else over bit-vector terms.false
push_to_realbooldistribute to_real over * and +.true
rewrite_patternsboolrewrite patterns.false
somboolput polynomials in sum-of-monomials formfalse
som_blowupunsigned intmaximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form10
sort_storeboolsort nested stores when the indices are known to be differentfalse
sort_sumsboolsort the arguments of + application.false
split_concat_eqboolsplit equalities of the form (= (concat t1 t2) t3)false

## Tactic fm​

### Short Description​

Use Fourier-Motzkin to eliminate variables. This strategy can handle conditional bounds (i.e., clauses with at most one constraint).

The tactic occf can be used to put the formula in OCC form.

### Parameters​

ParameterTypeDescriptionDefault
algebraic_number_evaluatorboolsimplify/evaluate expressions containing (algebraic) irrational numbers.true
arith_ineq_lhsboolrewrite inequalities so that right-hand-side is a constant.false
arith_lhsboolall monomials are moved to the left-hand-side, and the right-hand-side is just a constant.false
bit2boolbooltry to convert bit-vector terms of size 1 into Boolean termstrue
blast_distinctboolexpand a distinct predicate into a quadratic number of disequalitiesfalse
blast_distinct_thresholdunsigned intwhen blast_distinct is true, only distinct expressions with less than this number of arguments are blasted4294967295
blast_eq_valueboolblast (some) Bit-vector equalities into bitsfalse
blast_select_storebooleagerly replace all (select (store ..) ..) term by an if-then-else termfalse
bv_extract_propboolattempt to partially propagate extraction inwardsfalse
bv_ineq_consistency_test_maxunsigned intmax size of conjunctions on which to perform consistency test based on inequalities on bitvectors.0
bv_ite2idboolrewrite ite that can be simplified to identityfalse
bv_le2extractbooldisassemble bvule to extracttrue
bv_not_simplboolapply simplifications for bvnotfalse
bv_sort_acboolsort the arguments of all AC operatorsfalse
cache_allboolcache all intermediate results.false
elim_andboolconjunctions are rewritten using negation and disjunctionsfalse
elim_itebooleliminate ite in favor of and/ortrue
elim_remboolreplace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).false
elim_sign_extboolexpand sign-ext operator using concat and extracttrue
elim_to_realbooleliminate to_real from arithmetic predicates that contain only integers.false
eq2ineqboolexpand equalities into two inequalitiesfalse
expand_nested_storesboolreplace nested stores by a lambda expressionfalse
expand_powerboolexpand (^ t k) into (* t ... t) if 1 < k <= max_degree.false
expand_select_iteboolexpand select over ite expressionsfalse
expand_select_storeboolconservatively replace a (select (store ...) ...) term by an if-then-else termfalse
expand_store_eqboolreduce (store ...) = (store ...) with a common base into selectsfalse
expand_tanboolreplace (tan x) with (/ (sin x) (cos x)).false
flatboolcreate nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxortrue
flat_and_orboolcreate nary applications for and,ortrue
fm_cutoff1unsigned intfirst cutoff for FM based on maximum number of lower/upper occurrences.8
fm_cutoff2unsigned intsecond cutoff for FM based on num_lower * num_upper occurrences.256
fm_extraunsigned intmax. increase on the number of inequalities for each FM variable elimination step.0
fm_limitunsigned intmaximum number of constraints, monomials, clauses visited during FM.5000000
fm_occboolconsider inequalities occurring in clauses for FM.false
fm_real_onlyboolconsider only real variables for fourier-motzkin elimination.true
gcd_roundingbooluse gcd rounding on integer arithmetic atoms.false
hi_div0booluse the 'hardware interpretation' for division by zero (for bit-vector terms)true
hoist_iteboolhoist shared summands under ite expressionsfalse
hoist_mulboolhoist multiplication over summation to minimize number of multiplicationsfalse
ignore_patterns_on_ground_qbodyboolignores patterns on quantifiers that don't mention their bound variables.true
ite_extra_rulesboolextra ite simplifications, these additional simplifications may reduce size locally but increase globallytrue
local_ctxboolperform local (i.e., cheap) context simplificationsfalse
local_ctx_limitunsigned intlimit for applying local context simplifier4294967295
max_degreeunsigned intmax degree of algebraic numbers (and power operators) processed by simplifier.64
max_memoryunsigned intmaximum amount of memory in megabytes4294967295
max_stepsunsigned intmaximum number of steps4294967295
mul2concatboolreplace multiplication by a power of two into a concatenationfalse
mul_to_powerboolcollpase (* t ... t) into (^ t k), it is ignored if expand_power is true.false
produce_modelsboolmodel generation.false
pull_cheap_iteboolpull if-then-else terms when cheap.false
push_ite_arithboolpush if-then-else over arithmetic terms.false
push_ite_bvboolpush if-then-else over bit-vector terms.false
push_to_realbooldistribute to_real over * and +.true
rewrite_patternsboolrewrite patterns.false
somboolput polynomials in sum-of-monomials formfalse
som_blowupunsigned intmaximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form10
sort_storeboolsort nested stores when the indices are known to be differentfalse
sort_sumsboolsort the arguments of + application.false
split_concat_eqboolsplit equalities of the form (= (concat t1 t2) t3)false

## Tactic fpa2bv​

### Short Description​

Converts floating points to bit-vector representation.

## Tactic horn​

### Short Description​

Solve a set of Horn clauses using the SPACER engine.

### Long Description​

The SPACER engine is specialized to solving Constrained Horn Clauses. This tactic instructs

## Tactic horn-simplify​

### Short Description​

Apply pre-processing simplification rules to a set of Horn clauses

### Long Description​

This tactic exposes pre-processing simplification rules for Constrained Horn Clauses. They include a repertoire of simplification options that can be controlled by toggling the fp parameters.

### Parameters​

ParameterTypeDescriptionDefault
bmc.linear_unrolling_depthunsigned intMaximal level to explore4294967295
ctrl_cboolenable interrupts from ctrl-ctrue
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_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
timeoutunsigned int(default: infty) timeout in milliseconds.4294967295
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

## Tactic injectivity​

### Short Description:​

• Discover axioms of the form forall x. (= (g (f x)) x Mark f as injective

• Rewrite (sub)terms of the form (= (f x) (f y)) to (= x y) whenever f is injective.

### Notes​

• does not support cores nor proofs

### Parameters​

ParameterTypeDescriptionDefault
max_memoryunsigned int(default: infty) maximum amount of memory in megabytes.4294967295
produce_modelsboolmodel generation.false

## Tactic lia2card​

### Short Description​

Extract 0-1 integer variables used in cardinality and pseudo-Boolean constraints and replace them by Booleans.

### Notes​

• The tactic does not (properly) support proofs or cores.

### Parameters​

ParameterTypeDescriptionDefault
compile_equalitybool(default:false) compile equalities into pseudo-Boolean equality

## Tactic lia2pb​

### Short Description​

Reduce bounded LIA benchmark into 0-1 LIA benchmark.

### Parameters​

ParameterTypeDescriptionDefault
lia2pb_max_bitsunsigned int(default: 32) maximum number of bits to be used (per variable) in lia2pb.
lia2pb_partialbool(default: false) partial lia2pb conversion.
lia2pb_total_bitsunsigned int(default: 2048) total number of bits to be used (per problem) in lia2pb.

## Tactic macro-finder​

### Short Description​

Identifies and applies macros.

### Long Description​

It finds implicit macro definitions in quantifiers. A main instance of a macro an equality that defines a function f using some term t that does not contain f. Other instances of macros are also recognized by the macro finder.

• (forall (x) (= (f x) t))

• not (= (p x) t) is recognized as (p x) = (not t)

• (iff (= (f x) t) cond) rewrites to (f x) = (if cond t else (k x))

• add clause (not (= (k x) t))
• (= (+ (f x) s) t) becomes (= (f x) (- t s))

• (= (+ (* -1 (f x)) x) t) becomes (= (f x) (- (- t s)))

### Notes​

• Supports proofs, unsat cores, but not goals with recursive function definitions.

### Parameters​

ParameterTypeDescriptionDefault
elim_andbool(default: false) eliminate conjunctions during (internal) calls to the simplifier.
max_memoryunsigned int(default: infty) maximum amount of memory in megabytes.4294967295
produce_modelsboolmodel generation.false
produce_proofsboolproof generation.false

## Tactic max-bv-sharing​

### Short Description​

Use heuristics to maximize the sharing of bit-vector expressions such as adders and multipliers

### Long Description​

Rewriter for "maximing" the number of shared terms. The idea is to rewrite AC terms to maximize sharing. This rewriter is particularly useful for reducing the number of Adders and Multipliers before "bit-blasting".

## Tactic nla2bv​

### Short Description​

Convert quantified NIA problems to bounded bit-vector arithmetic problems.

### Notes​

• The tactic creates an under-approximation (a stronger set of formulas)

### Parameters​

ParameterTypeDescriptionDefault
nla2bv_bv_sizeunsigned intdefault bit-vector size used by nla2bv tactic.4
nla2bv_divisorunsigned intnla2bv tactic parameter.2
nla2bv_max_bv_sizeunsigned int(default: inf) maximum bit-vector size used by nla2bv tactic
nla2bv_rootunsigned intnla2bv tactic encodes reals into bit-vectors using expressions of the form a+b*sqrt(c), this parameter sets the value of c used in the encoding.2

## Tactic nlsat​

### Short Description​

(try to) solve goal using a nonlinear arithmetic solver

### Parameters​

ParameterTypeDescriptionDefault
check_lemmasboolcheck lemmas on the fly using an independent nlsat solverfalse
factorbool(default: true) factor polynomials.
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 lifiting 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
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 int(default: infty) maximum amount of memory in megabytes.4294967295
max_primeunsigned int(default: infty) 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 step.
max_search_sizeunsigned int(default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space.
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
minimize_conflictsboolminimize conflictsfalse
num_primesunsigned int(default: 1) 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 lifiting and searching.
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
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

## Tactic nnf​

### Short Description:​

The tactic converts formulas to negation normal form (NNF)

### Long Description​

In NNF, negations only appear in front of atomic formulas.

Standard rules for conversion into negation normal form are:

• (not (and p q)) is converted to (or (not p) (not q))
• (not (or p q)) is converted to (and (not p) (not q))
• (not (not p)) is converted to p
• (not (exists x. p)) is converted to (forall x. (not p))
• (not (forall x. p)) is converted to (exists x. (not p))

Once all negations are pushed inside, the resulting formula is in NNF.

### Notes​

• supports unsat cores, proof terms

### Parameters​

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

## Tactic normalize-bounds​

### Short Description​

Replace $x$ with $x' + l$, when $l \leq x$ where $x'$ is a fresh variable. Note that, after the transformation $0 \leq x'$.

### Notes​

• supports proofs and cores

### Parameters​

ParameterTypeDescriptionDefault
norm_int_onlyboolnormalize only the bounds of integer constants.true
produce_modelsboolmodel generation.false

## Tactic occf​

### Short Description​

Put goal in one constraint per clause normal form

### Long Description​

Put clauses in the assertion set in OOC (one constraint per clause) form. Constraints occurring in formulas that are not clauses are ignored. The formula can be put into CNF by using mk_sat_preprocessor strategy.

### Notes​

• Does not support proofs
• only clauses are considered

## Tactic pb2bv​

### Short Description​

Convert pseudo-boolean constraints to bit-vectors

### Parameters​

ParameterTypeDescriptionDefault
blast_distinctboolexpand a distinct predicate into a quadratic number of disequalitiesfalse
blast_distinct_thresholdunsigned intwhen blast_distinct is true, only distinct expressions with less than this number of arguments are blasted4294967295
cardinality.encodingsymbolencoding used for cardinality constraints: grouped, bimander, ordered, unate, circuitnone
elim_itebooleliminate ite in favor of and/ortrue
flat_and_orboolcreate nary applications for and,ortrue
ite_extra_rulesboolextra ite simplifications, these additional simplifications may reduce size locally but increase globallytrue
keep_cardinality_constraintsboolretain cardinality constraints (don't bit-blast them) and use built-in cardinality solverfalse
local_ctxboolperform local (i.e., cheap) context simplificationsfalse
local_ctx_limitunsigned intlimit for applying local context simplifier4294967295
max_memoryunsigned int(default: infty) maximum amount of memory in megabytes.4294967295
pb.solversymbolencoding used for Pseudo-Boolean constraints: totalizer, sorting, binary_merge, bv, solver. PB constraints are retained if set to 'solver'solver
pb2bv_all_clauses_limitunsigned int(default: 8) maximum number of literals for using equivalent CNF encoding of PB constraint.
pb2bv_cardinality_limitunsigned int(default: inf) limit for using arc-consistent cardinality constraint encoding.

## Tactic propagate-bv-bounds​

### Short Description​

Contextual bounds simplification tactic.

### Notes​

• assumes that bit-vector inequalities have been simplified to use bvule/bvsle

### Parameters​

ParameterTypeDescriptionDefault
max_depthunsigned intmaximum term depth.1024
max_memoryunsigned int(default: infty) maximum amount of memory in megabytes.4294967295
max_stepsunsigned int(default: infty) maximum number of steps.4294967295
propagate_eqboolenable equality propagation from bounds.false

## Tactic propagate-ineqs​

### Short Description​

Propagate ineqs/bounds, remove subsumed inequalities

### Long Description​

This tactic performs the following tasks:

• Propagate bounds using the bound_propagator.

• Eliminate subsumed inequalities.

• For example: x - y >= 3 can be replaced with true if we know that x >= 3 and y <= 0
• Convert inequalities of the form p <= k and p >= k into p = k, where p is a polynomial and k is a constant.

This strategy assumes the input is in arith LHS mode. This can be achieved by using option :arith-lhs true in the simplifier.

### Parameters​

ParameterTypeDescriptionDefault
bound_max_refinementsunsigned int(default: 16) maximum number of bound refinements (per round) for unbounded variables.
bound_thresholddouble(default: 0.05) bound propagation improvement threshold ratio.

## Tactic propagate-values​

### Short Description:​

Tactic for propagating equalities (= t v) where v is a value

### Long Description​

In a context where terms are equated to constants it is invariably beneficial to replace terms, that can be compound, with the constants and then simplify the resulting formulas. The propagate-values tactic accomplishes the task of replacing such terms.

### Notes​

• supports unsat cores

### Parameters​

ParameterTypeDescriptionDefault
algebraic_number_evaluatorboolsimplify/evaluate expressions containing (algebraic) irrational numbers.true
arith_ineq_lhsboolrewrite inequalities so that right-hand-side is a constant.false
arith_lhsboolall monomials are moved to the left-hand-side, and the right-hand-side is just a constant.false
bit2boolbooltry to convert bit-vector terms of size 1 into Boolean termstrue
blast_distinctboolexpand a distinct predicate into a quadratic number of disequalitiesfalse
blast_distinct_thresholdunsigned intwhen blast_distinct is true, only distinct expressions with less than this number of arguments are blasted4294967295
blast_eq_valueboolblast (some) Bit-vector equalities into bitsfalse
blast_select_storebooleagerly replace all (select (store ..) ..) term by an if-then-else termfalse
bv_extract_propboolattempt to partially propagate extraction inwardsfalse
bv_ineq_consistency_test_maxunsigned intmax size of conjunctions on which to perform consistency test based on inequalities on bitvectors.0
bv_ite2idboolrewrite ite that can be simplified to identityfalse
bv_le2extractbooldisassemble bvule to extracttrue
bv_not_simplboolapply simplifications for bvnotfalse
bv_sort_acboolsort the arguments of all AC operatorsfalse
cache_allboolcache all intermediate results.false
elim_andboolconjunctions are rewritten using negation and disjunctionsfalse
elim_itebooleliminate ite in favor of and/ortrue
elim_remboolreplace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).false
elim_sign_extboolexpand sign-ext operator using concat and extracttrue
elim_to_realbooleliminate to_real from arithmetic predicates that contain only integers.false
eq2ineqboolexpand equalities into two inequalitiesfalse
expand_nested_storesboolreplace nested stores by a lambda expressionfalse
expand_powerboolexpand (^ t k) into (* t ... t) if 1 < k <= max_degree.false
expand_select_iteboolexpand select over ite expressionsfalse
expand_select_storeboolconservatively replace a (select (store ...) ...) term by an if-then-else termfalse
expand_store_eqboolreduce (store ...) = (store ...) with a common base into selectsfalse
expand_tanboolreplace (tan x) with (/ (sin x) (cos x)).false
flatboolcreate nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxortrue
flat_and_orboolcreate nary applications for and,ortrue
gcd_roundingbooluse gcd rounding on integer arithmetic atoms.false
hi_div0booluse the 'hardware interpretation' for division by zero (for bit-vector terms)true
hoist_iteboolhoist shared summands under ite expressionsfalse
hoist_mulboolhoist multiplication over summation to minimize number of multiplicationsfalse
ignore_patterns_on_ground_qbodyboolignores patterns on quantifiers that don't mention their bound variables.true
ite_extra_rulesboolextra ite simplifications, these additional simplifications may reduce size locally but increase globallytrue
local_ctxboolperform local (i.e., cheap) context simplificationsfalse
local_ctx_limitunsigned intlimit for applying local context simplifier4294967295
max_degreeunsigned intmax degree of algebraic numbers (and power operators) processed by simplifier.64
max_memoryunsigned intmaximum amount of memory in megabytes4294967295
max_roundsunsigned intmaximum number of rounds.4
max_stepsunsigned intmaximum number of steps4294967295
mul2concatboolreplace multiplication by a power of two into a concatenationfalse
mul_to_powerboolcollpase (* t ... t) into (^ t k), it is ignored if expand_power is true.false
pull_cheap_iteboolpull if-then-else terms when cheap.false
push_ite_arithboolpush if-then-else over arithmetic terms.false
push_ite_bvboolpush if-then-else over bit-vector terms.false
push_to_realbooldistribute to_real over * and +.true
rewrite_patternsboolrewrite patterns.false
somboolput polynomials in sum-of-monomials formfalse
som_blowupunsigned intmaximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form10
sort_storeboolsort nested stores when the indices are known to be differentfalse
sort_sumsboolsort the arguments of + application.false
split_concat_eqboolsplit equalities of the form (= (concat t1 t2) t3)false

## Tactic purify-arith​

### Short Description​

Eliminate unnecessary operators: -, /, div, mod, rem, is-int, to-int, ^, root-objects. These operators can be replaced by introcing fresh variables and using multiplication and addition.

### Parameters​

ParameterTypeDescriptionDefault
algebraic_number_evaluatorboolsimplify/evaluate expressions containing (algebraic) irrational numbers.true
arith_ineq_lhsboolrewrite inequalities so that right-hand-side is a constant.false
arith_lhsboolall monomials are moved to the left-hand-side, and the right-hand-side is just a constant.false
bit2boolbooltry to convert bit-vector terms of size 1 into Boolean termstrue
blast_distinctboolexpand a distinct predicate into a quadratic number of disequalitiesfalse
blast_distinct_thresholdunsigned intwhen blast_distinct is true, only distinct expressions with less than this number of arguments are blasted4294967295
blast_eq_valueboolblast (some) Bit-vector equalities into bitsfalse
blast_select_storebooleagerly replace all (select (store ..) ..) term by an if-then-else termfalse
bv_extract_propboolattempt to partially propagate extraction inwardsfalse
bv_ineq_consistency_test_maxunsigned intmax size of conjunctions on which to perform consistency test based on inequalities on bitvectors.0
bv_ite2idboolrewrite ite that can be simplified to identityfalse
bv_le2extractbooldisassemble bvule to extracttrue
bv_not_simplboolapply simplifications for bvnotfalse
bv_sort_acboolsort the arguments of all AC operatorsfalse
cache_allboolcache all intermediate results.false
completebooladd constraints to make sure that any interpretation of a underspecified arithmetic operators is a function. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-roottrue
elim_andboolconjunctions are rewritten using negation and disjunctionsfalse
elim_inversesbooleliminate inverse trigonometric functions (asin, acos, atan).true
elim_itebooleliminate ite in favor of and/ortrue
elim_remboolreplace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).false
elim_root_objectsbooleliminate root objects.true
elim_sign_extboolexpand sign-ext operator using concat and extracttrue
elim_to_realbooleliminate to_real from arithmetic predicates that contain only integers.false
eq2ineqboolexpand equalities into two inequalitiesfalse
expand_nested_storesboolreplace nested stores by a lambda expressionfalse
expand_powerboolexpand (^ t k) into (* t ... t) if 1 < k <= max_degree.false
expand_select_iteboolexpand select over ite expressionsfalse
expand_select_storeboolconservatively replace a (select (store ...) ...) term by an if-then-else termfalse
expand_store_eqboolreduce (store ...) = (store ...) with a common base into selectsfalse
expand_tanboolreplace (tan x) with (/ (sin x) (cos x)).false
flatboolcreate nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxortrue
flat_and_orboolcreate nary applications for and,ortrue
gcd_roundingbooluse gcd rounding on integer arithmetic atoms.false
hi_div0booluse the 'hardware interpretation' for division by zero (for bit-vector terms)true
hoist_iteboolhoist shared summands under ite expressionsfalse
hoist_mulboolhoist multiplication over summation to minimize number of multiplicationsfalse
ignore_labelsboolremove/ignore labels in the input formula, this option is ignored if proofs are enabledfalse
ignore_patterns_on_ground_qbodyboolignores patterns on quantifiers that don't mention their bound variables.true
ite_extra_rulesboolextra ite simplifications, these additional simplifications may reduce size locally but increase globallytrue
local_ctxboolperform local (i.e., cheap) context simplificationsfalse
local_ctx_limitunsigned intlimit for applying local context simplifier4294967295
max_degreeunsigned intmax degree of algebraic numbers (and power operators) processed by simplifier.64
max_memoryunsigned intmaximum amount of memory in megabytes4294967295
max_stepsunsigned intmaximum number of steps4294967295
modesymbolNNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), fullskolem
mul2concatboolreplace multiplication by a power of two into a concatenationfalse
mul_to_powerboolcollpase (* t ... t) into (^ t k), it is ignored if expand_power is true.false
pull_cheap_iteboolpull if-then-else terms when cheap.false
push_ite_arithboolpush if-then-else over arithmetic terms.false
push_ite_bvboolpush if-then-else over bit-vector terms.false
push_to_realbooldistribute to_real over * and +.true
rewrite_patternsboolrewrite patterns.false
sk_hackboolhack for VCCfalse
somboolput polynomials in sum-of-monomials formfalse
som_blowupunsigned intmaximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form10
sort_storeboolsort nested stores when the indices are known to be differentfalse
sort_sumsboolsort the arguments of + application.false
split_concat_eqboolsplit equalities of the form (= (concat t1 t2) t3)false

## Tactic qe​

### Short Description​

Apply quantifier elimination on quantified sub-formulas.

### Long Description​

The tactic applies quantifier elimination procedures on quantified sub-formulas. It relies on theory plugins that can perform quanifier elimination for selected theories. These plugins include Booleans, bit-vectors, arithmetic (linear), arrays, and data-types (term algebra). It performs feasibility checks on cases to throttle the set of sub-formulas where quantifier elimination is applied.

### Parameters​

ParameterTypeDescriptionDefault
eliminate_variables_as_blockbool(default: true) eliminate variables as a block (true) or one at a time (false)
qe_nonlinearbool(default: false) enable virtual term substitution.

## Tactic qffp​

### Short Description​

Tactic for QF_FP formulas

## Tactic qffpbv​

### Short Description​

Tactic for QF_FPBV formulas

### Parameters​

ParameterTypeDescriptionDefault
abcebooleliminate blocked clauses using asymmetric literalsfalse
accebooleliminate covered clauses using asymmetric added literalsfalse
algebraic_number_evaluatorboolsimplify/evaluate expressions containing (algebraic) irrational numbers.true
anfboolenable ANF based simplification in-processingfalse
anf.delayunsigned intdelay ANF simplification by in-processing round2
anf.exlinboolenable extended linear simplificationfalse
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
arith_ineq_lhsboolrewrite inequalities so that right-hand-side is a constant.false
arith_lhsboolall monomials are moved to the left-hand-side, and the right-hand-side is just a constant.false
array.extensionalboolextensional array theorytrue
array.weakboolweak array theoryfalse
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
auto_configboolautomatically configure solvertrue
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
bit2boolbooltry to convert bit-vector terms of size 1 into Boolean termstrue
blast_distinctboolexpand a distinct predicate into a quadratic number of disequalitiesfalse
blast_distinct_thresholdunsigned intwhen blast_distinct is true, only distinct expressions with less than this number of arguments are blasted4294967295
blast_eq_valueboolblast (some) Bit-vector equalities into bitsfalse
blast_fullboolbit-blast any term with bit-vector sort, this option will make E-matching ineffective in any pattern containing bit-vector terms.false
blast_mulboolbit-blast multipliers (and dividers, remainders).true
blast_quantboolbit-blast quantified variables.false
blast_select_storebooleagerly replace all (select (store ..) ..) term by an if-then-else termfalse
blocked_clause_limitunsigned intmaximum number of literals visited during blocked clause elimination100000000
bound_simplifierboolapply bounds simplification during pre-processingtrue
branching.anti_explorationboolapply anti-exploration heuristic for branch selectionfalse
branching.heuristicsymbolbranching heuristic vsids, chbvsids
burst_searchunsigned intnumber of conflicts before first global simplification100
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
bv_extract_propboolattempt to partially propagate extraction inwardsfalse
bv_ineq_consistency_test_maxunsigned intmax size of conjunctions on which to perform consistency test based on inequalities on bitvectors.0
bv_ite2idboolrewrite ite that can be simplified to identityfalse
bv_le2extractbooldisassemble bvule to extracttrue
bv_not_simplboolapply simplifications for bvnotfalse
bv_sort_acboolsort the arguments of all AC operatorsfalse
cache_allboolcache all intermediate results.false
candidate_modelsboolcreate candidate models even when quantifier or theory reasoning is incompletefalse
cardinality.encodingsymbolencoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuitgrouped
cardinality.solverbooluse cardinality solvertrue
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
ccebooleliminate covered clausesfalse
check_lemmasboolcheck lemmas on the fly using an independent nlsat solverfalse
clause_proofboolrecord a clausal prooffalse
common_patternsboolminimize the number of auxiliary variables during CNF encoding by identifing commonly used patternstrue
completebooladd constraints to make sure that any interpretation of a underspecified arithmetic operators is a function. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-roottrue
context_solveboolsolve equalities under disjunctions.false
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.minimize_partialboolapply partial (cheap) core minimizationfalse
core.validatebool[internal] validate unsat core produced by SMT context. This option is intended for debuggingfalse
cube_depthunsigned intcube depth.1
cutboolenable AIG based simplification in-processingfalse
cut.aigboolextract aigs (and ites) from cluases 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
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 transtivity 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
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 hessitant 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
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
dimacs.coreboolextract core from DIMACS benchmarksfalse
distributivityboolminimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulastrue
distributivity_blowupunsigned intmaximum overhead for applying distributivity during CNF encoding32
div0_ackermann_limitunsigned inta bound for number of congruence Ackermann lemmas for div0 modelling1000
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
dt_lazy_splitsunsigned intHow lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy1
dyn_sub_resbooldynamic subsumption resolution for minimizing learned clausestrue
elim_andboolconjunctions are rewritten using negation and disjunctionsfalse
elim_inversesbooleliminate inverse trigonometric functions (asin, acos, atan).true
elim_itebooleliminate ite in favor of and/ortrue
elim_remboolreplace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).false
elim_root_objectsbooleliminate root objects.true
elim_sign_extboolexpand sign-ext operator using concat and extracttrue
elim_to_realbooleliminate to_real from arithmetic predicates that contain only integers.false
elim_unconstrainedboolpre-processing: eliminate unconstrained subtermstrue
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
eliminate_modbooleliminate modulus from equationstrue
ematchingboolE-Matching based quantifier instantiationtrue
enable_pre_simplifyboolenable pre simplifications before the bounded searchfalse
eq2ineqboolexpand equalities into two inequalitiesfalse
eufboolenable euf solver (this feature is preliminary and not ready for general consumption)false
expand_nested_storesboolreplace nested stores by a lambda expressionfalse
expand_powerboolexpand (^ t k) into (* t ... t) if 1 < k <= max_degree.false
expand_select_iteboolexpand select over ite expressionsfalse
expand_select_storeboolconservatively replace a (select (store ...) ...) term by an if-then-else termfalse
expand_store_eqboolreduce (store ...) = (store ...) with a common base into selectsfalse
expand_tanboolreplace (tan x) with (/ (sin x) (cos x)).false
factorbool(default: true) factor polynomials.
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 lifiting 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
fail_if_inconclusivebool(default: true) fail if found unsat (sat) for under (over) approximated goal.
flatboolcreate nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxortrue
flat_and_orboolcreate nary applications for and,ortrue
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
gcd_roundingbooluse gcd rounding on integer arithmetic atoms.false
hi_div0booluse the 'hardware interpretation' for division by zero (for bit-vector terms)true
hoist_iteboolhoist shared summands under ite expressionsfalse
hoist_mulboolhoist multiplication over summation to minimize number of multiplicationsfalse
ignore_labelsboolremove/ignore labels in the input formula, this option is ignored if proofs are enabledfalse
ignore_patterns_on_ground_qbodyboolignores patterns on quantifiers that don't mention their bound variables.true
inductionboolenable generation of induction lemmasfalse
inline_varsboolinline variables that can be isolated from equations (not supported in incremental mode)false
inprocess.maxunsigned intmaximal number of inprocessing passes4294967295
inprocess.outsymbolfile to dump result of the first inprocessing step and exit
ite_chaingboolminimize the number of auxiliary variables during CNF encoding by identifing if-then-else chainstrue
ite_extrabool(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas
ite_extra_rulesboolextra ite simplifications, these additional simplifications may reduce size locally but increase globallytrue
ite_solverbooluse if-then-else solver.true
lazyunsigned inthow lazy the solver is.0
learnedbool(default: false) collect also learned clauses.
lemma_gc_strategyunsigned intlemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none0
local_ctxboolperform local (i.e., cheap) context simplificationsfalse
local_ctx_limitunsigned intlimit for applying local context simplifier4294967295
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
log_lemmasbooldisplay lemmas as self-contained SMT formulasfalse
logicsymbollogic used to setup the SMT solver
lookahead.cube.depthunsigned intcut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.1
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.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
macro_finderbooltry to find universally quantified formulas that can be viewed as macrosfalse
max_argsunsigned int(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic.
max_conflictsunsigned intmaximum number of conflicts before giving up.4294967295
max_degreeunsigned intmax degree of algebraic numbers (and power operators) processed by simplifier.64
max_memoryunsigned intmaximum amount of memory in megabytes4294967295
max_primeunsigned int(default: infty) 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 step.
max_roundsunsigned intmaximum number of rounds.4
max_search_sizeunsigned int(default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space.
max_stepsunsigned intmaximum number of steps4294967295
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
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
minimize_conflictsboolminimize conflictsfalse
minimize_lemmasboolminimize learned clausestrue
modesymbolNNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), fullskolem
mul2concatboolreplace multiplication by a power of two into a concatenationfalse
mul_to_powerboolcollpase (* t ... t) into (^ t k), it is ignored if expand_power is true.false
nla2bv_bv_sizeunsigned intdefault bit-vector size used by nla2bv tactic.4
nla2bv_divisorunsigned intnla2bv tactic parameter.2
nla2bv_max_bv_sizeunsigned int(default: inf) maximum bit-vector size used by nla2bv tactic
nla2bv_rootunsigned intnla2bv tactic encodes reals into bit-vectors using expressions of the form a+b*sqrt(c), this parameter sets the value of c used in the encoding.2
num_primesunsigned int(default: 1) 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 lifiting and searching.
override_incrementalbooloverride incremental safety gaps. Enable elimination of blocked clauses and variables even if solver is reusedfalse
pb.conflict_frequencyunsigned intconflict frequency for Pseudo-Boolean theory1000
pb.learn_complementsboollearn complement literals for Pseudo-Boolean theorytrue
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, caching, local_searchcaching
phase.stickybooluse sticky phase cachingtrue
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
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
propagate_valuesboolpre-processing: propagate valuestrue
pull_cheap_iteboolpull if-then-else terms when cheap.false
pull_nested_quantifiersboolpre-processing: pull nested quantifiersfalse
push_ite_arithboolpush if-then-else over arithmetic terms.false
push_ite_bvboolpush if-then-else over bit-vector terms.false
push_to_realbooldistribute to_real over * and +.true
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_freqdoublefrequency of random case splits0.01
random_seedunsigned intrandom seed for the smt solver0
randomizeboolrandomize selection of a witness in nlsat.true
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
reorderboolreorder variables.true
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
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
retain_blocked_clausesboolretain blocked clauses as lemmastrue
rewrite_patternsboolrewrite patterns.false
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
seedunsigned intrandom seed.0
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
shuffle_varsbooluse a random variable order.false
simplify.delayunsigned intset initial delay of simplification by a conflict count0
simplify_conflictsboolsimplify conflicts using equalities before resolving them in nlsat solver.true
sk_hackboolhack for VCCfalse
smtbooluse the SAT solver based incremental SMT corefalse
smt.proof.checkboolcheck proofs on the fly during SMT searchfalse
solve_eqsboolpre-processing: solve equalitiestrue
solve_eqs_max_occsunsigned int(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations.4294967295
somboolput polynomials in sum-of-monomials formfalse
som_blowupunsigned intmaximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form10
sort_storeboolsort nested stores when the indices are known to be differentfalse
sort_sumsboolsort the arguments of + application.false
split_concat_eqboolsplit equalities of the form (= (concat t1 t2) t3)false
split_factorsboolapply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0)).true
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
subsumptionbooleliminate subsumed clausestrue
subsumption.limitunsigned intapprox. maximum number of literals visited during subsumption (and subsumption resolution)100000000
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
theory_solverbooltheory solvers.true
threads.cube_frequencyunsigned intfrequency for using cubing2
threads.max_conflictsunsigned intmaximal number of conflicts between rounds of cubing for parallel SMT400
variable_decayunsigned intmultiplier (divided by 100) for the VSIDS activity increment110
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

## Tactic qfnra-nlsat​

### Short Description​

Self-contained tactic that attempts to solve goal using a nonlinear arithmetic solver. It first applies tactics, such as purify-arith to convert the goal into a format where the nlsat tactic applies.

### Parameters​

ParameterTypeDescriptionDefault
algebraic_number_evaluatorboolsimplify/evaluate expressions containing (algebraic) irrational numbers.true
arith_ineq_lhsboolrewrite inequalities so that right-hand-side is a constant.false
arith_lhsboolall monomials are moved to the left-hand-side, and the right-hand-side is just a constant.false
bit2boolbooltry to convert bit-vector terms of size 1 into Boolean termstrue
blast_distinctboolexpand a distinct predicate into a quadratic number of disequalitiesfalse
blast_distinct_thresholdunsigned intwhen blast_distinct is true, only distinct expressions with less than this number of arguments are blasted4294967295
blast_eq_valueboolblast (some) Bit-vector equalities into bitsfalse
blast_select_storebooleagerly replace all (select (store ..) ..) term by an if-then-else termfalse
bv_extract_propboolattempt to partially propagate extraction inwardsfalse
bv_ineq_consistency_test_maxunsigned intmax size of conjunctions on which to perform consistency test based on inequalities on bitvectors.0
bv_ite2idboolrewrite ite that can be simplified to identityfalse
bv_le2extractbooldisassemble bvule to extracttrue
bv_not_simplboolapply simplifications for bvnotfalse
bv_sort_acboolsort the arguments of all AC operatorsfalse
cache_allboolcache all intermediate results.false
check_lemmasboolcheck lemmas on the fly using an independent nlsat solverfalse
common_patternsboolminimize the number of auxiliary variables during CNF encoding by identifing commonly used patternstrue
completebooladd constraints to make sure that any interpretation of a underspecified arithmetic operators is a function. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-roottrue
context_solveboolsolve equalities under disjunctions.false
distributivityboolminimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulastrue
distributivity_blowupunsigned intmaximum overhead for applying distributivity during CNF encoding32
elim_andboolconjunctions are rewritten using negation and disjunctionsfalse
elim_inversesbooleliminate inverse trigonometric functions (asin, acos, atan).true
elim_itebooleliminate ite in favor of and/ortrue
elim_remboolreplace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).false
elim_root_objectsbooleliminate root objects.true
elim_sign_extboolexpand sign-ext operator using concat and extracttrue
elim_to_realbooleliminate to_real from arithmetic predicates that contain only integers.false
eliminate_modbooleliminate modulus from equationstrue
eq2ineqboolexpand equalities into two inequalitiesfalse
expand_nested_storesboolreplace nested stores by a lambda expressionfalse
expand_powerboolexpand (^ t k) into (* t ... t) if 1 < k <= max_degree.false
expand_select_iteboolexpand select over ite expressionsfalse
expand_select_storeboolconservatively replace a (select (store ...) ...) term by an if-then-else termfalse
expand_store_eqboolreduce (store ...) = (store ...) with a common base into selectsfalse
expand_tanboolreplace (tan x) with (/ (sin x) (cos x)).false
factorbool(default: true) factor polynomials.
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 lifiting 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
flatboolcreate nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxortrue
flat_and_orboolcreate nary applications for and,ortrue
gcd_roundingbooluse gcd rounding on integer arithmetic atoms.false
hi_div0booluse the 'hardware interpretation' for division by zero (for bit-vector terms)true
hoist_iteboolhoist shared summands under ite expressionsfalse
hoist_mulboolhoist multiplication over summation to minimize number of multiplicationsfalse
ignore_labelsboolremove/ignore labels in the input formula, this option is ignored if proofs are enabledfalse
ignore_patterns_on_ground_qbodyboolignores patterns on quantifiers that don't mention their bound variables.true
inline_varsboolinline variables that can be isolated from equations (not supported in incremental mode)false
ite_chaingboolminimize the number of auxiliary variables during CNF encoding by identifing if-then-else chainstrue
ite_extrabooladd redundant clauses (that improve unit propagation) when encoding if-then-else formulastrue
ite_extra_rulesboolextra ite simplifications, these additional simplifications may reduce size locally but increase globallytrue
ite_solverbooluse if-then-else solver.true
lazyunsigned inthow lazy the solver is.0
local_ctxboolperform local (i.e., cheap) context simplificationsfalse
local_ctx_limitunsigned intlimit for applying local context simplifier4294967295
log_lemmasbooldisplay lemmas as self-contained SMT formulasfalse
max_argsunsigned int(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic.
max_conflictsunsigned intmaximum number of conflicts.4294967295
max_degreeunsigned intmax degree of algebraic numbers (and power operators) processed by simplifier.64
max_memoryunsigned intmaximum amount of memory in megabytes4294967295
max_primeunsigned int(default: infty) 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 step.
max_roundsunsigned intmaximum number of rounds.4
max_search_sizeunsigned int(default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space.
max_stepsunsigned intmaximum number of steps4294967295
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
minimize_conflictsboolminimize conflictsfalse
modesymbolNNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), fullskolem
mul2concatboolreplace multiplication by a power of two into a concatenationfalse
mul_to_powerboolcollpase (* t ... t) into (^ t k), it is ignored if expand_power is true.false
num_primesunsigned int(default: 1) 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 lifiting and searching.
pull_cheap_iteboolpull if-then-else terms when cheap.false
push_ite_arithboolpush if-then-else over arithmetic terms.false
push_ite_bvboolpush if-then-else over bit-vector terms.false
push_to_realbooldistribute to_real over * and +.true
randomizeboolrandomize selection of a witness in nlsat.true
reorderboolreorder variables.true
rewrite_patternsboolrewrite patterns.false
seedunsigned intrandom seed.0
shuffle_varsbooluse a random variable order.false
simplify_conflictsboolsimplify conflicts using equalities before resolving them in nlsat solver.true
sk_hackboolhack for VCCfalse
solve_eqs_max_occsunsigned int(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations.4294967295
somboolput polynomials in sum-of-monomials formfalse
som_blowupunsigned intmaximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form10
sort_storeboolsort nested stores when the indices are known to be differentfalse
sort_sumsboolsort the arguments of + application.false
split_concat_eqboolsplit equalities of the form (= (concat t1 t2) t3)false
split_factorsboolapply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0)).true
theory_solverbooltheory solvers.true
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

## Tactic quasi-macro-finder​

### Short Description​

dentifies and applies quasi-macros.

### Long Description​

A quasi macro defines a function symbol that contains more arguments than the number of bound variables it defines. The additional arguments are functions of the bound variables.

### Notes​

• Supports proofs and cores

## Tactic recover-01​

### Short Description​

Recover 01 variables from propositional constants.

### Long Description​

Search for clauses of the form

    p  or q or  x = 0    ~p or q or  x = k1    p  or ~q or x = k2    ~p or ~q or x = k1+k2

Then, replaces

• x with k1*y1 + k2*y2
• p with y1 = 1
• q with y2 = 1

where y1 and y2 are fresh 01 variables.

The clauses are also removed.

### Notes​

• does not support proofs, does not support cores

### Parameters​

ParameterTypeDescriptionDefault
algebraic_number_evaluatorboolsimplify/evaluate expressions containing (algebraic) irrational numbers.true
arith_ineq_lhsboolrewrite inequalities so that right-hand-side is a constant.false
arith_lhsboolall monomials are moved to the left-hand-side, and the right-hand-side is just a constant.false
bit2boolbooltry to convert bit-vector terms of size 1 into Boolean termstrue
blast_distinctboolexpand a distinct predicate into a quadratic number of disequalitiesfalse
blast_distinct_thresholdunsigned intwhen blast_distinct is true, only distinct expressions with less than this number of arguments are blasted4294967295
blast_eq_valueboolblast (some) Bit-vector equalities into bitsfalse
blast_select_storebooleagerly replace all (select (store ..) ..) term by an if-then-else termfalse
bv_extract_propboolattempt to partially propagate extraction inwardsfalse
bv_ineq_consistency_test_maxunsigned intmax size of conjunctions on which to perform consistency test based on inequalities on bitvectors.0
bv_ite2idboolrewrite ite that can be simplified to identityfalse
bv_le2extractbooldisassemble bvule to extracttrue
bv_not_simplboolapply simplifications for bvnotfalse
bv_sort_acboolsort the arguments of all AC operatorsfalse
cache_allboolcache all intermediate results.false
elim_andboolconjunctions are rewritten using negation and disjunctionsfalse
elim_itebooleliminate ite in favor of and/ortrue
elim_remboolreplace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).false
elim_sign_extboolexpand sign-ext operator using concat and extracttrue
elim_to_realbooleliminate to_real from arithmetic predicates that contain only integers.false
eq2ineqboolexpand equalities into two inequalitiesfalse
expand_nested_storesboolreplace nested stores by a lambda expressionfalse
expand_powerboolexpand (^ t k) into (* t ... t) if 1 < k <= max_degree.false
expand_select_iteboolexpand select over ite expressionsfalse
expand_select_storeboolconservatively replace a (select (store ...) ...) term by an if-then-else termfalse
expand_store_eqboolreduce (store ...) = (store ...) with a common base into selectsfalse
expand_tanboolreplace (tan x) with (/ (sin x) (cos x)).false
flatboolcreate nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxortrue
flat_and_orboolcreate nary applications for and,ortrue
gcd_roundingbooluse gcd rounding on integer arithmetic atoms.false
hi_div0booluse the 'hardware interpretation' for division by zero (for bit-vector terms)true
hoist_iteboolhoist shared summands under ite expressionsfalse
hoist_mulboolhoist multiplication over summation to minimize number of multiplicationsfalse
ignore_patterns_on_ground_qbodyboolignores patterns on quantifiers that don't mention their bound variables.true
ite_extra_rulesboolextra ite simplifications, these additional simplifications may reduce size locally but increase globallytrue
local_ctxboolperform local (i.e., cheap) context simplificationsfalse
local_ctx_limitunsigned intlimit for applying local context simplifier4294967295
max_degreeunsigned intmax degree of algebraic numbers (and power operators) processed by simplifier.64
max_memoryunsigned intmaximum amount of memory in megabytes4294967295
max_stepsunsigned intmaximum number of steps4294967295
mul2concatboolreplace multiplication by a power of two into a concatenationfalse
mul_to_powerboolcollpase (* t ... t) into (^ t k), it is ignored if expand_power is true.false
pull_cheap_iteboolpull if-then-else terms when cheap.false
push_ite_arithboolpush if-then-else over arithmetic terms.false
push_ite_bvboolpush if-then-else over bit-vector terms.false
push_to_realbooldistribute to_real over * and +.true
recover_01_max_bitsunsigned intmaximum number of bits to consider in a clause.10
rewrite_patternsboolrewrite patterns.false
somboolput polynomials in sum-of-monomials formfalse
som_blowupunsigned intmaximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form10
sort_storeboolsort nested stores when the indices are known to be differentfalse
sort_sumsboolsort the arguments of + application.false
split_concat_eqboolsplit equalities of the form (= (concat t1 t2) t3)false

## Tactic reduce-args​

### Short Description:​

Reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.

### Long Description​

Example, suppose we have a function $f$ with 2 arguments. There are 1000 applications of this function, but the first argument is always $a$, $b$ or $c$. Thus, we replace the $f(t_1, t_2)$ with

• $f_a(t_2)$ if $t_1 = a$
• $f_b(t_2)$ if $t_2 = b$
• $f_c(t_2)$ if $t_2 = c$

Since $f_a$, $f_b$, $f_c$ are new symbols, satisfiability is preserved.

This transformation is very similar in spirit to the Ackermman's reduction. For each function f and argument position of f it checks if all occurrences of f uses a value at position i. The values may be different, but all occurrences have to be values for the reduction to be applicable. It creates a fresh function for each of the different values at position i.

### Notes​

• supports unsat cores
• does not support proof terms

## Tactic reduce-bv-size​

### Short Description​

Rry to reduce bit-vector sizes using inequalities.

### Long Description​

Reduce the number of bits used to encode constants, by using signed bounds. Example: suppose $x$ is a bit-vector of size 8, and we have signed bounds for $x$ such that:

        -2 <= x <= 2

Then, $x$ can be replaced by ((sign-extend 5) k) where k is a fresh bit-vector constant of size 3.

### Notes​

• does not support proofs, nor unsat cores

## Tactic sat​

### Short Description​

Try to solve goal using a SAT solver

## Tactic sat-preprocess​

### Short Description​

Apply SAT solver preprocessing procedures (bounded resolution, Boolean constant propagation, 2-SAT, subsumption, subsumption resolution).

### Parameters​

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 cluases 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 hessitant 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
ite_extrabool(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas
learnedbool(default: false) collect also learned clauses.
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.depthunsigned intcut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.1
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.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
max_conflictsunsigned intmaximum number of conflicts4294967295
max_memoryunsigned int(default: infty) maximum amount of memory in megabytes.4294967295
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, caching, local_searchcaching
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 proofs on the fly during SMT searchfalse
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

## Tactic simplify​

### Short Description:​

The tactic performs algebraic simplifcations on formulas

### Long Description​

The simplify tactic invokes z3's main rewriting engine. The rewriting engine contains support for theory specific simplifications. The set of simplifications invoked is open ended. Useful algebraic simplifications are added to the rewrite engine as they are discovered to be useful.

Note that the simplifier does not ensure that equivalent formulas are simplified to the same form. In other words it does not guarantee canonicity. This contrasts with BDD packages where BDDs constructed from two equivalent formulas are guaranteed to be equal.

### Example​

The simplifier is also exposed as a stand-alone command. There are several options to control its behavior.

### Notes​

• supports unsat cores, proof terms

### Parameters​

ParameterTypeDescriptionDefault
algebraic_number_evaluatorboolsimplify/evaluate expressions containing (algebraic) irrational numbers.true
arith_ineq_lhsboolrewrite inequalities so that right-hand-side is a constant.false
arith_lhsboolall monomials are moved to the left-hand-side, and the right-hand-side is just a constant.false
bit2boolbooltry to convert bit-vector terms of size 1 into Boolean termstrue
blast_distinctboolexpand a distinct predicate into a quadratic number of disequalitiesfalse
blast_distinct_thresholdunsigned intwhen blast_distinct is true, only distinct expressions with less than this number of arguments are blasted4294967295
blast_eq_valueboolblast (some) Bit-vector equalities into bitsfalse
blast_select_storebooleagerly replace all (select (store ..) ..) term by an if-then-else termfalse
bv_extract_propboolattempt to partially propagate extraction inwardsfalse
bv_ineq_consistency_test_maxunsigned intmax size of conjunctions on which to perform consistency test based on inequalities on bitvectors.0
bv_ite2idboolrewrite ite that can be simplified to identityfalse
bv_le2extractbooldisassemble bvule to extracttrue
bv_not_simplboolapply simplifications for bvnotfalse
bv_sort_acboolsort the arguments of all AC operatorsfalse
cache_allboolcache all intermediate results.false
elim_andboolconjunctions are rewritten using negation and disjunctionsfalse
elim_itebooleliminate ite in favor of and/ortrue
elim_remboolreplace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).false
elim_sign_extboolexpand sign-ext operator using concat and extracttrue
elim_to_realbooleliminate to_real from arithmetic predicates that contain only integers.false
eq2ineqboolexpand equalities into two inequalitiesfalse
expand_nested_storesboolreplace nested stores by a lambda expressionfalse
expand_powerboolexpand (^ t k) into (* t ... t) if 1 < k <= max_degree.false
expand_select_iteboolexpand select over ite expressionsfalse
expand_select_storeboolconservatively replace a (select (store ...) ...) term by an if-then-else termfalse
expand_store_eqboolreduce (store ...) = (store ...) with a common base into selectsfalse
expand_tanboolreplace (tan x) with (/ (sin x) (cos x)).false
flatboolcreate nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxortrue
flat_and_orboolcreate nary applications for and,ortrue
gcd_roundingbooluse gcd rounding on integer arithmetic atoms.false
hi_div0booluse the 'hardware interpretation' for division by zero (for bit-vector terms)true
hoist_iteboolhoist shared summands under ite expressionsfalse
hoist_mulboolhoist multiplication over summation to minimize number of multiplicationsfalse
ignore_patterns_on_ground_qbodyboolignores patterns on quantifiers that don't mention their bound variables.true
ite_extra_rulesboolextra ite simplifications, these additional simplifications may reduce size locally but increase globallytrue
local_ctxboolperform local (i.e., cheap) context simplificationsfalse
local_ctx_limitunsigned intlimit for applying local context simplifier4294967295
max_degreeunsigned intmax degree of algebraic numbers (and power operators) processed by simplifier.64
max_memoryunsigned intmaximum amount of memory in megabytes4294967295
max_stepsunsigned intmaximum number of steps4294967295
mul2concatboolreplace multiplication by a power of two into a concatenationfalse
mul_to_powerboolcollpase (* t ... t) into (^ t k), it is ignored if expand_power is true.false
pull_cheap_iteboolpull if-then-else terms when cheap.false
push_ite_arithboolpush if-then-else over arithmetic terms.false
push_ite_bvboolpush if-then-else over bit-vector terms.false
push_to_realbooldistribute to_real over * and +.true
rewrite_patternsboolrewrite patterns.false
somboolput polynomials in sum-of-monomials formfalse
som_blowupunsigned intmaximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form10
sort_storeboolsort nested stores when the indices are known to be differentfalse
sort_sumsboolsort the arguments of + application.false
split_concat_eqboolsplit equalities of the form (= (concat t1 t2) t3)false

## Tactic solve-eqs​

### Short Description​

Solve for variables

### Long Description​

The tactic eliminates variables that can be brought into solved form. For example, the assertion x = f(y + z) can be solved for x, replacing x everywhere by f(x + y). It depends on a set of theory specific equality solvers

• Basic equations

• equations between uninterpreted constants and terms.
• equations written as (if p (= x t) (= x s)) are solved as (= x (if p t s)).
• asserting p or (not p) where p is uninterpreted, causes p to be replaced by true (or false).
• Arithmetic equations

• It solves x mod k = s to x = k * m' + s, where m' is a fresh constant.
• It finds variables with unit coefficients in integer linear equations.
• It solves for x * Y = Z under the side-condition Y != 0 as x = Z/Y.

It also allows solving for uninterpreted constants that only appear in a single disjuction. For example, (or (= x (+ 5 y)) (= y (+ u z))) allows solving for x.

### Example​

(declare-const x Int)(declare-const y Int)(declare-const z Int)(declare-const u Int)(assert (or (and (= x (+ 5 y)) (> u z)) (= y (+ u z))))(apply solve-eqs)

It produces the goal

(goal  (or (not (<= u z)) (= y (+ u z)))  :precision precise :depth 1)

where x was solved as (+ 5 y).

### Notes​

• supports unsat cores
• does not support fine-grained proofs

### Parameters​

ParameterTypeDescriptionDefault
context_solveboolsolve equalities under disjunctions.false
eliminate_modbooleliminate modulus from equationstrue
ite_solverbooluse if-then-else solver.true
solve_eqs_max_occsunsigned int(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations.4294967295
theory_solverbooltheory solvers.true

## Tactic split-clause​

### Short Description​

Tactic that creates a subgoal for each literal in a clause (l_1 or ... or l_n). The tactic fails if the main goal does not contain any clause.

### Parameters​

ParameterTypeDescriptionDefault
split_largest_clausebool(default: false) split the largest clause in the goal.

## Tactic symmetry-reduce​

### Short Description​

Apply symmetry reduction

### Long Description​

The tactic applies symmetry reduction for uninterpreted functions and equalities. It applies a straight-forward adaption of an algorithm proposed for veriT.

## Tactic tseitin-cnf​

### Short Description​

Convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored).

### Long Description​

Puts an assertion set in CNF. Auxiliary variables are used to avoid blowup.

Features:

• Efficient encoding is used for commonly used patterns such as: (iff a (iff b c)) (or (not (or a b)) (not (or a c)) (not (or b c)))`

• Efficient encoding is used for chains of if-then-elses

• Distributivity is applied to non-shared nodes if the blowup is acceptable.

• The features above can be disabled/enabled using parameters.

• The assertion-set is only modified if the resultant set of clauses is "acceptable".

Notes:

• Term-if-then-else expressions are not handled by this strategy. This kind of expression should be processed by other strategies.

• Quantifiers are treated as "theory" atoms. They are viewed as propositional variables by this strategy.

• The assertion set may contain free variables.

• This strategy assumes the assertion_set_rewriter was used before invoking it. In particular, it is more effective when "and" operators were eliminated.

### Parameters​

ParameterTypeDescriptionDefault
algebraic_number_evaluatorboolsimplify/evaluate expressions containing (algebraic) irrational numbers.true
arith_ineq_lhsboolrewrite inequalities so that right-hand-side is a constant.false
arith_lhsboolall monomials are moved to the left-hand-side, and the right-hand-side is just a constant.false
bit2boolbooltry to convert bit-vector terms of size 1 into Boolean termstrue
blast_distinctboolexpand a distinct predicate into a quadratic number of disequalitiesfalse
blast_distinct_thresholdunsigned intwhen blast_distinct is true, only distinct expressions with less than this number of arguments are blasted4294967295
blast_eq_valueboolblast (some) Bit-vector equalities into bitsfalse
blast_select_storebooleagerly replace all (select (store ..) ..) term by an if-then-else termfalse
bv_extract_propboolattempt to partially propagate extraction inwardsfalse
bv_ineq_consistency_test_maxunsigned intmax size of conjunctions on which to perform consistency test based on inequalities on bitvectors.0
bv_ite2idboolrewrite ite that can be simplified to identityfalse
bv_le2extractbooldisassemble bvule to extracttrue
bv_not_simplboolapply simplifications for bvnotfalse
bv_sort_acboolsort the arguments of all AC operatorsfalse
cache_allboolcache all intermediate results.false
common_patternsboolminimize the number of auxiliary variables during CNF encoding by identifing commonly used patternstrue
distributivityboolminimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulastrue
distributivity_blowupunsigned intmaximum overhead for applying distributivity during CNF encoding32
elim_andboolconjunctions are rewritten using negation and disjunctionsfalse
elim_itebooleliminate ite in favor of and/ortrue
elim_remboolreplace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).false
elim_sign_extboolexpand sign-ext operator using concat and extracttrue
elim_to_realbooleliminate to_real from arithmetic predicates that contain only integers.false
eq2ineqboolexpand equalities into two inequalitiesfalse
expand_nested_storesboolreplace nested stores by a lambda expressionfalse
expand_powerboolexpand (^ t k) into (* t ... t) if 1 < k <= max_degree.false
expand_select_iteboolexpand select over ite expressionsfalse
expand_select_storeboolconservatively replace a (select (store ...) ...) term by an if-then-else termfalse
expand_store_eqboolreduce (store ...) = (store ...) with a common base into selectsfalse
expand_tanboolreplace (tan x) with (/ (sin x) (cos x)).false
flatboolcreate nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxortrue
flat_and_orboolcreate nary applications for and,ortrue
gcd_roundingbooluse gcd rounding on integer arithmetic atoms.false
hi_div0booluse the 'hardware interpretation' for division by zero (for bit-vector terms)true
hoist_iteboolhoist shared summands under ite expressionsfalse
hoist_mulboolhoist multiplication over summation to minimize number of multiplicationsfalse
ignore_patterns_on_ground_qbodyboolignores patterns on quantifiers that don't mention their bound variables.true
ite_chaingboolminimize the number of auxiliary variables during CNF encoding by identifing if-then-else chainstrue
ite_extrabooladd redundant clauses (that improve unit propagation) when encoding if-then-else formulastrue
ite_extra_rulesboolextra ite simplifications, these additional simplifications may reduce size locally but increase globallytrue
local_ctxboolperform local (i.e., cheap) context simplificationsfalse
local_ctx_limitunsigned intlimit for applying local context simplifier4294967295
max_degreeunsigned intmax degree of algebraic numbers (and power operators) processed by simplifier.64
max_memoryunsigned int(default: infty) maximum amount of memory in megabytes.4294967295
max_stepsunsigned intmaximum number of steps4294967295
mul2concatboolreplace multiplication by a power of two into a concatenationfalse
mul_to_powerboolcollpase (* t ... t) into (^ t k), it is ignored if expand_power is true.false
pull_cheap_iteboolpull if-then-else terms when cheap.false
push_ite_arithboolpush if-then-else over arithmetic terms.false
push_ite_bvboolpush if-then-else over bit-vector terms.false
push_to_realbooldistribute to_real over * and +.true
rewrite_patternsboolrewrite patterns.false
somboolput polynomials in sum-of-monomials formfalse
som_blowupunsigned intmaximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form10
sort_storeboolsort nested stores when the indices are known to be differentfalse
sort_sumsboolsort the arguments of + application.false
split_concat_eqboolsplit equalities of the form (= (concat t1 t2) t3)false

## Tactic unit-subsume-simplify​

### Short Description​

implify goal using subsumption based on unit propagation

### Long Description​

Background: PDR generates several clauses that subsume each-other. Simplify a goal assuming it is a conjunction of clauses. Subsumed clauses are simplified by using unit-propagation It uses the default SMT solver.