Parameters

Z3 Options

Global Parameters

Parameter	Type	Description	Default
auto_config	bool	use heuristics to automatically select solver and configure it	true
debug_ref_count	bool	debug support for AST reference counting	false
dot_proof_file	string	file in which to output graphical proofs	proof.dot
dump_models	bool	dump models whenever check-sat returns sat	false
encoding	string	string encoding used internally: unicode	bmp
memory_high_watermark	unsigned int	set high watermark for memory consumption (in bytes), if 0 then there is no limit	0
memory_high_watermark_mb	unsigned int	set high watermark for memory consumption (in megabytes), if 0 then there is no limit	0
memory_max_alloc_count	unsigned int	set hard upper limit for memory allocations, if 0 then there is no limit	0
memory_max_size	unsigned int	set hard upper limit for memory consumption (in megabytes), if 0 then there is no limit	0
model	bool	model generation for solvers, this parameter can be overwritten when creating a solver	true
model_validate	bool	validate models produced by solvers	false
proof	bool	proof generation, it must be enabled when the Z3 context is created	false
rlimit	unsigned int	default resource limit used for solvers. Unrestricted when set to 0.	0
smtlib2_compliant	bool	enable/disable SMT-LIB 2.0 compliance	false
stats	bool	enable/disable statistics	false
timeout	unsigned int	(default: infty) timeout in milliseconds.	4294967295
trace	bool	trace generation for VCC	false
trace_file_name	string	trace out file name (see option 'trace')	z3.log
type_check	bool	type checker (alias for well_sorted_check)	true
unsat_core	bool	unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation	false
verbose	unsigned int	be verbose, where the value is the verbosity level	0
warning	bool	enable/disable warning messages	true
well_sorted_check	bool	type checker	false

pi

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

Parameter	Type	Description	Default
arith	unsigned int	0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms	1
arith_weight	unsigned int	default weight for quantifiers where the only available pattern has nested arithmetic terms	5
block_loop_patterns	bool	block looping patterns during pattern inference	true
max_multi_patterns	unsigned int	when patterns are not provided, the prover uses a heuristic to infer them, this option sets the threshold on the number of extra multi-patterns that can be created; by default, the prover creates at most one multi-pattern when there is no unary pattern	0
non_nested_arith_weight	unsigned int	default weight for quantifiers where the only available pattern has non nested arithmetic terms	10
pull_quantifiers	bool	pull nested quantifiers, if no pattern was found	true
use_database	bool	use pattern database	false
warnings	bool	enable/disable warning messages in the pattern inference module	false

tactic

tactic parameters

Parameter	Type	Description	Default
blast_term_ite.max_inflation	unsigned int	multiplicative factor of initial term size.	4294967295
blast_term_ite.max_steps	unsigned int	maximal number of steps allowed for tactic.	4294967295
default_tactic	symbol	overwrite default tactic in strategic solver
propagate_values.max_rounds	unsigned int	maximal number of rounds to propagate values.	4
solve_eqs.context_solve	bool	solve equalities within disjunctions.	true
solve_eqs.ite_solver	bool	use if-then-else solvers.	true
solve_eqs.max_occs	unsigned int	maximum number of occurrences for considering a variable for Gaussian eliminations.	4294967295
solve_eqs.theory_solver	bool	use theory solvers.	true

pp

pretty printer

