Any replacement for Timeout? (to ensure determinacy)

[tczpl]

Thanks for helping me.

My problem is that, if I use timeout, then the solving result might be different on different CPU.

For example, as for the same SMT, CPU A spends 3 seconds, but CPU B spends 6 seconds, to solve it as SAT.
Hence, if I set timeout=5s, then CPU A is different with CPU B, SAT v.s. Unknown.

This looks like some kind of randomness.
Is there any parameter to replace Timeout, then A and B can stop at the same point, then we can achieve determinacy rather than randomness?

Thanks for your answer, very very much.

[tczpl]

Hey guys I am a noob on SMT solving, I just wonder that, is it possible to set other parameters, e.g., depth, steps, counter? I want my program to be reproducible with the same result but on different CPUs.

I find an option max_steps in the code, but I am not sure of it and I cannot find the document on it.

If there is no such parameter on Z3 now, is it possible for me to add one, how difficult is that?

Thanks for all your help!

[tczpl]

[NikolajBjorner]

there is a resource limit parameter. It is called rlimit. Finding good values for it can be done by running z3 with a timeout, then picking the value from rlimit shown in statistics.
z3 'file' -t:2000 -st
z3 'file' rlimit='value-shown-in-statistics'

[tczpl]

Thanks for your very detailed answer, which is also quick. Let me try. Many thanks!