How to leverage the fact that I'm solving 1000's of very similar SMT instances? I have a core SMT solver problem consisting of 100,000 bit-vector array clauses, and one 10000-dimensional bit-vector array.  Then, my program takes as input k &lt;&lt; 100,000 new clauses, and adds them to the core SMT problem.  My goal is, for any input of k clauses, to solve the entire problem.
Is there any static optimization or learning I could do on the core problem in order to find a better way to solve each of its siblings?  For instance, is there some property of the graph of bit-vector variables being constrained in each clause that I could use as a heuristic for solving the specific instances?
Thanks!
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.