SMT solvers support stack-based incremental solving, but it only supports going back and forth at the end of the history chain and needs manual creation of checkpoints. I want an SMT solver with continuous learning that works out-of-the-box. If a solver previously checked conditions A and B independently, that information could be used later to make checking for A && B faster. I believe a solver with this optimization will significantly improve the performance of many research projects that rely on satisfiability checking.

To be more specific, symbolic execution engines will greatly benefit from this optimization. State-of-the-art symbolic execution engines are caching terms on the execution side to reduce the number of calls to SMT solvers. This optimization surely helps, but it is still pretty limited. Doing similar optimizations on the solver side is more promising to me since solvers have a better context to utilize that information. There is a report that nonoptimized stack-based incremental solving already gives 5x speedup, and I believe we can achieve greater speedup with an optimization based on continuous learning.