Z3_SINGLE_THREADED CMake option meaning

[etienne-mlsc]

Hello,

Can someone clarify the purpose of the Z3_SINGLE_THREADED build option? My first understanding is that, when turned on, it would disable parallel processing and solving. But the CMakeList.txt describes it as "Non-thread-safe build" which sounds a bit contradictory:

Does this allows benefits in case it is certain that we would run in a single threaded environment?

Thanks in advance!

[NikolajBjorner]

If you build z3 with single-threaded and then use the API to spawn multiple threads with separate contexts then code that was previously thread safe isn't any longer.
If you are just using z3.exe, then multi-threaded features are disabled internally. It is safe.
The option is used when applications only use a single thread for z3 and it then avoids overhead that is required for multi-threading.