z3-options.txt

 enforce_model_conversion                             apply model transformation on new assertions                                                                                                                                                                                                                                                                                                                                                            
 smtlib2_log                                          file to save solver interaction                                                                                                                                                                                                                                                                                                                                                                         
 cancel_backup_file                                   file to save partial search state if search is canceled                                                                                                                                                                                                                                                                                                                                                 
 timeout                                              timeout on the solver object; overwrites a global timeout                                                                                                                                                                                                                                                                                                                                               
 partial                                              enable/disable partial function interpretations                                                                                                                                                                                                                                                                                                                                                         
 v1                                                   use Z3 version 1.x pretty printer                                                                                                                                                                                                                                                                                                                                                                       
 v2                                                   use Z3 version 2.x (x <= 16) pretty printer                                                                                                                                                                                                                                                                                                                                                             
 compact                                              try to compact function graph (i.e., function interpretations that are lookup tables)                                                                                                                                                                                                                                                                                                                   
 inline_def                                           inline local function definitions ignoring possible expansion                                                                                                                                                                                                                                                                                                                                           
 completion                                           enable/disable model completion                                                                                                                                                                                                                                                                                                                                                                         
 rlimit                                               default resource limit used for solvers. Unrestricted when set to 0.                                                                                                                                                                                                                                                                                                                                    
 max_memory                                           (default: infty) maximum amount of memory in megabytes.                                                                                                                                                                                                                                                                                                                                                 
 ctrl_c                                               enable interrupts from ctrl-c                                                                                                                                                                                                                                                                                                                                                                           
 ite_extra_rules                                      extra ite simplifications, these additional simplifications may reduce size locally but increase globally                                                                                                                                                                                                                                                                                               
 flat                                                 create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor                                                                                                                                                                                                                                                                                                                                    
 elim_and                                             conjunctions are rewritten using negation and disjunctions                                                                                                                                                                                                                                                                                                                                              
 elim_ite                                             eliminate ite in favor of and/or                                                                                                                                                                                                                                                                                                                                                                        
 local_ctx                                            perform local (i.e., cheap) context simplifications                                                                                                                                                                                                                                                                                                                                                     
 local_ctx_limit                                      limit for applying local context simplifier                                                                                                                                                                                                                                                                                                                                                             
 blast_distinct                                       expand a distinct predicate into a quadratic number of disequalities                                                                                                                                                                                                                                                                                                                                    
 blast_distinct_threshold                             when blast_distinct is true, only distinct expressions with less than this number of arguments are blasted                                                                                                                                                                                                                                                                                              
 som                                                  put polynomials in sum-of-monomials form                                                                                                                                                                                                                                                                                                                                                                
 som_blowup                                           maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form                                                                                                                                                                                                                                                                                                       
 hoist_mul                                            hoist multiplication over summation to minimize number of multiplications                                                                                                                                                                                                                                                                                                                               
 hoist_ite                                            hoist shared summands under ite expressions                                                                                                                                                                                                                                                                                                                                                             
 algebraic_number_evaluator                           simplify/evaluate expressions containing (algebraic) irrational numbers.                                                                                                                                                                                                                                                                                                                                
 mul_to_power                                         collpase (* t ... t) into (^ t k), it is ignored if expand_power is true.                                                                                                                                                                                                                                                                                                                               
 expand_power                                         expand (^ t k) into (* t ... t) if  1 < k <= max_degree.                                                                                                                                                                                                                                                                                                                                                
 expand_tan                                           replace (tan x) with (/ (sin x) (cos x)).                                                                                                                                                                                                                                                                                                                                                               
 max_degree                                           max degree of algebraic numbers (and power operators) processed by simplifier.                                                                                                                                                                                                                                                                                                                          
 sort_sums                                            sort the arguments of + application.                                                                                                                                                                                                                                                                                                                                                                    
 gcd_rounding                                         use gcd rounding on integer arithmetic atoms.                                                                                                                                                                                                                                                                                                                                                           
 arith_lhs                                            all monomials are moved to the left-hand-side, and the right-hand-side is just a constant.                                                                                                                                                                                                                                                                                                              
 arith_ineq_lhs                                       rewrite inequalities so that right-hand-side is a constant.                                                                                                                                                                                                                                                                                                                                             
 elim_to_real                                         eliminate to_real from arithmetic predicates that contain only integers.                                                                                                                                                                                                                                                                                                                                
 push_to_real                                         distribute to_real over * and +.                                                                                                                                                                                                                                                                                                                                                                        
 eq2ineq                                              expand equalities into two inequalities                                                                                                                                                                                                                                                                                                                                                                 
 elim_rem                                             replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).                                                                                                                                                                                                                                                                                                                                          
 split_concat_eq                                      split equalities of the form (= (concat t1 t2) t3)                                                                                                                                                                                                                                                                                                                                                      
 bit2bool                                             try to convert bit-vector terms of size 1 into Boolean terms                                                                                                                                                                                                                                                                                                                                            
 blast_eq_value                                       blast (some) Bit-vector equalities into bits                                                                                                                                                                                                                                                                                                                                                            
 elim_sign_ext                                        expand sign-ext operator using concat and extract                                                                                                                                                                                                                                                                                                                                                       
 hi_div0                                              use the 'hardware interpretation' for division by zero (for bit-vector terms)                                                                                                                                                                                                                                                                                                                           
 mul2concat                                           replace multiplication by a power of two into a concatenation                                                                                                                                                                                                                                                                                                                                           
 bv_sort_ac                                           sort the arguments of all AC operators                                                                                                                                                                                                                                                                                                                                                                  
 bv_extract_prop                                      attempt to partially propagate extraction inwards                                                                                                                                                                                                                                                                                                                                                       
 bv_not_simpl                                         apply simplifications for bvnot                                                                                                                                                                                                                                                                                                                                                                         
 bv_ite2id                                            rewrite ite that can be simplified to identity                                                                                                                                                                                                                                                                                                                                                          
 bv_le_extra                                          additional bu_(u/s)le simplifications                                                                                                                                                                                                                                                                                                                                                                   
 mkbv2num                                             (default: false) convert (mkbv [true/false]*) into a numeral                                                                                                                                                                                                                                                                                                                                            
 expand_select_store                                  conservatively replace a (select (store ...) ...) term by an if-then-else term                                                                                                                                                                                                                                                                                                                          
 blast_select_store                                   eagerly replace all (select (store ..) ..) term by an if-then-else term                                                                                                                                                                                                                                                                                                                                 
 expand_nested_stores                                 replace nested stores by a lambda expression                                                                                                                                                                                                                                                                                                                                                            
 expand_store_eq                                      reduce (store ...) = (store ...) with a common base into selects                                                                                                                                                                                                                                                                                                                                        
 sort_store                                           sort nested stores when the indices are known to be different                                                                                                                                                                                                                                                                                                                                           
 max_steps                                            maximum number of steps                                                                                                                                                                                                                                                                                                                                                                                 
 push_ite_arith                                       push if-then-else over arithmetic terms.                                                                                                                                                                                                                                                                                                                                                                
 push_ite_bv                                          push if-then-else over bit-vector terms.                                                                                                                                                                                                                                                                                                                                                                
 pull_cheap_ite                                       pull if-then-else terms when cheap.                                                                                                                                                                                                                                                                                                                                                                     
 bv_ineq_consistency_test_max                         max size of conjunctions on which to perform consistency test based on inequalities on bitvectors.                                                                                                                                                                                                                                                                                                      
 cache_all                                            cache all intermediate results.                                                                                                                                                                                                                                                                                                                                                                         
 rewrite_patterns                                     rewrite patterns.                                                                                                                                                                                                                                                                                                                                                                                       
 ignore_patterns_on_ground_qbody                      ignores patterns on quantifiers that don't mention their bound variables.                                                                                                                                                                                                                                                                                                                               
 ite_extra                                            (default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas                                                                                                                                                                                                                                                                                               
 phase                                                phase selection strategy: always_false, always_true, basic_caching, random, caching                                                                                                                                                                                                                                                                                                                     
 phase.sticky                                         use sticky phase caching                                                                                                                                                                                                                                                                                                                                                                                
 search.unsat.conflicts                               period for solving for unsat (in number of conflicts)                                                                                                                                                                                                                                                                                                                                                   
 search.sat.conflicts                                 period for solving for sat (in number of conflicts)                                                                                                                                                                                                                                                                                                                                                     
 rephase.base                                         number of conflicts per rephase                                                                                                                                                                                                                                                                                                                                                                         
 reorder.base                                         number of conflicts per random reorder                                                                                                                                                                                                                                                                                                                                                                  
 reorder.itau                                         inverse temperature for softmax                                                                                                                                                                                                                                                                                                                                                                         
 reorder.activity_scale                               scaling factor for activity update                                                                                                                                                                                                                                                                                                                                                                      
 propagate.prefetch                                   prefetch watch lists for assigned literals                                                                                                                                                                                                                                                                                                                                                              
 restart                                              restart strategy: static, luby, ema or geometric                                                                                                                                                                                                                                                                                                                                                        
 restart.initial                                      initial restart (number of conflicts)                                                                                                                                                                                                                                                                                                                                                                   
 restart.max                                          maximal number of restarts.                                                                                                                                                                                                                                                                                                                                                                             
 restart.fast                                         use fast restart approach only removing less active literals.                                                                                                                                                                                                                                                                                                                                           
 restart.factor                                       restart increment factor for geometric strategy                                                                                                                                                                                                                                                                                                                                                         
 restart.margin                                       margin between fast and slow restart factors. For ema                                                                                                                                                                                                                                                                                                                                                   
 restart.emafastglue                                  ema alpha factor for fast moving average                                                                                                                                                                                                                                                                                                                                                                
 restart.emaslowglue                                  ema alpha factor for slow moving average                                                                                                                                                                                                                                                                                                                                                                
 variable_decay                                       multiplier (divided by 100) for the VSIDS activity increment                                                                                                                                                                                                                                                                                                                                            
 inprocess.max                                        maximal number of inprocessing passes                                                                                                                                                                                                                                                                                                                                                                   
 inprocess.out                                        file to dump result of the first inprocessing step and exit                                                                                                                                                                                                                                                                                                                                             
 branching.heuristic                                  branching heuristic vsids, chb                                                                                                                                                                                                                                                                                                                                                                          
 branching.anti_exploration                           apply anti-exploration heuristic for branch selection                                                                                                                                                                                                                                                                                                                                                   
 random_freq                                          frequency of random case splits                                                                                                                                                                                                                                                                                                                                                                         
 random_seed                                          random seed                                                                                                                                                                                                                                                                                                                                                                                             
 burst_search                                         number of conflicts before first global simplification                                                                                                                                                                                                                                                                                                                                                  
 enable_pre_simplify                                  enable pre simplifications before the bounded search                                                                                                                                                                                                                                                                                                                                                    
 max_conflicts                                        maximum number of conflicts                                                                                                                                                                                                                                                                                                                                                                             
 gc                                                   garbage collection strategy: psm, glue, glue_psm, dyn_psm                                                                                                                                                                                                                                                                                                                                               
 gc.initial                                           learned clauses garbage collection frequency                                                                                                                                                                                                                                                                                                                                                            
 gc.increment                                         increment to the garbage collection threshold                                                                                                                                                                                                                                                                                                                                                           
 gc.small_lbd                                         learned clauses with small LBD are never deleted (only used in dyn_psm)                                                                                                                                                                                                                                                                                                                                 
 gc.k                                                 learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)                                                                                                                                                                                                                                                                                                        
 gc.burst                                             perform eager garbage collection during initialization                                                                                                                                                                                                                                                                                                                                                  
 gc.defrag                                            defragment clauses when garbage collecting                                                                                                                                                                                                                                                                                                                                                              
 simplify.delay                                       set initial delay of simplification by a conflict count                                                                                                                                                                                                                                                                                                                                                 
 force_cleanup                                        force cleanup to remove tautologies and simplify clauses                                                                                                                                                                                                                                                                                                                                                
 minimize_lemmas                                      minimize learned clauses                                                                                                                                                                                                                                                                                                                                                                                
 dyn_sub_res                                          dynamic subsumption resolution for minimizing learned clauses                                                                                                                                                                                                                                                                                                                                           
 core.minimize                                        minimize computed core                                                                                                                                                                                                                                                                                                                                                                                  
 core.minimize_partial                                apply partial (cheap) core minimization                                                                                                                                                                                                                                                                                                                                                                 
 backtrack.scopes                                     number of scopes to enable chronological backtracking                                                                                                                                                                                                                                                                                                                                                   
 backtrack.conflicts                                  number of conflicts before enabling chronological backtracking                                                                                                                                                                                                                                                                                                                                          
 threads                                              number of parallel threads to use                                                                                                                                                                                                                                                                                                                                                                       
 dimacs.core                                          extract core from DIMACS benchmarks                                                                                                                                                                                                                                                                                                                                                                     
 drat.file                                            file to dump DRAT proofs                                                                                                                                                                                                                                                                                                                                                                                
 drat.binary                                          use Binary DRAT output format                                                                                                                                                                                                                                                                                                                                                                           
 drat.check_unsat                                     build up internal proof and check                                                                                                                                                                                                                                                                                                                                                                       
 drat.check_sat                                       build up internal trace, check satisfying model                                                                                                                                                                                                                                                                                                                                                         
 drat.activity                                        dump variable activities                                                                                                                                                                                                                                                                                                                                                                                
 cardinality.solver                                   use cardinality solver                                                                                                                                                                                                                                                                                                                                                                                  
 pb.solver                                            method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), binary_merge, segmented, solver (use native solver)                                                                                                                                                                                                      
 pb.min_arity                                         minimal arity to compile pb/cardinality constraints to CNF                                                                                                                                                                                                                                                                                                                                              
 cardinality.encoding                                 encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit                                                                                                                                                                                                                                                                                                                     
 pb.resolve                                           resolution strategy for boolean algebra solver: cardinality, rounding                                                                                                                                                                                                                                                                                                                                   
 pb.lemma_format                                      generate either cardinality or pb lemmas                                                                                                                                                                                                                                                                                                                                                                
 euf                                                  enable euf solver (this feature is preliminary and not ready for general consumption)                                                                                                                                                                                                                                                                                                                   
 ddfw_search                                          use ddfw local search instead of CDCL                                                                                                                                                                                                                                                                                                                                                                   
 ddfw.init_clause_weight                              initial clause weight for DDFW local search                                                                                                                                                                                                                                                                                                                                                             
 ddfw.use_reward_pct                                  percentage to pick highest reward variable when it has reward 0                                                                                                                                                                                                                                                                                                                                         
 ddfw.restart_base                                    number of flips used a starting point for hessitant restart backoff                                                                                                                                                                                                                                                                                                                                     
 ddfw.reinit_base                                     increment basis for geometric backoff scheme of re-initialization of weights                                                                                                                                                                                                                                                                                                                            
 ddfw.threads                                         number of ddfw threads to run in parallel with sat solver                                                                                                                                                                                                                                                                                                                                               
 prob_search                                          use probsat local search instead of CDCL                                                                                                                                                                                                                                                                                                                                                                
 local_search                                         use local search instead of CDCL                                                                                                                                                                                                                                                                                                                                                                        
 local_search_threads                                 number of local search threads to find satisfiable solution                                                                                                                                                                                                                                                                                                                                             
 local_search_mode                                    local search algorithm, either default wsat or qsat                                                                                                                                                                                                                                                                                                                                                     
 local_search_dbg_flips                               write debug information for number of flips                                                                                                                                                                                                                                                                                                                                                             
 binspr                                               enable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates models                                                                                                                                                                                                                                                                                                 
 anf                                                  enable ANF based simplification in-processing                                                                                                                                                                                                                                                                                                                                                           
 anf.delay                                            delay ANF simplification by in-processing round                                                                                                                                                                                                                                                                                                                                                         
 anf.exlin                                            enable extended linear simplification                                                                                                                                                                                                                                                                                                                                                                   
 cut                                                  enable AIG based simplification in-processing                                                                                                                                                                                                                                                                                                                                                           
 cut.delay                                            delay cut simplification by in-processing round                                                                                                                                                                                                                                                                                                                                                         
 cut.aig                                              extract aigs (and ites) from cluases for cut simplification                                                                                                                                                                                                                                                                                                                                             
 cut.lut                                              extract luts from clauses for cut simplification                                                                                                                                                                                                                                                                                                                                                        
 cut.xor                                              extract xors from clauses for cut simplification                                                                                                                                                                                                                                                                                                                                                        
 cut.npn3                                             extract 3 input functions from clauses for cut simplification                                                                                                                                                                                                                                                                                                                                           
 cut.dont_cares                                       integrate dont cares with cuts                                                                                                                                                                                                                                                                                                                                                                          
 cut.redundancies                                     integrate redundancy checking of cuts                                                                                                                                                                                                                                                                                                                                                                   
 cut.force                                            force redoing cut-enumeration until a fixed-point                                                                                                                                                                                                                                                                                                                                                       
 lookahead.cube.cutoff                                cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat                                                                                                                                                                                                                                                                                                     
 lookahead.cube.fraction                              adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat                                                                                                                                                                                                                                                                                      
 lookahead.cube.depth                                 cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.                                                                                                                                                                                                                                                                                                                                
 lookahead.cube.freevars                              cube free variable fraction. Used when lookahead.cube.cutoff is freevars                                                                                                                                                                                                                                                                                                                                
 lookahead.cube.psat.var_exp                          free variable exponent for PSAT cutoff                                                                                                                                                                                                                                                                                                                                                                  
 lookahead.cube.psat.clause_base                      clause base for PSAT cutoff                                                                                                                                                                                                                                                                                                                                                                             
 lookahead.cube.psat.trigger                          trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat                                                                                                                                                                                                                                                                                                        
 lookahead.preselect                                  use pre-selection of subset of variables for branching                                                                                                                                                                                                                                                                                                                                                  
 lookahead_simplify                                   use lookahead solver during simplification                                                                                                                                                                                                                                                                                                                                                              
 lookahead_scores                                     extract lookahead scores. A utility that can only be used from the DIMACS front-end                                                                                                                                                                                                                                                                                                                     
 lookahead.double                                     enable doubld lookahead                                                                                                                                                                                                                                                                                                                                                                                 
 lookahead.use_learned                                use learned clauses when selecting lookahead literal                                                                                                                                                                                                                                                                                                                                                    
 lookahead_simplify.bca                               add learned binary clauses as part of lookahead simplification                                                                                                                                                                                                                                                                                                                                          
 lookahead.global_autarky                             prefer to branch on variables that occur in clauses that are reduced                                                                                                                                                                                                                                                                                                                                    
 lookahead.delta_fraction                             number between 0 and 1, the smaller the more literals are selected for double lookahead                                                                                                                                                                                                                                                                                                                 
 lookahead.reward                                     select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu                                                                                                                                                                                                                                                                                                  
 bce                                                  eliminate blocked clauses                                                                                                                                                                                                                                                                                                                                                                               
 abce                                                 eliminate blocked clauses using asymmetric literals                                                                                                                                                                                                                                                                                                                                                     
 cce                                                  eliminate covered clauses                                                                                                                                                                                                                                                                                                                                                                               
 ate                                                  asymmetric tautology elimination                                                                                                                                                                                                                                                                                                                                                                        
 acce                                                 eliminate covered clauses using asymmetric added literals                                                                                                                                                                                                                                                                                                                                               
 bce_at                                               eliminate blocked clauses only once at the given simplification round                                                                                                                                                                                                                                                                                                                                   
 bca                                                  blocked clause addition - add blocked binary clauses                                                                                                                                                                                                                                                                                                                                                    
 bce_delay                                            delay eliminate blocked clauses until simplification round                                                                                                                                                                                                                                                                                                                                              
 retain_blocked_clauses                               retain blocked clauses as lemmas                                                                                                                                                                                                                                                                                                                                                                        
 blocked_clause_limit                                 maximum number of literals visited during blocked clause elimination                                                                                                                                                                                                                                                                                                                                    
 override_incremental                                 override incremental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused                                                                                                                                                                                                                                                                                          
 resolution.limit                                     approx. maximum number of literals visited during variable elimination                                                                                                                                                                                                                                                                                                                                  
 resolution.occ_cutoff                                first cutoff (on number of positive/negative occurrences) for Boolean variable elimination                                                                                                                                                                                                                                                                                                              
 resolution.occ_cutoff_range1                         second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses                                                                                                                                                                                                                                                     
 resolution.occ_cutoff_range2                         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                                                                                                                                                                                                                               
 resolution.occ_cutoff_range3                         second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff2                                                                                                                                                                                                                                                             
 resolution.lit_cutoff_range1                         second cutoff (total number of literals) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses                                                                                                                                                                                                                                                                    
 resolution.lit_cutoff_range2                         second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2                                                                                                                                                                                                                                              
 resolution.lit_cutoff_range3                         second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff2                                                                                                                                                                                                                                                                            
 resolution.cls_cutoff1                               limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination                                                                                                                                                                                                                                                                                                         
 resolution.cls_cutoff2                               limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination                                                                                                                                                                                                                                                                                                         
 elim_vars                                            enable variable elimination using resolution during simplification                                                                                                                                                                                                                                                                                                                                      
 elim_vars_bdd                                        enable variable elimination using BDD recompilation during simplification                                                                                                                                                                                                                                                                                                                               
 elim_vars_bdd_delay                                  delay elimination of variables using BDDs until after simplification round                                                                                                                                                                                                                                                                                                                              
 probing                                              apply failed literal detection during simplification                                                                                                                                                                                                                                                                                                                                                    
 probing_limit                                        limit to the number of probe calls                                                                                                                                                                                                                                                                                                                                                                      
 probing_cache                                        add binary literals as lemmas                                                                                                                                                                                                                                                                                                                                                                           
 probing_cache_limit                                  cache binaries unless overall memory usage exceeds cache limit                                                                                                                                                                                                                                                                                                                                          
 probing_binary                                       probe binary clauses                                                                                                                                                                                                                                                                                                                                                                                    
 subsumption                                          eliminate subsumed clauses                                                                                                                                                                                                                                                                                                                                                                              
 subsumption.limit                                    approx. maximum number of literals visited during subsumption (and subsumption resolution)                                                                                                                                                                                                                                                                                                              
 asymm_branch                                         asymmetric branching                                                                                                                                                                                                                                                                                                                                                                                    
 asymm_branch.rounds                                  maximal number of rounds to run asymmetric branch simplifications if progress is made                                                                                                                                                                                                                                                                                                                   
 asymm_branch.delay                                   number of simplification rounds to wait until invoking asymmetric branch simplification                                                                                                                                                                                                                                                                                                                 
 asymm_branch.sampled                                 use sampling based asymmetric branching based on binary implication graph                                                                                                                                                                                                                                                                                                                               
 asymm_branch.limit                                   approx. maximum number of literals visited during asymmetric branching                                                                                                                                                                                                                                                                                                                                  
 asymm_branch.all                                     asymmetric branching on all literals per clause                                                                                                                                                                                                                                                                                                                                                         
 scc                                                  eliminate Boolean variables by computing strongly connected components                                                                                                                                                                                                                                                                                                                                  
 scc.tr                                               apply transitive reduction, eliminate redundant binary clauses                                                                                                                                                                                                                                                                                                                                          
 keep_cardinality_constraints                         (default: false) retain cardinality constraints (don't bit-blast them) and use built-in cardinality solver                                                                                                                                                                                                                                                                                              
 max_rounds                                           (default: 4) maximum number of rounds.                                                                                                                                                                                                                                                                                                                                                                  
 solve_eqs_max_occs                                   (default: infty) maximum number of occurrences for considering a variable for gaussian eliminations.                                                                                                                                                                                                                                                                                                    
 theory_solver                                        (default: true) use theory solvers.                                                                                                                                                                                                                                                                                                                                                                     
 ite_solver                                           (default: true) use if-then-else solver.                                                                                                                                                                                                                                                                                                                                                                
 context_solve                                        (default: false) solve equalities under disjunctions.                                                                                                                                                                                                                                                                                                                                                   
 max_args                                             (default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic.                                                                                                                                                                                                                                                                               
 div0_ackermann_limit                                 a bound for number of congruence Ackermann lemmas for div0 modelling                                                                                                                                                                                                                                                                                                                                    
 fail_if_inconclusive                                 (default: true) fail if found unsat (sat) for under (over) approximated goal.                                                                                                                                                                                                                                                                                                                           
 auto_config                                          automatically configure solver                                                                                                                                                                                                                                                                                                                                                                          
 logic                                                logic used to setup the SMT solver                                                                                                                                                                                                                                                                                                                                                                      
 relevancy                                            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                                                                                                                                                                                                              
 macro_finder                                         try to find universally quantified formulas that can be viewed as macros                                                                                                                                                                                                                                                                                                                                
 quasi_macros                                         try to find universally quantified formulas that are quasi-macros                                                                                                                                                                                                                                                                                                                                       
 restricted_quasi_macros                              try to find universally quantified formulas that are restricted quasi-macros                                                                                                                                                                                                                                                                                                                            
 ematching                                            E-Matching based quantifier instantiation                                                                                                                                                                                                                                                                                                                                                               
 phase_selection                                      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                                                                                                                                                                                                    
 phase_caching_on                                     number of conflicts while phase caching is on                                                                                                                                                                                                                                                                                                                                                           
 phase_caching_off                                    number of conflicts while phase caching is off                                                                                                                                                                                                                                                                                                                                                          
 restart_strategy                                     0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic                                                                                                                                                                                                                                                                                                                           
 restart_factor                                       when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the current restart threshold                                                                                                                                                                                                                                                       
 case_split                                           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                           
 delay_units                                          if true then z3 will not restart when a unit clause is learned                                                                                                                                                                                                                                                                                                                                          
 delay_units_threshold                                maximum number of learned unit clauses before restarting, ignored if delay_units is false                                                                                                                                                                                                                                                                                                               
 pull_nested_quantifiers                              pull nested quantifiers                                                                                                                                                                                                                                                                                                                                                                                 
 refine_inj_axioms                                    refine injectivity axioms                                                                                                                                                                                                                                                                                                                                                                               
 candidate_models                                     create candidate models even when quantifier or theory reasoning is incomplete                                                                                                                                                                                                                                                                                                                          
 cube_depth                                           cube depth.                                                                                                                                                                                                                                                                                                                                                                                             
 threads.max_conflicts                                maximal number of conflicts between rounds of cubing for parallel SMT                                                                                                                                                                                                                                                                                                                                   
 threads.cube_frequency                               frequency for using cubing                                                                                                                                                                                                                                                                                                                                                                              
 mbqi                                                 model based quantifier instantiation (MBQI)                                                                                                                                                                                                                                                                                                                                                             
 mbqi.max_cexs                                        initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation                                                                                                                                                                                                                                                                                        
 mbqi.max_cexs_incr                                   increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI                                                                                                                                                                                                                                                                                                                        
 mbqi.max_iterations                                  maximum number of rounds of MBQI                                                                                                                                                                                                                                                                                                                                                                        
 mbqi.trace                                           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                                                                                                                                                                                                                            
 mbqi.force_template                                  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                                                                                                                                           
 mbqi.id                                              Only use model-based instantiation for quantifiers with id's beginning with string                                                                                                                                                                                                                                                                                                                      
 q.lift_ite                                           0 - don not lift non-ground if-then-else, 1 - use conservative ite lifting, 2 - use full lifting of if-then-else under quantifiers                                                                                                                                                                                                                                                                      
 qi.profile                                           profile quantifier instantiation                                                                                                                                                                                                                                                                                                                                                                        
 qi.profile_freq                                      how frequent results are reported by qi.profile                                                                                                                                                                                                                                                                                                                                                         
 qi.max_instances                                     maximum number of quantifier instantiations                                                                                                                                                                                                                                                                                                                                                             
 qi.eager_threshold                                   threshold for eager quantifier instantiation                                                                                                                                                                                                                                                                                                                                                            
 qi.lazy_threshold                                    threshold for lazy quantifier instantiation                                                                                                                                                                                                                                                                                                                                                             
 qi.cost                                              expression specifying what is the cost of a given quantifier instantiation                                                                                                                                                                                                                                                                                                                              
 qi.max_multi_patterns                                specify the number of extra multi patterns                                                                                                                                                                                                                                                                                                                                                              
 qi.quick_checker                                     specify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances                                                                                                                                                                                                                                                                                  
 induction                                            enable generation of induction lemmas                                                                                                                                                                                                                                                                                                                                                                   
 bv.reflect                                           create enode for every bit-vector term                                                                                                                                                                                                                                                                                                                                                                  
 bv.enable_int2bv                                     enable support for int2bv and bv2int operators                                                                                                                                                                                                                                                                                                                                                          
 bv.eq_axioms                                         add dynamic equality axioms                                                                                                                                                                                                                                                                                                                                                                             
 bv.watch_diseq                                       use watch lists instead of eager axioms for bit-vectors                                                                                                                                                                                                                                                                                                                                                 
 bv.delay                                             delay internalize expensive bit-vector operations                                                                                                                                                                                                                                                                                                                                                       
 arith.random_initial_value                           use random initial values in the simplex-based procedure for linear arithmetic                                                                                                                                                                                                                                                                                                                          
 arith.solver                                         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                                                                                                                                                                
 arith.nl                                             (incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2                                                                                                                                                                                                                                                                         
 arith.nl.nra                                         call nra_solver when incremental lianirization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6                                                                                                                                                                                                                                                
 arith.nl.branching                                   branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2                                                                                                                                                                                                                                                                                                              
 arith.nl.rounds                                      threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2                                                                                                                                                                                                                                                                                            
 arith.nl.order                                       run order lemmas                                                                                                                                                                                                                                                                                                                                                                                        
 arith.nl.expp                                        expensive patching                                                                                                                                                                                                                                                                                                                                                                                      
 arith.nl.tangents                                    run tangent lemmas                                                                                                                                                                                                                                                                                                                                                                                      
 arith.nl.horner                                      run horner's heuristic                                                                                                                                                                                                                                                                                                                                                                                  
 arith.nl.horner_subs_fixed                           0 - no subs, 1 - substitute, 2 - substitute fixed zeros only                                                                                                                                                                                                                                                                                                                                            
 arith.nl.horner_frequency                            horner's call frequency                                                                                                                                                                                                                                                                                                                                                                                 
 arith.nl.horner_row_length_limit                     row is disregarded by the heuristic if its length is longer than the value                                                                                                                                                                                                                                                                                                                              
 arith.nl.grobner_frequency                           grobner's call frequency                                                                                                                                                                                                                                                                                                                                                                                
 arith.nl.grobner                                     run grobner's basis heuristic                                                                                                                                                                                                                                                                                                                                                                           
 arith.nl.grobner_eqs_growth                          grobner's number of equalities growth                                                                                                                                                                                                                                                                                                                                                                   
 arith.nl.grobner_expr_size_growth                    grobner's maximum expr size growth                                                                                                                                                                                                                                                                                                                                                                      
 arith.nl.grobner_expr_degree_growth                  grobner's maximum expr degree growth                                                                                                                                                                                                                                                                                                                                                                    
 arith.nl.grobner_max_simplified                      grobner's maximum number of simplifications                                                                                                                                                                                                                                                                                                                                                             
 arith.nl.grobner_cnfl_to_report                      grobner's maximum number of conflicts to report                                                                                                                                                                                                                                                                                                                                                         
 arith.nl.gr_q                                        grobner's quota                                                                                                                                                                                                                                                                                                                                                                                         
 arith.nl.grobner_subs_fixed                          0 - no subs, 1 - substitute, 2 - substitute fixed zeros only                                                                                                                                                                                                                                                                                                                                            
 arith.propagate_eqs                                  propagate (cheap) equalities                                                                                                                                                                                                                                                                                                                                                                            
 arith.propagation_mode                               0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds                                                                                                                                                                                                                                                                                                                           
 arith.reflect                                        reflect arithmetical operators to the congruence closure                                                                                                                                                                                                                                                                                                                                                
 arith.branch_cut_ratio                               branch/cut ratio for linear integer arithmetic                                                                                                                                                                                                                                                                                                                                                          
 arith.int_eq_branch                                  branching using derived integer equations                                                                                                                                                                                                                                                                                                                                                               
 arith.ignore_int                                     treat integer variables as real                                                                                                                                                                                                                                                                                                                                                                         
 arith.dump_lemmas                                    dump arithmetic theory lemmas to files                                                                                                                                                                                                                                                                                                                                                                  
 arith.greatest_error_pivot                           Pivoting strategy                                                                                                                                                                                                                                                                                                                                                                                       
 arith.eager_eq_axioms                                eager equality axioms                                                                                                                                                                                                                                                                                                                                                                                   
 arith.auto_config_simplex                            force simplex solver in auto_config                                                                                                                                                                                                                                                                                                                                                                     
 arith.rep_freq                                       the report frequency, in how many iterations print the cost and other info                                                                                                                                                                                                                                                                                                                              
 arith.min                                            minimize cost                                                                                                                                                                                                                                                                                                                                                                                           
 arith.print_stats                                    print statistic                                                                                                                                                                                                                                                                                                                                                                                         
 arith.simplex_strategy                               simplex strategy for the solver                                                                                                                                                                                                                                                                                                                                                                         
 arith.enable_hnf                                     enable hnf (Hermite Normal Form) cuts                                                                                                                                                                                                                                                                                                                                                                   
 arith.bprop_on_pivoted_rows                          propagate bounds on rows changed by the pivot operation                                                                                                                                                                                                                                                                                                                                                 
 arith.print_ext_var_names                            print external variable names                                                                                                                                                                                                                                                                                                                                                                           
 pb.conflict_frequency                                conflict frequency for Pseudo-Boolean theory                                                                                                                                                                                                                                                                                                                                                            
 pb.learn_complements                                 learn complement literals for Pseudo-Boolean theory                                                                                                                                                                                                                                                                                                                                                     
 array.weak                                           weak array theory                                                                                                                                                                                                                                                                                                                                                                                       
 array.extensional                                    extensional array theory                                                                                                                                                                                                                                                                                                                                                                                
 clause_proof                                         record a clausal proof                                                                                                                                                                                                                                                                                                                                                                                  
 dack                                                 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                                                                                                                                                                                                               
 dack.eq                                              enable dynamic ackermannization for transtivity of equalities                                                                                                                                                                                                                                                                                                                                           
 dack.factor                                          number of instance per conflict                                                                                                                                                                                                                                                                                                                                                                         
 dack.gc                                              Dynamic ackermannization garbage collection frequency (per conflict)                                                                                                                                                                                                                                                                                                                                    
 dack.gc_inv_decay                                    Dynamic ackermannization garbage collection decay                                                                                                                                                                                                                                                                                                                                                       
 dack.threshold                                        number of times the congruence rule must be used before Leibniz's axiom is expanded                                                                                                                                                                                                                                                                                                                    
 theory_case_split                                    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.                                                                                                                                                                       
 string_solver                                        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)                                                                                                                                    
 core.validate                                        [internal] validate unsat core produced by SMT context. This option is intended for debugging                                                                                                                                                                                                                                                                                                           
 seq.split_w_len                                      enable splitting guided by length constraints                                                                                                                                                                                                                                                                                                                                                           
 seq.validate                                         enable self-validation of theory axioms created by seq theory                                                                                                                                                                                                                                                                                                                                           
 seq.use_unicode                                      dev flag (not for users) enable unicode semantics                                                                                                                                                                                                                                                                                                                                                       
 str.strong_arrangements                              assert equivalences instead of implications when generating string arrangement axioms                                                                                                                                                                                                                                                                                                                   
 str.aggressive_length_testing                        prioritize testing concrete length values over generating more options                                                                                                                                                                                                                                                                                                                                  
 str.aggressive_value_testing                         prioritize testing concrete string constant values over generating more options                                                                                                                                                                                                                                                                                                                         
 str.aggressive_unroll_testing                        prioritize testing concrete regex unroll counts over generating more options                                                                                                                                                                                                                                                                                                                            
 str.fast_length_tester_cache                         cache length tester constants instead of regenerating them                                                                                                                                                                                                                                                                                                                                              
 str.fast_value_tester_cache                          cache value tester constants instead of regenerating them                                                                                                                                                                                                                                                                                                                                               
 str.string_constant_cache                            cache all generated string constants generated from anywhere in theory_str                                                                                                                                                                                                                                                                                                                              
 theory_aware_branching                               Allow the context to use extra information from theory solvers regarding literal branching prioritization.                                                                                                                                                                                                                                                                                              
 str.overlap_priority                                 theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true                                                                                                                                                                                                                                                                                                               
 str.regex_automata_difficulty_threshold              difficulty threshold for regex automata heuristics                                                                                                                                                                                                                                                                                                                                                      
 str.regex_automata_intersection_difficulty_threshold difficulty threshold for regex intersection heuristics                                                                                                                                                                                                                                                                                                                                                  
 str.regex_automata_failed_automaton_threshold        number of failed automaton construction attempts after which a full automaton is automatically built                                                                                                                                                                                                                                                                                                    
 str.regex_automata_failed_intersection_threshold     number of failed automaton intersection attempts after which intersection is always computed                                                                                                                                                                                                                                                                                                            
 str.regex_automata_length_attempt_threshold          number of length/path constraint attempts before checking unsatisfiability of regex terms                                                                                                                                                                                                                                                                                                               
 str.fixed_length_refinement                          use abstraction refinement in fixed-length equation solver (Z3str3 only)                                                                                                                                                                                                                                                                                                                                
 str.fixed_length_naive_cex                           construct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only)                                                                                                                                                                                                                                                                                  
 core.extend_patterns                                 extend unsat core with literals that trigger (potential) quantifier instances                                                                                                                                                                                                                                                                                                                           
 core.extend_patterns.max_distance                    limits the distance of a pattern-extended unsat core                                                                                                                                                                                                                                                                                                                                                    
 core.extend_nonlocal_patterns                        extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier's body                                                                                                                                                                                                                                                                        
 lemma_gc_strategy                                    lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none                                                                                                                                                                                                                                                                                                                   
 dt_lazy_splits                                       How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy                                                                                                                                                                                                                                                                                                                   
 blast_mul                                            (default: true) bit-blast multipliers (and dividers, remainders).                                                                                                                                                                                                                                                                                                                                       
 blast_add                                            (default: true) bit-blast adders.                                                                                                                                                                                                                                                                                                                                                                       
 blast_quant                                          (default: false) bit-blast quantified variables.                                                                                                                                                                                                                                                                                                                                                        
 blast_full                                           (default: false) bit-blast any term with bit-vector sort, this option will make E-matching ineffective in any pattern containing bit-vector terms.                                                                                                                                                                                                                                                      
 aig_per_assertion                                    (default: true) process one assertion at a time.                                                                                                                                                                                                                                                                                                                                                        
 learned                                              (default: false) collect also learned clauses.                                                                                                                                                                                                                                                                                                                                                          
 max_depth                                            (default: 1024) maximum term depth.                                                                                                                                                                                                                                                                                                                                                                     
 propagate_eq                                         (default: false) enable equality propagation from bounds.                                                                                                                                                                                                                                                                                                                                               
 add_bound_lower                                      (default: -2) lower bound to be added to unbounded variables.                                                                                                                                                                                                                                                                                                                                           
 add_bound_upper                                      (default: 2) upper bound to be added to unbounded variables.                                                                                                                                                                                                                                                                                                                                            
 produce_models                                       (default: false) model generation.                                                                                                                                                                                                                                                                                                                                                                      
 norm_int_only                                        (default: true) normalize only the bounds of integer constants.                                                                                                                                                                                                                                                                                                                                         
 lia2pb_partial                                       (default: false) partial lia2pb conversion.                                                                                                                                                                                                                                                                                                                                                             
 lia2pb_max_bits                                      (default: 32) maximum number of bits to be used (per variable) in lia2pb.                                                                                                                                                                                                                                                                                                                               
 lia2pb_total_bits                                    (default: 2048) total number of bits to be used (per problem) in lia2pb.                                                                                                                                                                                                                                                                                                                                
 pb2bv_all_clauses_limit                              (default: 8) maximum number of literals for using equivalent CNF encoding of PB constraint.                                                                                                                                                                                                                                                                                                             
 pb2bv_cardinality_limit                              (default: inf) limit for using arc-consistent cardinality constraint encoding.                                                                                                                                                                                                                                                                                                                          
 flat                                                 create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor                                                                                                                                                                                                                                                                                                                                    
 elim_and                                             conjunctions are rewritten using negation and disjunctions                                                                                                                                                                                                                                                                                                                                              
 flat                                                 create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor                                                                                                                                                                                                                                                                                                                                    
 elim_and                                             conjunctions are rewritten using negation and disjunctions                                                                                                                                                                                                                                                                                                                                              
 flat                                                 create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor                                                                                                                                                                                                                                                                                                                                    
 elim_and                                             conjunctions are rewritten using negation and disjunctions                                                                                                                                                                                                                                                                                                                                              
 flat                                                 create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor                                                                                                                                                                                                                                                                                                                                    
 elim_and                                             conjunctions are rewritten using negation and disjunctions                                                                                                                                                                                                                                                                                                                                              
 sk_hack                                              hack for VCC                                                                                                                                                                                                                                                                                                                                                                                            
 mode                                                 NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full                                                                                                                                                                                                                                                                                          
 ignore_labels                                        remove/ignore labels in the input formula, this option is ignored if proofs are enabled                                                                                                                                                                                                                                                                                                                 
 complete                                             (default: true) add constraints to make sure that any interpretation of a underspecified arithmetic operators is a function. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-root                                                                                                                                                                        
 elim_root_objects                                    (default: true) eliminate root objects.                                                                                                                                                                                                                                                                                                                                                                 
 elim_inverses                                        (default: true) eliminate inverse trigonometric functions (asin, acos, atan).                                                                                                                                                                                                                                                                                                                           
 split_factors                                        (default: true) apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0)).                                                                                                                                                                                                                                                                                                               
 max_search_size                                      (default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space.                                                                                                                                                                                                                              
 max_prime                                            (default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step.                                                                                                                                                                                                     
 num_primes                                           (default: 1) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching.                                                                                  
 common_patterns                                      (default: true) minimize the number of auxiliary variables during CNF encoding by identifing commonly used patterns                                                                                                                                                                                                                                                                                     
 distributivity                                       (default: true) minimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulas                                                                                                                                                                                                                                                                     
 distributivity_blowup                                (default: 32) maximum overhead for applying distributivity during CNF encoding                                                                                                                                                                                                                                                                                                                          
 ite_chaing                                           (default: true) minimize the number of auxiliary variables during CNF encoding by identifing if-then-else chains                                                                                                                                                                                                                                                                                        
 factor                                               (default: true) factor polynomials.                                                                                                                                                                                                                                                                                                                                                                     
 zero_accuracy                                        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) 
 min_mag                                              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                                                
 factor_max_prime                                     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                                                                                                                                  
 factor_num_primes                                    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           
 factor_search_size                                   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                                                                                                                                                           
 lazy                                                 how lazy the solver is.                                                                                                                                                                                                                                                                                                                                                                                 
 reorder                                              reorder variables.                                                                                                                                                                                                                                                                                                                                                                                      
 log_lemmas                                           display lemmas as self-contained SMT formulas                                                                                                                                                                                                                                                                                                                                                           
 check_lemmas                                         check lemmas on the fly using an independent nlsat solver                                                                                                                                                                                                                                                                                                                                               
 simplify_conflicts                                   simplify conflicts using equalities before resolving them in nlsat solver.                                                                                                                                                                                                                                                                                                                              
 minimize_conflicts                                   minimize conflicts                                                                                                                                                                                                                                                                                                                                                                                      
 randomize                                            randomize selection of a witness in nlsat.                                                                                                                                                                                                                                                                                                                                                              
 shuffle_vars                                         use a random variable order.                                                                                                                                                                                                                                                                                                                                                                            
 inline_vars                                          inline variables that can be isolated from equations (not supported in incremental mode)                                                                                                                                                                                                                                                                                                                
 seed                                                 random seed.                                                                                                                                                                                                                                                                                                                                                                                            
 nla2bv_max_bv_size                                   (default: inf) maximum bit-vector size used by nla2bv tactic                                                                                                                                                                                                                                                                                                                                            
 nla2bv_bv_size                                       (default: 4) default bit-vector size used by nla2bv tactic.                                                                                                                                                                                                                                                                                                                                             
 nla2bv_root                                          (default: 2) nla2bv tactic encodes reals into bit-vectors using expressions of the form a+b*sqrt(c), this parameter sets the value of c used in the encoding.                                                                                                                                                                                                                                           
 nla2bv_divisor                                       (default: 2) nla2bv tactic parameter.                                                                                                                                                                                                                                                                                                                                                                   
 compile_equality                                     (default:false) compile equalities into pseudo-Boolean equality                                                                                                                                                                                                                                                                                                                                         
 cofactor_equalities                                  (default: true) use equalities to rewrite bodies of ite-expressions. This is potentially expensive.                                                                                                                                                                                                                                                                                                     
 qe_nonlinear                                         (default: false) enable virtual term substitution.                                                                                                                                                                                                                                                                                                                                                      
 eliminate_variables_as_block                         (default: true) eliminate variables as a block (true) or one at a time (false)                                                                                                                                                                                                                                                                                                                          
 solver2_timeout                                      fallback to solver 1 after timeout even when in incremental model                                                                                                                                                                                                                                                                                                                                       
 ignore_solver1                                       if true, solver 2 is always used                                                                                                                                                                                                                                                                                                                                                                        
 solver2_unknown                                      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                                                                                                                                                                                                                                                       
 proof                                                proof generation, it must be enabled when the Z3 context is created                                                                                                                                                                                                                                                                                                                                     
 model                                                model generation for solvers, this parameter can be overwritten when creating a solver                                                                                                                                                                                                                                                                                                                  
 unsat_core                                           unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation