(set-option :bv-solver prop")