introduce new --smt-bitvectors command line option

We sort of jumped the gun in 6c92a15f in
supporting an unknown or even blank logic. When calling a portfolio solver that
calls out to, e.g., Z3 as well as another solver that only supports bitvectors,
you want to (a) pass no logic but also (b) use bitvectors. There's currently no
way to do this. This commit lays the ground for controlling this more
accurately. Note that this option is not plumbed to any functionality yet.