Conflicting solver selection should make CBMC fail

[tautschnig]

Running cbmc --smt2 --external-sat-solver kissat some.c will currently pick the SAT solver over SMT2, but really CBMC should fail when command-line options contradict each other.

[rod-chapman]

+1 to this. It's a common failure more if the users has EXTERNAL_SAT_SOLVER in their environment, but doesn't know it, then wonders why their proofs aren't working.