# some reasonable configuration settings for formulae in the combination of
# Floating Points and Bit-Vectors

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
dpll.preprocessor.mode = 1
theory.bv.eager = true
theory.bv.bit_blast_mode = 2
theory.bv.delay_propagated_eqs = true
theory.arr.mode = 1
theory.la.enabled = false
theory.eq_propagation = false
theory.fp.mode = 1
theory.fp.bit_blast_mode = 2
theory.fp.bv_combination_enabled = true

# set these to true if you need uninterpreted functions and/or arrays
theory.euf.enabled = false
theory.arr.enabled = false
