Z3 Options Enabled
## Module pi



Description: 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


## Module tactic



Description: 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


## Module pp



Description: 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


## Module sat



Description: 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 cluases 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 hessitant 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.file | symbol  |  file to dump DRAT proofs | 

drup.trim | bool  |  build and trim drup proof | false

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

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


## Module solver



Description: 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 | 

lemmas2console | bool  |  print lemmas during search | false

smtlib2_log | symbol  |  file to save solver interaction | 

timeout | unsigned int  |  timeout on the solver object; overwrites a global timeout | 4294967295


## Module opt



Description: 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  |  restict 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 inequalites) | 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 priortize 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


## Module parallel



Description: 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 simplifcation 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


## Module nnf



Description: 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


## Module algebraic



Description: 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 lifiting 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


## Module combined_solver



Description: 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


## Module rcf



Description: 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


## Module ackermannization



Description: 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


## Module nlsat



Description: 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



## Module fp



Description: 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.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.print_json | symbol  |  Print pobs tree in JSON format to a given file | 

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


## Module smt



Description: 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 | true

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

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

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

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


## Module sls



Description: 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


