Internal Solver State and Cloning of a Solver

[baierd]

Hi,

is it possible to clone/copy an existing solver with its internal state?
If not, would it be possible to add this?

Our use-case is that we add formulas to the assertion stack, check them and then want to continue in multiple ways (concurrently) without removing the assertions. For this we reuse the previously used solver and additionally create new solvers where we add the formulas from the other solver. We already know that the solver instance that previously checked the formulas for satisfiability is much faster compared to a new solver instance. We guess that the solver remembers some lemmas etc.?

Best,
Daniel from JavaSMT

[NikolajBjorner]

Does this work for what you need? https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_solver.html#a2f4086956a17bb24964a5b0d53ff65f6

[baierd]

Most likely yes!
I will test this and report back.

Thank you!

[baierd]

I've tested the function and found that it produces an com.microsoft.z3.Z3Exception: translation of contexts is only supported at base level error if we have already pushed the assertion stack. Is it possible to use the call with an already used assertion stack? (Please note that we use the internal API)