Parameter	Type	Description	Default
bounded	bool	ignore characters exceeding max width	false
bv_literals	bool	use Bit-Vector literals (e.g, #x0F and #b0101) during pretty printing	true
bv_neg	bool	use bvneg when displaying Bit-Vector literals where the most significant bit is 1	false
decimal	bool	pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a ? if the value is not precise	false
decimal_precision	unsigned int	maximum number of decimal places to be used when pp.decimal=true	10
fixed_indent	bool	use a fixed indentation for applications	false
flat_assoc	bool	flat associative operators (when pretty printing SMT2 terms/formulas)	true
fp_real_literals	bool	use real-numbered floating point literals (e.g, +1.0p-1) during pretty printing	false
max_depth	unsigned int	max. term depth (when pretty printing SMT2 terms/formulas)	5
max_indent	unsigned int	max. indentation in pretty printer	4294967295
max_num_lines	unsigned int	max. number of lines to be displayed in pretty printer	4294967295
max_ribbon	unsigned int	max. ribbon (width - indentation) in pretty printer	80
max_width	unsigned int	max. width in pretty printer	80
min_alias_size	unsigned int	min. size for creating an alias for a shared term (when pretty printing SMT2 terms/formulas)	10
pretty_proof	bool	use slower, but prettier, printer for proofs	false
simplify_implies	bool	simplify nested implications for pretty printing	true
single_line	bool	ignore line breaks when true	false

sat

propositional SAT solver

Parameter	Type	Description	Default
abce	bool	eliminate blocked clauses using asymmetric literals	false
acce	bool	eliminate covered clauses using asymmetric added literals	false
anf	bool	enable ANF based simplification in-processing	false
anf.delay	unsigned int	delay ANF simplification by in-processing round	2
anf.exlin	bool	enable extended linear simplification	false
asymm_branch	bool	asymmetric branching	true
asymm_branch.all	bool	asymmetric branching on all literals per clause	false
asymm_branch.delay	unsigned int	number of simplification rounds to wait until invoking asymmetric branch simplification	1
asymm_branch.limit	unsigned int	approx. maximum number of literals visited during asymmetric branching	100000000
asymm_branch.rounds	unsigned int	maximal number of rounds to run asymmetric branch simplifications if progress is made	2
asymm_branch.sampled	bool	use sampling based asymmetric branching based on binary implication graph	true
ate	bool	asymmetric tautology elimination	true
backtrack.conflicts	unsigned int	number of conflicts before enabling chronological backtracking	4000
backtrack.scopes	unsigned int	number of scopes to enable chronological backtracking	100
bca	bool	blocked clause addition - add blocked binary clauses	false
bce	bool	eliminate blocked clauses	false
bce_at	unsigned int	eliminate blocked clauses only once at the given simplification round	2
bce_delay	unsigned int	delay eliminate blocked clauses until simplification round	2
binspr	bool	enable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates models	false
blocked_clause_limit	unsigned int	maximum number of literals visited during blocked clause elimination	100000000
branching.anti_exploration	bool	apply anti-exploration heuristic for branch selection	false
branching.heuristic	symbol	branching heuristic vsids, chb	vsids
burst_search	unsigned int	number of conflicts before first global simplification	100
cardinality.encoding	symbol	encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit	grouped
cardinality.solver	bool	use cardinality solver	true
cce	bool	eliminate covered clauses	false
core.minimize	bool	minimize computed core	false
core.minimize_partial	bool	apply partial (cheap) core minimization	false
cut	bool	enable AIG based simplification in-processing	false
cut.aig	bool	extract aigs (and ites) from clauses for cut simplification	false
cut.delay	unsigned int	delay cut simplification by in-processing round	2
cut.dont_cares	bool	integrate dont cares with cuts	true
cut.force	bool	force redoing cut-enumeration until a fixed-point	false
cut.lut	bool	extract luts from clauses for cut simplification	false
cut.npn3	bool	extract 3 input functions from clauses for cut simplification	false
cut.redundancies	bool	integrate redundancy checking of cuts	true
cut.xor	bool	extract xors from clauses for cut simplification	false
ddfw.init_clause_weight	unsigned int	initial clause weight for DDFW local search	8
ddfw.reinit_base	unsigned int	increment basis for geometric backoff scheme of re-initialization of weights	10000
ddfw.restart_base	unsigned int	number of flips used a starting point for hesitant restart backoff	100000
ddfw.threads	unsigned int	number of ddfw threads to run in parallel with sat solver	0
ddfw.use_reward_pct	unsigned int	percentage to pick highest reward variable when it has reward 0	15
ddfw_search	bool	use ddfw local search instead of CDCL	false
dimacs.core	bool	extract core from DIMACS benchmarks	false
drat.activity	bool	dump variable activities	false
drat.binary	bool	use Binary DRAT output format	false
drat.check_sat	bool	build up internal trace, check satisfying model	false
drat.check_unsat	bool	build up internal proof and check	false
drat.disable	bool	override anything that enables DRAT	false
drat.file	symbol	file to dump DRAT proofs
dyn_sub_res	bool	dynamic subsumption resolution for minimizing learned clauses	true
elim_vars	bool	enable variable elimination using resolution during simplification	true
elim_vars_bdd	bool	enable variable elimination using BDD recompilation during simplification	true
elim_vars_bdd_delay	unsigned int	delay elimination of variables using BDDs until after simplification round	3
enable_pre_simplify	bool	enable pre simplifications before the bounded search	false
euf	bool	enable euf solver (this feature is preliminary and not ready for general consumption)	false
force_cleanup	bool	force cleanup to remove tautologies and simplify clauses	false
gc	symbol	garbage collection strategy: psm, glue, glue_psm, dyn_psm	glue_psm
gc.burst	bool	perform eager garbage collection during initialization	false
gc.defrag	bool	defragment clauses when garbage collecting	true
gc.increment	unsigned int	increment to the garbage collection threshold	500
gc.initial	unsigned int	learned clauses garbage collection frequency	20000
gc.k	unsigned int	learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)	7
gc.small_lbd	unsigned int	learned clauses with small LBD are never deleted (only used in dyn_psm)	3
inprocess.max	unsigned int	maximal number of inprocessing passes	4294967295
inprocess.out	symbol	file to dump result of the first inprocessing step and exit
local_search	bool	use local search instead of CDCL	false
local_search_dbg_flips	bool	write debug information for number of flips	false
local_search_mode	symbol	local search algorithm, either default wsat or qsat	wsat
local_search_threads	unsigned int	number of local search threads to find satisfiable solution	0
lookahead.cube.cutoff	symbol	cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat	depth
lookahead.cube.depth	unsigned int	cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.	1
lookahead.cube.fraction	double	adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat	0.4
lookahead.cube.freevars	double	cube free variable fraction. Used when lookahead.cube.cutoff is freevars	0.8
lookahead.cube.psat.clause_base	double	clause base for PSAT cutoff	2
lookahead.cube.psat.trigger	double	trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat	5
lookahead.cube.psat.var_exp	double	free variable exponent for PSAT cutoff	1
lookahead.delta_fraction	double	number between 0 and 1, the smaller the more literals are selected for double lookahead	1.0
lookahead.double	bool	enable double lookahead	true
lookahead.global_autarky	bool	prefer to branch on variables that occur in clauses that are reduced	false
lookahead.preselect	bool	use pre-selection of subset of variables for branching	false
lookahead.reward	symbol	select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu	march_cu
lookahead.use_learned	bool	use learned clauses when selecting lookahead literal	false
lookahead_scores	bool	extract lookahead scores. A utility that can only be used from the DIMACS front-end	false
lookahead_simplify	bool	use lookahead solver during simplification	false
lookahead_simplify.bca	bool	add learned binary clauses as part of lookahead simplification	true
max_conflicts	unsigned int	maximum number of conflicts	4294967295
max_memory	unsigned int	maximum amount of memory in megabytes	4294967295
minimize_lemmas	bool	minimize learned clauses	true
override_incremental	bool	override incremental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused	false
pb.lemma_format	symbol	generate either cardinality or pb lemmas	cardinality
pb.min_arity	unsigned int	minimal arity to compile pb/cardinality constraints to CNF	9
pb.resolve	symbol	resolution strategy for boolean algebra solver: cardinality, rounding	cardinality
pb.solver	symbol	method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), binary_merge, segmented, solver (use native solver)	solver
phase	symbol	phase selection strategy: always_false, always_true, basic_caching, random, caching	caching
phase.sticky	bool	use sticky phase caching	true
prob_search	bool	use probsat local search instead of CDCL	false
probing	bool	apply failed literal detection during simplification	true
probing_binary	bool	probe binary clauses	true
probing_cache	bool	add binary literals as lemmas	true
probing_cache_limit	unsigned int	cache binaries unless overall memory usage exceeds cache limit	1024
probing_limit	unsigned int	limit to the number of probe calls	5000000
propagate.prefetch	bool	prefetch watch lists for assigned literals	true
random_freq	double	frequency of random case splits	0.01
random_seed	unsigned int	random seed	0
reorder.activity_scale	unsigned int	scaling factor for activity update	100
reorder.base	unsigned int	number of conflicts per random reorder	4294967295
reorder.itau	double	inverse temperature for softmax	4.0
rephase.base	unsigned int	number of conflicts per rephase	1000
resolution.cls_cutoff1	unsigned int	limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination	100000000
resolution.cls_cutoff2	unsigned int	limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination	700000000
resolution.limit	unsigned int	approx. maximum number of literals visited during variable elimination	500000000
resolution.lit_cutoff_range1	unsigned int	second cutoff (total number of literals) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses	700
resolution.lit_cutoff_range2	unsigned int	second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2	400
resolution.lit_cutoff_range3	unsigned int	second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff2	300
resolution.occ_cutoff	unsigned int	first cutoff (on number of positive/negative occurrences) for Boolean variable elimination	10
resolution.occ_cutoff_range1	unsigned int	second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses	8
resolution.occ_cutoff_range2	unsigned int	second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2	5
resolution.occ_cutoff_range3	unsigned int	second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff2	3
restart	symbol	restart strategy: static, luby, ema or geometric	ema
restart.emafastglue	double	ema alpha factor for fast moving average	0.03
restart.emaslowglue	double	ema alpha factor for slow moving average	1e-05
restart.factor	double	restart increment factor for geometric strategy	1.5
restart.fast	bool	use fast restart approach only removing less active literals.	true
restart.initial	unsigned int	initial restart (number of conflicts)	2
restart.margin	double	margin between fast and slow restart factors. For ema	1.1
restart.max	unsigned int	maximal number of restarts.	4294967295
retain_blocked_clauses	bool	retain blocked clauses as lemmas	true
scc	bool	eliminate Boolean variables by computing strongly connected components	true
scc.tr	bool	apply transitive reduction, eliminate redundant binary clauses	true
search.sat.conflicts	unsigned int	period for solving for sat (in number of conflicts)	400
search.unsat.conflicts	unsigned int	period for solving for unsat (in number of conflicts)	400
simplify.delay	unsigned int	set initial delay of simplification by a conflict count	0
smt	bool	use the SAT solver based incremental SMT core	false
smt.proof.check	bool	check SMT proof while it is created	false
smt.proof.check_rup	bool	apply forward RUP proof checking	true
subsumption	bool	eliminate subsumed clauses	true
subsumption.limit	unsigned int	approx. maximum number of literals visited during subsumption (and subsumption resolution)	100000000
threads	unsigned int	number of parallel threads to use	1
variable_decay	unsigned int	multiplier (divided by 100) for the VSIDS activity increment	110

