How to leverage the fact that I'm solving 1000's of very similar SMT instances?
Some SAT solvers and SMT solvers offer an interface that lets you push clauses, and then later pop/retract them and push some new ones.  You could explore to see whether this offers a speedup in your situation.  There are no guarantees, and the only way to tell is to try it.