Limiting the number of threads

[riscvare]

I am trying to limit the number of threads invoked by Z3. I have disabled parallelism by set_param("parallel.enable", false) and also set_param("parallel.threads.max", 1).

Yet I see that there are 8 threads invoked on my machine. I am using bvecs in incremental mode and I have set_param("smt.phase_selection", 5). Only one thread is fully active though. The other seven threads are becoming active for a few millisecond.

Is that the expected behavior? Is it possible to have absolutely one active thread?

[NikolajBjorner]

Use the "simple solver" or set your tactic manually.
The default solvers will attempt strategies that involve multiple threads.