solver

solver parameters

Parameter	Type	Description	Default
axioms2files	bool	print negated theory axioms to separate files during search	false
cancel_backup_file	symbol	file to save partial search state if search is canceled
instantiations2console	bool	print quantifier instantiations to the console	false
lemmas2console	bool	print lemmas during search	false
proof.check	bool	check proof logs	true
proof.log	symbol	log clause proof trail into a file
proof.save	bool	save proof log into a proof object that can be extracted using (get-proof)	false
proof.trim	bool	trim and save proof into a proof object that an be extracted using (get-proof)	false
smtlib2_log	symbol	file to save solver interaction
timeout	unsigned int	timeout on the solver object; overwrites a global timeout	4294967295

opt

optimization parameters

Parameter	Type	Description	Default
dump_benchmarks	bool	dump benchmarks for profiling	false
dump_models	bool	display intermediary models to stdout	false
elim_01	bool	eliminate 01 variables	true
enable_core_rotate	bool	enable core rotation to both sample cores and correction sets	false
enable_lns	bool	enable LNS during weighted maxsat	false
enable_sat	bool	enable the new SAT core for propositional constraints	true
enable_sls	bool	enable SLS tuning during weighted maxsat	false
incremental	bool	set incremental mode. It disables pre-processing and enables adding constraints in model event handler	false
lns_conflicts	unsigned int	initial conflict count for LNS search	1000
maxlex.enable	bool	enable maxlex heuristic for lexicographic MaxSAT problems	true
maxres.add_upper_bound_block	bool	restrict upper bound with constraint	false
maxres.hill_climb	bool	give preference for large weight cores	true
maxres.max_core_size	unsigned int	break batch of generated cores if size reaches this number	3
maxres.max_correction_set_size	unsigned int	allow generating correction set constraints up to maximal size	3
maxres.max_num_cores	unsigned int	maximal number of cores per round	200
maxres.maximize_assignment	bool	find an MSS/MCS to improve current assignment	false
maxres.pivot_on_correction_set	bool	reduce soft constraints if the current correction set is smaller than current core	true
maxres.wmax	bool	use weighted theory solver to constrain upper bounds	false
maxsat_engine	symbol	select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'maxres-bin', 'rc2'	maxres
optsmt_engine	symbol	select optimization engine: 'basic', 'symba'	basic
pb.compile_equality	bool	compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalities)	false
pp.neat	bool	use neat (as opposed to less readable, but faster) pretty printer when displaying context	true
pp.wcnf	bool	print maxsat benchmark into wcnf format	false
priority	symbol	select how to prioritize objectives: 'lex' (lexicographic), 'pareto', 'box'	lex
rc2.totalizer	bool	use totalizer for rc2 encoding	true
rlimit	unsigned int	resource limit (0 means no limit)	0
solution_prefix	symbol	path prefix to dump intermediary, but non-optimal, solutions
timeout	unsigned int	timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)	4294967295

