It is possible to set parameter sat.threads to make z3py use multiple threads for satisfiability problems with Boolean variables.

Example code:

if cfg.threads > 1:
    z3.set_param("sat.threads", cfg.threads)

As recommended here, I also tried:

z3.set_param("parallel.enable", True)
z3.set_param("parallel.threads.max", 8)

The program still does not use more than one thread. In fact, it does use multiple threads, but it does not consume more than 12.5% of the CPU capacity of my 8-core machine.

What about problems like this with integer rather than Boolean decision variables?

How can I activate z3py multithreading for such problems?