Is it possible to store and load the state of the Z3 prover across different program launches?

[gogo9th]

Hi,

I am using the Z3 prover to solve path constraints for execution paths of a target application. However, due to the limitation of my system's setup, I need to re-launch the Z3 prover's wrapping program whenever a single execution path of the target application is fully explored. For example, if there are 8 execution paths in a target application, I need to run the Z3 prover's wrapping program 8 times freshly. This is very inefficient, because whenever the Z3 prover gets re-launched, it forgets about the intermediate results (i.e., learned satisfiability) of prior path constraints of the target program. Such intermediate results could have been re-used for resolving other related path constraints. To solve such inefficiency, I wonder if there is any way I can store any intermediate results (prior knowledge) to the disk before finishing the Z3 prover's wrapping program and reload/reuse them when it re-launches.

[NikolajBjorner]

Depending on which backend solver you use, get function for retrieving assertions from a solver state follows the internal state.
It may work out if you first "copy" the original solver into a fresh solver (use the "translate" function) and then extract formulas.
Since the solver state may be obtained after rewriting, models for the original formula are not generally preserved.
The routines for printing solver state to SMTLIB have some remedies for model repair.