Since SMT-LIB has already been mentioned (it is both an input format and a huge benchmark), I should point out that it is divided in plenty of categories, the joke goes that there is one category per prover participating in the corresponding competitions.
True, but I'd still recommend checking out the latest smt-comp results as first step for solver selection. At least for the kind of problems I'm working with (mostly incremental QF_AUFBV) the smt-comp results match my own benchmarks pretty well.
