(set-option :bv-solver prop)