(set-option :bv-solver "prop)