z3.params

auto_config = true (bool)
debug_ref_count = false (bool)
dump_models = false (bool)
memory_high_watermark = 0 (unsigned int)
memory_max_alloc_count = 0 (unsigned int)
memory_max_size = 0 (unsigned int)
model = true (bool)
model_validate = false (bool)
proof = false (bool)
rlimit = 4294967295 (unsigned int)
smtlib2_compliant = false (bool)
timeout = 3000 (unsigned int)
trace = false (bool)
trace_file_name = z3.log (string)
type_check = true (bool)
unsat_core = true (bool)
verbose = 0 (unsigned int)
warning = true (bool)
well_sorted_check = true (bool)
pi.arith = 1 (unsigned int)
pi.arith_weight = 5 (unsigned int)
pi.block_loop_patterns = true (bool)
pi.max_multi_patterns = 0 (unsigned int)
pi.non_nested_arith_weight = 10 (unsigned int)
pi.pull_quantifiers = true (bool)
pi.use_database = false (bool)
pi.warnings = false (bool)
pp.bounded = false (bool)
pp.bv_literals = true (bool)
pp.bv_neg = false (bool)
pp.decimal = false (bool)
pp.decimal_precision = 10 (unsigned int)
pp.fixed_indent = false (bool)
pp.flat_assoc = true (bool)
pp.fp_real_literals = false (bool)
pp.max_depth = 5 (unsigned int)
pp.max_indent = 4294967295 (unsigned int)
pp.max_num_lines = 4294967295 (unsigned int)
pp.max_ribbon = 80 (unsigned int)
pp.max_width = 80 (unsigned int)
pp.min_alias_size = 10 (unsigned int)
pp.pretty_proof = false (bool)
pp.simplify_implies = true (bool)
pp.single_line = false (bool)
fixedpoint.datalog.all_or_nothing_deltas = false (bool)
fixedpoint.datalog.check_relation = null (symbol)
fixedpoint.datalog.compile_with_widening = false (bool)
fixedpoint.datalog.dbg_fpr_nonempty_relation_signature = false (bool)
fixedpoint.datalog.default_relation = pentagon (symbol)
fixedpoint.datalog.default_table = sparse (symbol)
fixedpoint.datalog.default_table_checked = false (bool)
fixedpoint.datalog.default_table_checker = null (symbol)
fixedpoint.datalog.explanations_on_relation_level = false (bool)
fixedpoint.datalog.generate_explanations = false (bool)
fixedpoint.datalog.initial_restart_timeout = 0 (unsigned int)
fixedpoint.datalog.magic_sets_for_queries = false (bool)
fixedpoint.datalog.output_profile = false (bool)
fixedpoint.datalog.print.tuples = true (bool)
fixedpoint.datalog.profile_timeout_milliseconds = 0 (unsigned int)
fixedpoint.datalog.similarity_compressor = true (bool)
fixedpoint.datalog.similarity_compressor_threshold = 11 (unsigned int)
fixedpoint.datalog.unbound_compressor = true (bool)
fixedpoint.datalog.use_map_names = true (bool)
fixedpoint.duality.batch_expand = false (bool)
fixedpoint.duality.conjecture_file =  (string)
fixedpoint.duality.enable_restarts = false (bool)
fixedpoint.duality.feasible_edges = true (bool)
fixedpoint.duality.full_expand = false (bool)
fixedpoint.duality.mbqi = true (bool)
fixedpoint.duality.no_conj = false (bool)
fixedpoint.duality.profile = false (bool)
fixedpoint.duality.recursion_bound = 4294967295 (unsigned int)
fixedpoint.duality.stratified_inlining = false (bool)
fixedpoint.duality.use_underapprox = false (bool)
fixedpoint.engine = auto-config (symbol)
fixedpoint.generate_proof_trace = false (bool)
fixedpoint.pdr.bfs_model_search = true (bool)
fixedpoint.pdr.cache_mode = 0 (unsigned int)
fixedpoint.pdr.farkas = true (bool)
fixedpoint.pdr.flexible_trace = false (bool)
fixedpoint.pdr.inductive_reachability_check = false (bool)
fixedpoint.pdr.max_num_contexts = 500 (unsigned int)
fixedpoint.pdr.simplify_formulas_post = false (bool)
fixedpoint.pdr.simplify_formulas_pre = false (bool)
fixedpoint.pdr.try_minimize_core = false (bool)
fixedpoint.pdr.use_arith_inductive_generalizer = false (bool)
fixedpoint.pdr.use_convex_closure_generalizer = false (bool)
fixedpoint.pdr.use_convex_interior_generalizer = false (bool)
fixedpoint.pdr.use_inductive_generalizer = true (bool)
fixedpoint.pdr.use_model_generalizer = false (bool)
fixedpoint.pdr.use_multicore_generalizer = false (bool)
fixedpoint.pdr.utvpi = true (bool)
fixedpoint.pdr.validate_result = false (bool)
fixedpoint.print_aig =  (symbol)
fixedpoint.print_answer = false (bool)
fixedpoint.print_boogie_certificate = false (bool)
fixedpoint.print_certificate = false (bool)
fixedpoint.print_fixedpoint_extensions = true (bool)
fixedpoint.print_low_level_smt2 = false (bool)
fixedpoint.print_statistics = false (bool)
fixedpoint.print_with_variable_declarations = true (bool)
fixedpoint.tab.selection = weight (symbol)
fixedpoint.timeout = 4294967295 (unsigned int)
fixedpoint.xform.bit_blast = false (bool)
fixedpoint.xform.coalesce_rules = false (bool)
fixedpoint.xform.coi = true (bool)
fixedpoint.xform.compress_unbound = true (bool)
fixedpoint.xform.fix_unbound_vars = false (bool)
fixedpoint.xform.inline_eager = true (bool)
fixedpoint.xform.inline_linear = true (bool)
fixedpoint.xform.inline_linear_branch = false (bool)
fixedpoint.xform.instantiate_quantifiers = false (bool)
fixedpoint.xform.karr = false (bool)
fixedpoint.xform.magic = false (bool)
fixedpoint.xform.quantify_arrays = false (bool)
fixedpoint.xform.scale = false (bool)
fixedpoint.xform.slice = true (bool)
fixedpoint.xform.unfold_rules = 0 (unsigned int)
model.compact = false (bool)
model.partial = false (bool)
model.v1 = false (bool)
model.v2 = false (bool)
# old_simplify.arith.expand_eqs = false (bool)
# old_simplify.arith.process_all_eqs = false (bool)
# old_simplify.array.canonize = false (bool)
# old_simplify.array.simplify = true (bool)
# old_simplify.bv.bv2int_distribute = true (bool)
sat.asymm_branch = true (bool)
sat.asymm_branch.limit = 100000000 (unsigned int)
sat.asymm_branch.rounds = 32 (unsigned int)
# sat.bcd = false (bool)
sat.blocked_clause_limit = 100000000 (unsigned int)
sat.burst_search = 100 (unsigned int)
sat.core.minimize = false (bool)
sat.core.minimize_partial = false (bool)
sat.dimacs.core = false (bool)
sat.dyn_sub_res = true (bool)
sat.elim_blocked_clauses = false (bool)
sat.elim_blocked_clauses_at = 2 (unsigned int)
sat.elim_vars = true (bool)
sat.gc = glue_psm (symbol)
sat.gc.increment = 500 (unsigned int)
sat.gc.initial = 20000 (unsigned int)
sat.gc.k = 7 (unsigned int)
sat.gc.small_lbd = 3 (unsigned int)
sat.max_conflicts = 4294967295 (unsigned int)
sat.max_memory = 4294967295 (unsigned int)
sat.minimize_lemmas = true (bool)
# sat.optimize_model = false (bool)
sat.phase = caching (symbol)
sat.phase.caching.off = 100 (unsigned int)
sat.phase.caching.on = 400 (unsigned int)
sat.random_freq = 0.01 (double)
sat.random_seed = 0 (unsigned int)
sat.resolution = true (bool)
sat.resolution.cls_cutoff1 = 100000000 (unsigned int)
sat.resolution.cls_cutoff2 = 700000000 (unsigned int)
sat.resolution.limit = 500000000 (unsigned int)
sat.resolution.lit_cutoff_range1 = 700 (unsigned int)
sat.resolution.lit_cutoff_range2 = 400 (unsigned int)
sat.resolution.lit_cutoff_range3 = 300 (unsigned int)
sat.resolution.occ_cutoff = 10 (unsigned int)
sat.resolution.occ_cutoff_range1 = 8 (unsigned int)
sat.resolution.occ_cutoff_range2 = 5 (unsigned int)
sat.resolution.occ_cutoff_range3 = 3 (unsigned int)
sat.restart = luby (symbol)
sat.restart.factor = 1.5 (double)
sat.restart.initial = 100 (unsigned int)
sat.scc = true (bool)
sat.subsumption = true (bool)
sat.subsumption.limit = 100000000 (unsigned int)
opt.dump_benchmarks = false (bool)
opt.elim_01 = true (bool)
opt.enable_sat = true (bool)
opt.enable_sls = false (bool)
opt.maxres.add_upper_bound_block = false (bool)
opt.maxres.hill_climb = true (bool)
opt.maxres.max_core_size = 3 (unsigned int)
opt.maxres.max_correction_set_size = 3 (unsigned int)
opt.maxres.max_num_cores = 4294967295 (unsigned int)
opt.maxres.maximize_assignment = false (bool)
opt.maxres.pivot_on_correction_set = true (bool)
opt.maxres.wmax = false (bool)
opt.maxsat_engine = maxres (symbol)
opt.optsmt_engine = basic (symbol)
opt.pb.compile_equality = false (bool)
opt.pp.neat = true (bool)
# opt.print_model = false (bool)
opt.priority = lex (symbol)
nnf.ignore_labels = false (bool)
nnf.max_memory = 4294967295 (unsigned int)
nnf.mode = skolem (symbol)
nnf.sk_hack = false (bool)
nnf.skolemize = true (bool)
algebraic.factor = true (bool)
algebraic.factor_max_prime = 31 (unsigned int)
algebraic.factor_num_primes = 1 (unsigned int)
algebraic.factor_search_size = 5000 (unsigned int)
algebraic.min_mag = 16 (unsigned int)
algebraic.zero_accuracy = 0 (unsigned int)
combined_solver.ignore_solver1 = false (bool)
combined_solver.solver2_timeout = 4294967295 (unsigned int)
combined_solver.solver2_unknown = 1 (unsigned int)
rcf.clean_denominators = true (bool)
rcf.inf_precision = 24 (unsigned int)
rcf.initial_precision = 24 (unsigned int)
rcf.lazy_algebraic_normalization = true (bool)
rcf.max_precision = 128 (unsigned int)
rcf.use_prem = true (bool)
model_evaluator.cache = true (bool)
model_evaluator.completion = false (bool)
model_evaluator.max_memory = 4294967295 (unsigned int)
model_evaluator.max_steps = 4294967295 (unsigned int)
ackermannization.eager = true (bool)
ackermannization.inc_sat_backend = false (bool)
ackermannization.sat_backend = false (bool)
nlsat.factor = true (bool)
nlsat.lazy = 0 (unsigned int)
nlsat.max_conflicts = 4294967295 (unsigned int)
nlsat.max_memory = 4294967295 (unsigned int)
nlsat.minimize_conflicts = false (bool)
nlsat.randomize = true (bool)
nlsat.reorder = true (bool)
nlsat.seed = 0 (unsigned int)
nlsat.shuffle_vars = false (bool)
nlsat.simplify_conflicts = true (bool)
parser.error_for_visual_studio = false (bool)
parser.ignore_bad_patterns = true (bool)
parser.ignore_user_patterns = false (bool)
rewriter.algebraic_number_evaluator = true (bool)
rewriter.arith_lhs = false (bool)
rewriter.bit2bool = true (bool)
rewriter.blast_distinct = false (bool)
rewriter.blast_distinct_threshold = 4294967295 (unsigned int)
rewriter.blast_eq_value = false (bool)
rewriter.bv_extract_prop = false (bool)
rewriter.bv_ineq_consistency_test_max = 0 (unsigned int)
rewriter.bv_ite2id = false (bool)
rewriter.bv_le_extra = false (bool)
rewriter.bv_not_simpl = false (bool)
rewriter.bv_sort_ac = false (bool)
rewriter.bv_trailing = false (bool)
rewriter.bv_urem_simpl = false (bool)
rewriter.bvnot2arith = false (bool)
rewriter.cache_all = false (bool)
rewriter.div0_ackermann_limit = 1000 (unsigned int)
rewriter.elim_and = true (bool)
rewriter.elim_rem = false (bool)
rewriter.elim_sign_ext = true (bool)
rewriter.elim_to_real = false (bool)
rewriter.eq2ineq = false (bool)
rewriter.expand_power = false (bool)
rewriter.expand_select_store = false (bool)
rewriter.expand_store_eq = false (bool)
rewriter.expand_tan = false (bool)
rewriter.flat = false (bool)
rewriter.gcd_rounding = false (bool)
rewriter.hi_div0 = true (bool)
rewriter.hi_fp_unspecified = true (bool)
rewriter.hoist_cmul = false (bool)
rewriter.hoist_mul = false (bool)
rewriter.ite_extra_rules = false (bool)
rewriter.local_ctx = false (bool)
rewriter.local_ctx_limit = 4294967295 (unsigned int)
rewriter.max_degree = 64 (unsigned int)
rewriter.max_memory = 4294967295 (unsigned int)
rewriter.max_steps = 4294967295 (unsigned int)
rewriter.mul2concat = false (bool)
rewriter.mul_to_power = false (bool)
rewriter.pull_cheap_ite = false (bool)
rewriter.push_ite_arith = false (bool)
rewriter.push_ite_bv = false (bool)
rewriter.push_to_real = true (bool)
rewriter.som = false (bool)
rewriter.som_blowup = 4294967295 (unsigned int)
rewriter.sort_store = false (bool)
rewriter.sort_sums = false (bool)
rewriter.split_concat_eq = false (bool)
rewriter.udiv2mul = false (bool)
interp.check = false (bool)
interp.profile = false (bool)
smt.arith.branch_cut_ratio = 2 (unsigned int)
smt.arith.dump_lemmas = false (bool)
smt.arith.euclidean_solver = false (bool)
smt.arith.greatest_error_pivot = false (bool)
smt.arith.ignore_int = false (bool)
smt.arith.int_eq_branch = false (bool)
smt.arith.nl = true (bool)
smt.arith.nl.branching = true (bool)
smt.arith.nl.gb = true (bool)
smt.arith.nl.rounds = 1024 (unsigned int)
smt.arith.propagate_eqs = true (bool)
smt.arith.propagation_mode = 2 (unsigned int)
smt.arith.random_initial_value = false (bool)
smt.arith.solver = 2 (unsigned int)
smt.array.extensional = true (bool)
smt.array.weak = false (bool)
smt.auto_config = true (bool)
smt.bv.enable_int2bv = false (bool)
smt.bv.reflect = true (bool)
smt.case_split = 1 (unsigned int)
smt.core.minimize = false (bool)
smt.core.validate = false (bool)
smt.dack = 1 (unsigned int)
smt.dack.eq = false (bool)
smt.dack.factor = 0.1 (double)
smt.dack.gc = 2000 (unsigned int)
smt.dack.gc_inv_decay = 0.8 (double)
smt.dack.threshold = 10 (unsigned int)
smt.delay_units = false (bool)
smt.delay_units_threshold = 32 (unsigned int)
smt.ematching = true (bool)
smt.macro_finder = false (bool)
smt.max_conflicts = 4294967295 (unsigned int)
smt.mbqi = true (bool)
smt.mbqi.force_template = 10 (unsigned int)
smt.mbqi.id =  (string)
smt.mbqi.max_cexs = 1 (unsigned int)
smt.mbqi.max_cexs_incr = 0 (unsigned int)
smt.mbqi.max_iterations = 1000 (unsigned int)
smt.mbqi.trace = false (bool)
smt.pb.conflict_frequency = 1000 (unsigned int)
smt.pb.enable_compilation = true (bool)
smt.pb.enable_simplex = false (bool)
smt.pb.learn_complements = true (bool)
smt.phase_selection = 3 (unsigned int)
smt.pull_nested_quantifiers = false (bool)
smt.qi.cost = (+ weight generation) (string)
smt.qi.eager_threshold = 10.0 (double)
smt.qi.lazy_threshold = 20.0 (double)
smt.qi.max_instances = 4294967295 (unsigned int)
smt.qi.max_multi_patterns = 0 (unsigned int)
smt.qi.profile = false (bool)
smt.qi.profile_freq = 4294967295 (unsigned int)
smt.random_seed = 0 (unsigned int)
smt.refine_inj_axioms = true (bool)
smt.relevancy = 2 (unsigned int)
smt.restart_factor = 1.1 (double)
smt.restart_strategy = 1 (unsigned int)
smt.rlimit = 0 (unsigned int)
smt.timeout = 0 (unsigned int)
sls.early_prune = true (bool)
sls.max_memory = 4294967295 (unsigned int)
sls.max_restarts = 4294967295 (unsigned int)
sls.paws_init = 40 (unsigned int)
sls.paws_sp = 52 (unsigned int)
sls.random_offset = true (bool)
sls.random_seed = 0 (unsigned int)
sls.rescore = true (bool)
sls.restart_base = 100 (unsigned int)
sls.restart_init = false (bool)
sls.scale_unsat = 0.5 (double)
sls.track_unsat = false (bool)
sls.vns_mc = 0 (unsigned int)
sls.vns_repick = false (bool)
sls.walksat = true (bool)
sls.walksat_repick = true (bool)
sls.walksat_ucb = true (bool)
sls.walksat_ucb_constant = 20.0 (double)
sls.walksat_ucb_forget = 1.0 (double)
sls.walksat_ucb_init = false (bool)
sls.walksat_ucb_noise = 0.0002 (double)
sls.wp = 100 (unsigned int)