Context-wise or thread-wise random seed?

[riscvare]

I am creating multiple Z3 contexts on multiple threads using C/C++ API. I see that I can set the global parameters "'smt.random_seed" and "sat.random_seed".

Is it possible to set these parameters at context level or at thread-level?

Is there some other way to enable deterministic behavior when creating and solving multiple contexts on parallel threads?

[NikolajBjorner]

You can set these parameters on the "solver" object. They will be local to each solver.

[dgpv]

Z3 will throw "unknown parameter" exception when trying to set "smt.random_seed" for the solver object. The exception text gives a list of possible params, but no smt.* or sat.* params are listed there.

[dgpv]

It turns out that the parameter name for the solver object is simply "random_seed"

[NikolajBjorner]

I have wanted to get rid of sat.random_seed and smt.random_seed for a long time. It is going to be a bit of a breaking change, but just having random_seed should streamline such confusing experiences.