parallel

parameters for parallel solver

Parameter	Type	Description	Default
conquer.backtrack_frequency	unsigned int	frequency to apply core minimization during conquer	10
conquer.batch_size	unsigned int	number of cubes to batch together for fast conquer	100
conquer.delay	unsigned int	delay of cubes until applying conquer	10
conquer.restart.max	unsigned int	maximal number of restarts during conquer phase	5
enable	bool	enable parallel solver by default on selected tactics (for QF_BV)	false
simplify.exp	double	restart and inprocess max is multiplied by simplify.exp ^ depth	1
simplify.inprocess.max	unsigned int	maximal number of inprocessing steps during simplification	2
simplify.max_conflicts	unsigned int	maximal number of conflicts during simplification phase	4294967295
simplify.restart.max	unsigned int	maximal number of restarts during simplification phase	5000
threads.max	unsigned int	caps maximal number of threads below the number of processors	10000

nnf

negation normal form

Parameter	Type	Description	Default
ignore_labels	bool	remove/ignore labels in the input formula, this option is ignored if proofs are enabled	false
max_memory	unsigned int	maximum amount of memory in megabytes	4294967295
mode	symbol	NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full	skolem
sk_hack	bool	hack for VCC	false

algebraic

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

Parameter	Type	Description	Default
factor	bool	use polynomial factorization to simplify polynomials representing algebraic numbers	true
factor_max_prime	unsigned int	parameter 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 step	31
factor_num_primes	unsigned int	parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifting and searching	1
factor_search_size	unsigned int	parameter 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 space	5000
min_mag	unsigned int	Z3 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^16	16
zero_accuracy	unsigned int	one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k)	0

combined_solver

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

Parameter	Type	Description	Default
ignore_solver1	bool	if true, solver 2 is always used	false
solver2_timeout	unsigned int	fallback to solver 1 after timeout even when in incremental model	4294967295
solver2_unknown	unsigned int	what should be done when solver 2 returns unknown: 0 - just return unknown, 1 - execute solver 1 if quantifier free problem, 2 - execute solver 1	1

rcf

real closed fields

Parameter	Type	Description	Default
clean_denominators	bool	clean denominators before root isolation	true
inf_precision	unsigned int	a value k that is the initial interval size (i.e., (0, 1/2^l)) used as an approximation for infinitesimal values	24
initial_precision	unsigned int	a value k that is the initial interval size (as 1/2^k) when creating transcendentals and approximated division	24
lazy_algebraic_normalization	bool	during sturm-seq and square-free polynomial computations, only normalize algebraic polynomial expressions when the defining polynomial is monic	true
max_precision	unsigned int	during sign determination we switch from interval arithmetic to complete methods when the interval size is less than 1/2^k, where k is the max_precision	128
use_prem	bool	use pseudo-remainder instead of remainder when computing GCDs and Sturm-Tarski sequences	true

ackermannization

solving UF via ackermannization

Parameter	Type	Description	Default
eager	bool	eagerly instantiate all congruence rules	true
inc_sat_backend	bool	use incremental SAT	false
sat_backend	bool	use SAT rather than SMT in qfufbv_ackr_tactic	false

nlsat

nonlinear solver

Parameter	Type	Description	Default
check_lemmas	bool	check lemmas on the fly using an independent nlsat solver	false
factor	bool	factor polynomials produced during conflict resolution.	true
inline_vars	bool	inline variables that can be isolated from equations (not supported in incremental mode)	false
lazy	unsigned int	how lazy the solver is.	0
log_lemmas	bool	display lemmas as self-contained SMT formulas	false
max_conflicts	unsigned int	maximum number of conflicts.	4294967295
max_memory	unsigned int	maximum amount of memory in megabytes	4294967295
minimize_conflicts	bool	minimize conflicts	false
randomize	bool	randomize selection of a witness in nlsat.	true
reorder	bool	reorder variables.	true
seed	unsigned int	random seed.	0
shuffle_vars	bool	use a random variable order.	false
simplify_conflicts	bool	simplify conflicts using equalities before resolving them in nlsat solver.	true

