Yes. Been there, done that, with the pre-ACL2 Boyer-Moore prover. We had the Oppen-Nelson prover (the first SAT solver) handling the easy stuff, and used the Boyer-Moore prover for the hard stuff. Not that much manual work.

I assume you mean first SMT solver when you refer to Oppen-Nelson? I thought their contribution was the basis for SMT methods.