# configuration settings for bit-vector interpolation.
# See the paper
# A. Griggio, "Effective Word-Level Interpolation for Software Verification",
# FMCAD'11

# settings that should not be changed 
# (otherwise BV interpolation will not work)
interpolation = true
theory.eq_propagation = false
theory.bv.eager = false
theory.euf.dyn_ack = 0

# settings that might be changed (these are the suggested values, but feel
# free to experiment with other settings)
preprocessor.simplification = 3
theory.bv.bit_blast_aig = false
theory.bv.interpolation_mode = 0
theory.euf.enabled = true