fp

fixedpoint parameters

Parameter	Type	Description	Default
bmc.linear_unrolling_depth	unsigned int	Maximal level to explore	4294967295
datalog.all_or_nothing_deltas	bool	compile 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 not	false
datalog.check_relation	symbol	name of default relation to check. operations on the default relation will be verified using SMT solving	null
datalog.compile_with_widening	bool	widening will be used to compile recursive rules	false
datalog.dbg_fpr_nonempty_relation_signature	bool	if 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 otherwise	false
datalog.default_relation	symbol	default relation implementation: external_relation, pentagon	pentagon
datalog.default_table	symbol	default table implementation: sparse, hashtable, bitvector, interval	sparse
datalog.default_table_checked	bool	if true, the default table will be default_table inside a wrapper that checks that its results are the same as of default_table_checker table	false
datalog.default_table_checker	symbol	see default_table_checked	null
datalog.explanations_on_relation_level	bool	if 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_explanations	bool	produce explanations for produced facts when using the datalog engine	false
datalog.initial_restart_timeout	unsigned int	length of saturation run before the first restart (in ms), zero means no restarts	0
datalog.magic_sets_for_queries	bool	magic set transformation will be used for queries	false
datalog.output_profile	bool	determines whether profile information should be output when outputting Datalog rules or instructions	false
datalog.print.tuples	bool	determines whether tuples for output predicates should be output	true
datalog.profile_timeout_milliseconds	unsigned int	instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list	0
datalog.similarity_compressor	bool	rules that differ only in values of constants will be merged into a single rule	true
datalog.similarity_compressor_threshold	unsigned int	if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged	11
datalog.subsumption	bool	if true, removes/filters predicates with total transitions	true
datalog.timeout	unsigned int	Time limit used for saturation	0
datalog.unbound_compressor	bool	auxiliary relations will be introduced to avoid unbound variables in rule heads	true
datalog.use_map_names	bool	use names from map files when displaying tuples	true
engine	symbol	Select: auto-config, datalog, bmc, spacer	auto-config
generate_proof_trace	bool	trace for 'sat' answer as proof object	false
print_aig	symbol	Dump clauses in AIG text format (AAG) to the given file name
print_answer	bool	print answer instance(s) to query	false
print_boogie_certificate	bool	print certificate for reachability or non-reachability using a format understood by Boogie	false
print_certificate	bool	print certificate for reachability or non-reachability	false
print_fixedpoint_extensions	bool	use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules	true
print_low_level_smt2	bool	use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)	false
print_statistics	bool	print statistics	false
print_with_variable_declarations	bool	use variable declarations when displaying rules (instead of attempting to use original names)	true
spacer.arith.solver	unsigned int	arithmetic 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 solver	2
spacer.blast_term_ite_inflation	unsigned int	Maximum inflation for non-Boolean ite-terms expansion: 0 (none), k (multiplicative)	3
spacer.ctp	bool	Enable counterexample-to-pushing	true
spacer.dump_benchmarks	bool	Dump SMT queries as benchmarks	false
spacer.dump_threshold	double	Threshold in seconds on dumping benchmarks	5.0
spacer.elim_aux	bool	Eliminate auxiliary variables in reachability facts	true
spacer.eq_prop	bool	Enable equality and bound propagation in arithmetic	true
spacer.expand_bnd	bool	Enable expand-bound lemma generalization	false
spacer.gg.concretize	bool	Enable global guidance concretize	true
spacer.gg.conjecture	bool	Enable global guidance conjecture	true
spacer.gg.subsume	bool	Enable global guidance subsume	true
spacer.global	bool	Enable global guidance	false
spacer.gpdr	bool	Use GPDR solving strategy for non-linear CHC	false
spacer.gpdr.bfs	bool	Use BFS exploration strategy for expanding model search	true
spacer.ground_pobs	bool	Ground pobs by using values from a model	true
spacer.iuc	unsigned int	0 = use old implementation of unsat-core-generation, 1 = use new implementation of IUC generation, 2 = use new implementation of IUC + min-cut optimization	1
spacer.iuc.arith	unsigned int	0 = 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 plugin	1
spacer.iuc.debug_proof	bool	prints proof used by unsat-core-learner for debugging purposes (debugging)	false
spacer.iuc.old_hyp_reducer	bool	use old hyp reducer instead of new implementation, for debugging only	false
spacer.iuc.print_farkas_stats	bool	prints 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_literals	bool	Split Farkas literals	false
spacer.keep_proxy	bool	keep proxy variables (internal parameter)	true
spacer.logic	symbol	SMT-LIB logic to configure internal SMT solvers
spacer.max_level	unsigned int	Maximum level to explore	4294967295
spacer.max_num_contexts	unsigned int	maximal number of contexts to create	500
spacer.mbqi	bool	Enable mbqi	true
spacer.min_level	unsigned int	Minimal level to explore	0
spacer.native_mbp	bool	Use native mbp of Z3	true
spacer.order_children	unsigned int	SPACER: order of enqueuing children in non-linear rules : 0 (original), 1 (reverse), 2 (random)	0
spacer.p3.share_invariants	bool	Share invariants lemmas	false
spacer.p3.share_lemmas	bool	Share frame lemmas	false
spacer.propagate	bool	Enable propagate/pushing phase	true
spacer.push_pob	bool	push blocked pobs to higher level	false
spacer.push_pob_max_depth	unsigned int	Maximum depth at which push_pob is enabled	4294967295
spacer.q3	bool	Allow quantified lemmas in frames	true
spacer.q3.instantiate	bool	Instantiate quantified lemmas	true
spacer.q3.qgen.normalize	bool	normalize cube before quantified generalization	true
spacer.q3.use_qgen	bool	use quantified lemma generalizer	false
spacer.random_seed	unsigned int	Random seed to be used by SMT solver	0
spacer.reach_dnf	bool	Restrict reachability facts to DNF	true
spacer.reset_pob_queue	bool	SPACER: reset pob obligation queue when entering a new level	true
spacer.restart_initial_threshold	unsigned int	Initial threshold for restarts	10
spacer.restarts	bool	Enable resetting obligation queue	false
spacer.simplify_lemmas_post	bool	simplify derived lemmas after inductive propagation	false
spacer.simplify_lemmas_pre	bool	simplify derived lemmas before inductive propagation	false
spacer.simplify_pob	bool	simplify pobs by removing redundant constraints	false
spacer.trace_file	symbol	Log file for progress events
spacer.use_array_eq_generalizer	bool	SPACER: attempt to generalize lemmas with array equalities	true
spacer.use_bg_invs	bool	Enable external background invariants	false
spacer.use_derivations	bool	SPACER: using derivation mechanism to cache intermediate results for non-linear rules	true
spacer.use_euf_gen	bool	Generalize lemmas and pobs using implied equalities	false
spacer.use_inc_clause	bool	Use incremental clause to represent trans	true
spacer.use_inductive_generalizer	bool	generalize lemmas using induction strengthening	true
spacer.use_iuc	bool	Enable Interpolating Unsat Core(IUC) for lemma generalization	true
spacer.use_lemma_as_cti	bool	SPACER: use a lemma instead of a CTI in flexible_trace	false
spacer.use_lim_num_gen	bool	Enable limit numbers generalizer to get smaller numbers	false
spacer.validate_lemmas	bool	Validate each lemma after generalization	false
spacer.weak_abs	bool	Weak abstraction	true
tab.selection	symbol	selection method for tabular strategy: weight (default), first, var-use	weight
validate	bool	validate result (by proof checking or model checking)	false
xform.array_blast	bool	try to eliminate local array terms using Ackermannization -- some array terms may remain	false
xform.array_blast_full	bool	eliminate all local array variables by QE	false
xform.bit_blast	bool	bit-blast bit-vectors	false
xform.coalesce_rules	bool	coalesce rules	false
xform.coi	bool	use cone of influence simplification	true
xform.compress_unbound	bool	compress tails with unbound variables	true
xform.elim_term_ite	bool	Eliminate term-ite expressions	false
xform.elim_term_ite.inflation	unsigned int	Maximum inflation for non-Boolean ite-terms blasting: 0 (none), k (multiplicative)	3
xform.fix_unbound_vars	bool	fix unbound variables in tail	false
xform.inline_eager	bool	try eager inlining of rules	true
xform.inline_linear	bool	try linear inlining method	true
xform.inline_linear_branch	bool	try linear inlining method with potential expansion	false
xform.instantiate_arrays	bool	Transforms P(a) into P(i, a[i] a)	false
xform.instantiate_arrays.enforce	bool	Transforms P(a) into P(i, a[i]), discards a from predicate	false
xform.instantiate_arrays.nb_quantifier	unsigned int	Gives the number of quantifiers per array	1
xform.instantiate_arrays.slice_technique	symbol	<no-slicing>=> GetId(i) = i, <smash> => GetId(i) = true	no-slicing
xform.instantiate_quantifiers	bool	instantiate quantified Horn clauses using E-matching heuristic	false
xform.magic	bool	perform symbolic magic set transformation	false
xform.quantify_arrays	bool	create quantified Horn clauses from clauses with arrays	false
xform.scale	bool	add scaling variable to linear real arithmetic clauses	false
xform.slice	bool	simplify clause set using slicing	true
xform.subsumption_checker	bool	Enable subsumption checker (no support for model conversion)	true
xform.tail_simplifier_pve	bool	propagate_variable_equivalences	true
xform.transform_arrays	bool	Rewrites arrays equalities and applies select over store	false
xform.unfold_rules	unsigned int	unfold rules statically using iterative squaring	0

