I started with a solver-heavy approach whereby the SMT solver was trusted to come up with all sorts of things. By a process of steady refinement, my experience

I started with a solver-heavy approach whereby the SMT solver was trusted to come up with all sorts of things. By a process of steady refinement, my experience is that if there's a change whereby you trust the solver less and your own optimizations more, you do it. So now I call the SMT solver a gazillion times with much more simple problems. I also use the SMT solver in a bunch of different ways to invent general and specific (i.e. knowing the workload) optimizations for the problem which I then can apply without intervention of a solver. I may ultimately wind up throwing SMT under the bus and doing my own bit-blasting; QF_BV ("the quantifier-free bit-vector logic") is not one of SMT's more difficult corners, and I may get some benefit in specializing my own bit-blast and talking straight to a SAT solver. I have been doing a fair bit of work to try to reduce the 'black box' aspect of SMT solver performance, but SMT is hard to get a handle on it. One minute, you're solving Sudoko and logic problems ("The professor lives in the same street as the baker, while the man who lives in the blue house does not ride a bike, ..."). The next, staring at pages and pages of math that's aimed at people who want to be researchers in SMT - there's not much intermediate-level stuff aimed at the practitioners.