#
# MathSAT5 configuration file for the main track of SMT-EVAL 2013
#

theory.fp.enabled = false

[QF_AUFLIA, QF_ALIA]
theory.la.pure_equality_filtering = true 
theory.arr.enable_nonlinear = true 
theory.la.detect_euf_fragment = true 
theory.la.delay_alien = true
theory.euf.dyn_ack = 2
theory.euf.dyn_ack_threshold = 100
theory.bv.enabled = false 
theory.arr.permanent_lemma_inst = true 
theory.arr.enable_witness = true
dpll.ghost_filtering = false
dpll.branching_random_frequency = 0
preprocessor.simplification = 5

[QF_AX]
theory.bv.enabled = false
theory.la.enabled = false
preprocessor.simplification = 7 
theory.arr.permanent_lemma_inst = true 
dpll.branching_random_frequency = 0 
theory.euf.dyn_ack = 2 
theory.euf.dyn_ack_threshold = 10 
theory.arr.enable_nonlinear = true

[QF_LIA]
theory.arr.enabled = false
theory.bv.enabled = false
dpll.branching_random_frequency = 0

[QF_LRA]
theory.arr.enabled = false
theory.bv.enabled = false

[QF_UF]
theory.arr.enabled = false
theory.bv.enabled = false
theory.la.enabled = false

[QF_UFLIA]
theory.arr.enabled = false
theory.bv.enabled = false
dpll.branching_random_frequency = 0

[QF_UFLRA]
theory.arr.enabled = false
theory.bv.enabled = false

[QF_BV, QF_UFBV, QF_AUFBV, QF_ABV]
preprocessor.toplevel_propagation = true
preprocessor.simplification = 7
dpll.branching_random_frequency = 0.01
dpll.branching_random_invalidate_phase_cache = true
dpll.restart_strategy = 3
dpll.glucose_var_activity = true
dpll.glucose_learnt_minimization = true
theory.bv.eager = true
theory.bv.bit_blast_mode = 1
theory.bv.delay_propagated_eqs = true
theory.arr.mode = 1
theory.la.enabled = false

[QF_BV]
theory.eq_propagation = false 
theory.la.enabled = false 
theory.arr.enabled = false

[QF_AUFBV, QF_ABV]
theory.la.enabled = false
theory.bv.delay_propagated_eqs = true
theory.arr.max_wr_lemmas = 0
theory.arr.enable_nonlinear = true
theory.arr.enable_witness = false
theory.arr.permanent_lemma_inst = true
theory.eq_propagation = false
theory.interface_eq_policy = 3

[QF_UFBV]
theory.arr.enabled = false

[QF_AUFBV]
theory.interface_eq_policy = 0