smt

smt solver based on lazy smt

Parameter	Type	Description	Default
arith.auto_config_simplex	bool	force simplex solver in auto_config	false
arith.bprop_on_pivoted_rows	bool	propagate bounds on rows changed by the pivot operation	true
arith.branch_cut_ratio	unsigned int	branch/cut ratio for linear integer arithmetic	2
arith.dump_lemmas	bool	dump arithmetic theory lemmas to files	false
arith.eager_eq_axioms	bool	eager equality axioms	true
arith.enable_hnf	bool	enable hnf (Hermite Normal Form) cuts	true
arith.greatest_error_pivot	bool	Pivoting strategy	false
arith.ignore_int	bool	treat integer variables as real	false
arith.int_eq_branch	bool	branching using derived integer equations	false
arith.min	bool	minimize cost	false
arith.nl	bool	(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2	true
arith.nl.branching	bool	branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2	true
arith.nl.delay	unsigned int	number of calls to final check before invoking bounded nlsat check	500
arith.nl.expp	bool	expensive patching	false
arith.nl.gr_q	unsigned int	grobner's quota	10
arith.nl.grobner	bool	run grobner's basis heuristic	true
arith.nl.grobner_cnfl_to_report	unsigned int	grobner's maximum number of conflicts to report	1
arith.nl.grobner_eqs_growth	unsigned int	grobner's number of equalities growth	10
arith.nl.grobner_expr_degree_growth	unsigned int	grobner's maximum expr degree growth	2
arith.nl.grobner_expr_size_growth	unsigned int	grobner's maximum expr size growth	2
arith.nl.grobner_frequency	unsigned int	grobner's call frequency	4
arith.nl.grobner_max_simplified	unsigned int	grobner's maximum number of simplifications	10000
arith.nl.grobner_subs_fixed	unsigned int	0 - no subs, 1 - substitute, 2 - substitute fixed zeros only	1
arith.nl.horner	bool	run horner's heuristic	true
arith.nl.horner_frequency	unsigned int	horner's call frequency	4
arith.nl.horner_row_length_limit	unsigned int	row is disregarded by the heuristic if its length is longer than the value	10
arith.nl.horner_subs_fixed	unsigned int	0 - no subs, 1 - substitute, 2 - substitute fixed zeros only	2
arith.nl.nra	bool	call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6	true
arith.nl.order	bool	run order lemmas	true
arith.nl.rounds	unsigned int	threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2	1024
arith.nl.tangents	bool	run tangent lemmas	true
arith.print_ext_var_names	bool	print external variable names	false
arith.print_stats	bool	print statistic	false
arith.propagate_eqs	bool	propagate (cheap) equalities	true
arith.propagation_mode	unsigned int	0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds	1
arith.random_initial_value	bool	use random initial values in the simplex-based procedure for linear arithmetic	false
arith.rep_freq	unsigned int	the report frequency, in how many iterations print the cost and other info	0
arith.simplex_strategy	unsigned int	simplex strategy for the solver	0
arith.solver	unsigned int	arithmetic 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 solver	6
array.extensional	bool	extensional array theory	true
array.weak	bool	weak array theory	false
auto_config	bool	automatically configure solver	true
bv.delay	bool	delay internalize expensive bit-vector operations	false
bv.enable_int2bv	bool	enable support for int2bv and bv2int operators	true
bv.eq_axioms	bool	enable redundant equality axioms for bit-vectors	true
bv.reflect	bool	create enode for every bit-vector term	true
bv.size_reduce	bool	pre-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 constant	false
bv.watch_diseq	bool	use watch lists instead of eager axioms for bit-vectors	false
candidate_models	bool	create candidate models even when quantifier or theory reasoning is incomplete	false
case_split	unsigned int	0 - 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 activity	1
clause_proof	bool	record a clausal proof	false
core.extend_nonlocal_patterns	bool	extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier's body	false
core.extend_patterns	bool	extend unsat core with literals that trigger (potential) quantifier instances	false
core.extend_patterns.max_distance	unsigned int	limits the distance of a pattern-extended unsat core	4294967295
core.minimize	bool	minimize unsat core produced by SMT context	false
core.validate	bool	[internal] validate unsat core produced by SMT context. This option is intended for debugging	false
cube_depth	unsigned int	cube depth.	1
dack	unsigned int	0 - 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 resolution	1
dack.eq	bool	enable dynamic ackermannization for transitivity of equalities	false
dack.factor	double	number of instance per conflict	0.1
dack.gc	unsigned int	Dynamic ackermannization garbage collection frequency (per conflict)	2000
dack.gc_inv_decay	double	Dynamic ackermannization garbage collection decay	0.8
dack.threshold	unsigned int	number of times the congruence rule must be used before Leibniz's axiom is expanded	10
delay_units	bool	if true then z3 will not restart when a unit clause is learned	false
delay_units_threshold	unsigned int	maximum number of learned unit clauses before restarting, ignored if delay_units is false	32
dt_lazy_splits	unsigned int	How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy	1
elim_unconstrained	bool	pre-processing: eliminate unconstrained subterms	true
ematching	bool	E-Matching based quantifier instantiation	true
induction	bool	enable generation of induction lemmas	false
lemma_gc_strategy	unsigned int	lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none	0
logic	symbol	logic used to setup the SMT solver
macro_finder	bool	try to find universally quantified formulas that can be viewed as macros	false
max_conflicts	unsigned int	maximum number of conflicts before giving up.	4294967295
mbqi	bool	model based quantifier instantiation (MBQI)	true
mbqi.force_template	unsigned int	some 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 template	10
mbqi.id	string	Only use model-based instantiation for quantifiers with id's beginning with string
mbqi.max_cexs	unsigned int	initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation	1
mbqi.max_cexs_incr	unsigned int	increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI	0
mbqi.max_iterations	unsigned int	maximum number of rounds of MBQI	1000
mbqi.trace	bool	generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied	false
pb.conflict_frequency	unsigned int	conflict frequency for Pseudo-Boolean theory	1000
pb.learn_complements	bool	learn complement literals for Pseudo-Boolean theory	true
phase_caching_off	unsigned int	number of conflicts while phase caching is off	100
phase_caching_on	unsigned int	number of conflicts while phase caching is on	400
phase_selection	unsigned int	phase 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 - theory	3
propagate_values	bool	pre-processing: propagate values	true
pull_nested_quantifiers	bool	pre-processing: pull nested quantifiers	false
q.lift_ite	unsigned int	0 - don not lift non-ground if-then-else, 1 - use conservative ite lifting, 2 - use full lifting of if-then-else under quantifiers	0
q.lite	bool	Use cheap quantifier elimination during pre-processing	false
qi.cost	string	expression specifying what is the cost of a given quantifier instantiation	(+ weight generation)
qi.eager_threshold	double	threshold for eager quantifier instantiation	10.0
qi.lazy_threshold	double	threshold for lazy quantifier instantiation	20.0
qi.max_instances	unsigned int	maximum number of quantifier instantiations	4294967295
qi.max_multi_patterns	unsigned int	specify the number of extra multi patterns	0
qi.profile	bool	profile quantifier instantiation	false
qi.profile_freq	unsigned int	how frequent results are reported by qi.profile	4294967295
qi.quick_checker	unsigned int	specify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances	0
quasi_macros	bool	try to find universally quantified formulas that are quasi-macros	false
random_seed	unsigned int	random seed for the smt solver	0
refine_inj_axioms	bool	pre-processing: refine injectivity axioms	true
relevancy	unsigned int	relevancy 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 relevant	2
restart.max	unsigned int	maximal number of restarts.	4294967295
restart_factor	double	when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the current restart threshold	1.1
restart_strategy	unsigned int	0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic	1
restricted_quasi_macros	bool	try to find universally quantified formulas that are restricted quasi-macros	false
seq.max_unfolding	unsigned int	maximal unfolding depth for checking string equations and regular expressions	1000000000
seq.min_unfolding	unsigned int	initial bound for strings whose lengths are bounded by iterative deepening. Set this to a higher value if there are only models with larger string lengths	1
seq.split_w_len	bool	enable splitting guided by length constraints	true
seq.validate	bool	enable self-validation of theory axioms created by seq theory	false
solve_eqs	bool	pre-processing: solve equalities	true
str.aggressive_length_testing	bool	prioritize testing concrete length values over generating more options	false
str.aggressive_unroll_testing	bool	prioritize testing concrete regex unroll counts over generating more options	true
str.aggressive_value_testing	bool	prioritize testing concrete string constant values over generating more options	false
str.fast_length_tester_cache	bool	cache length tester constants instead of regenerating them	false
str.fast_value_tester_cache	bool	cache value tester constants instead of regenerating them	true
str.fixed_length_naive_cex	bool	construct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only)	true
str.fixed_length_refinement	bool	use abstraction refinement in fixed-length equation solver (Z3str3 only)	false
str.overlap_priority	double	theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true	-0.1
str.regex_automata_difficulty_threshold	unsigned int	difficulty threshold for regex automata heuristics	1000
str.regex_automata_failed_automaton_threshold	unsigned int	number of failed automaton construction attempts after which a full automaton is automatically built	10
str.regex_automata_failed_intersection_threshold	unsigned int	number of failed automaton intersection attempts after which intersection is always computed	10
str.regex_automata_intersection_difficulty_threshold	unsigned int	difficulty threshold for regex intersection heuristics	1000
str.regex_automata_length_attempt_threshold	unsigned int	number of length/path constraint attempts before checking unsatisfiability of regex terms	10
str.string_constant_cache	bool	cache all generated string constants generated from anywhere in theory_str	true
str.strong_arrangements	bool	assert equivalences instead of implications when generating string arrangement axioms	true
string_solver	symbol	solver 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_branching	bool	Allow the context to use extra information from theory solvers regarding literal branching prioritization.	false
theory_case_split	bool	Allow 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	unsigned int	maximal number of parallel threads.	1
threads.cube_frequency	unsigned int	frequency for using cubing	2
threads.max_conflicts	unsigned int	maximal number of conflicts between rounds of cubing for parallel SMT	400

