#
# . Options may be written in any order
# . Unrecognized options will throw an error
# . Use '#' for line comments
#
# GENERIC CONFIGURATION
#
# Regular output channel
regular_output_channel stdout
# Diagnostic output channel
diagnostic_output_channel stderr
# Prints statistics in stats.out
produce_stats 0
# Prints statistics to screen
print_stats 1
# Prints models
produce_models 0
# Dumps input formula (debugging)
dump_formula 0
# Choose verbosity level
verbosity 1
#
# SAT SOLVER CONFIGURATION
#
# Preprocess variables and clauses when possible
sat_preprocess_booleans 1
sat_dump_cnf 0
# Try to propagate first smaller clauses
sat_propagate_small 0
# Restart solver if current learnt width is greater than threshold (>0)
sat_restart_learnt_thresh 0
# Uses only original clauses of width up to threshold (>0)
sat_orig_thresh 0
#
# PROOF TRANSFORMER AND INTERPOLATOR CONFIGURATION
# Remember to add in the SMTLIB2 file
# (get-proof) or (set-option :produce-interpolants true) plus (get-interpolants)
#
# Prints proofs
print_proofs_smtlib2 0
print_proofs_dotty 0
# Enable proof checking
proof_check 0
#proof_check 1 # ALF: Use only in testing runs
# Generate a new SMTLIB2 file by splitting the input formula into (sat_dump_rnd_inter+1) partitions
sat_dump_rnd_inter 0
# Set to 0,1,2,3 to use McMillan, Pudlak, McMillan', minimal interpolation algorithm
proof_set_inter_algo 0
# Use dual formula for interpolant minimization in Pudlak
proof_alternative_inter 0
# Choose:
# 0 for path interpolation, 1 for simultaneous abstraction
# 2 for gen. simultaneous abstraction, 3 for state-transition interpolation
proof_multiple_inter 0
# Enable proof restructuring step for generation of interpolants (partially) in CNF
# Needs exactly two partitions and McMillan interpolation algorithm
proof_interpolant_cnf 0
# Enable light proof restructuring step for generation of stronger/weaker interpolants
# Needs exactly two partitions and McMillan/McMillan'/Pudlak interpolation algorithm
# 1 for stronger interpolants, 2 for weaker interpolants
proof_trans_strength 0
# Enable certification of interpolants
proof_certify_inter 0
#proof_certify_inter 1 # Use z3 to verify computed itps. Only fortesting
certifying_solver ./tool_wrapper.sh
# Proof reduction is based on a run of LowerUnits followed by a number of global iterations.
# Each global iteration consists of: RecyclePivots, StructuralHashing, TransformationTraversals
# Enable structural hashing while building proof
proof_struct_hash_build 0
# Enable proof reduction
proof_reduce 0
# Enable LowerUnits
proof_push_units 1
# Enable RecyclePivots
proof_rec_piv 1
# Enable StructuralHashing
proof_struct_hash 1
# Invert the normal order StructuralHashing -> RecyclePivots
proof_switch_to_rp_hash 0
# Enable proof TransformationTraversals
proof_transf_trav 1
# Reduction timeout w.r.t. solving time for each global iteration
proof_ratio_red_solv 0
# Reduction timeout for each global iteration
proof_red_time 0
# Number of TransformationTraversals for each global iteration
proof_num_graph_traversals 0
# Number of global iterations
proof_red_trans 0
#
#
assignment_mode PVAI