Pseudo-incremental EF solving?

[boqwxp]

I typically call Yices in EF BV mode repeatedly, each time on a very slightly different problem--only one constant argument to a bvule changes. The idea is to assert some constant threshold on a value in the design, change that threshold for each problem, and keep solving problems until we find a model that minimizes/maximizes that value.

This is AFAIK the only reasonable approach, as I do not know of any SMT solver that supports a proper optimization procedure for quantified values. Obviously it seems also to be hugely wasteful, with an enormous amount of duplication of effort.

Would it be straightforward to take the following approach to eliminating much of that duplicated effort? Would this approach, at first estimation, work? Are there any obvious impediments?

Idea

The idea is to save the learned clauses for the exists/forall contexts when a model is found or the problem is determined to be UNSAT. When the solver is started again on a slightly different problem, it can load in the saved learned clauses from the previous problem. Of course, not all learned clauses are guaranteed still to be implied, but most will be, so there needs to be import validation to ensure each loaded learned clause is actually still implied.