sls

Experimental Stochastic Local Search Solver (for QFBV only).

Parameter	Type	Description	Default
early_prune	bool	use early pruning for score prediction	true
max_memory	unsigned int	maximum amount of memory in megabytes	4294967295
max_restarts	unsigned int	maximum number of restarts	4294967295
paws_init	unsigned int	initial/minimum assertion weights	40
paws_sp	unsigned int	smooth assertion weights with probability paws_sp / 1024	52
random_offset	bool	use random offset for candidate evaluation	true
random_seed	unsigned int	random seed	0
rescore	bool	rescore/normalize top-level score every base restart interval	true
restart_base	unsigned int	base restart interval given by moves per run	100
restart_init	bool	initialize to 0 or random value (= 1) after restart	false
scale_unsat	double	scale score of unsat expressions by this factor	0.5
track_unsat	bool	keep a list of unsat assertions as done in SAT - currently disabled internally	false
vns_mc	unsigned int	in local minima, try Monte Carlo sampling vns_mc many 2-bit-flips per bit	0
vns_repick	bool	in local minima, try picking a different assertion (only for walksat)	false
walksat	bool	use walksat assertion selection (instead of gsat)	true
walksat_repick	bool	repick assertion if randomizing in local minima	true
walksat_ucb	bool	use bandit heuristic for walksat assertion selection (instead of random)	true
walksat_ucb_constant	double	the ucb constant c in the term score + c * f(touched)	20.0
walksat_ucb_forget	double	scale touched by this factor every base restart interval	1.0
walksat_ucb_init	bool	initialize total ucb touched to formula size	false
walksat_ucb_noise	double	add noise 0 <= 256 * ucb_noise to ucb score for assertion selection	0.0002
wp	unsigned int	random walk with probability wp / 1024	100