Does parallel version of Z3 work for BV logic?

Question

I could not utilize both cores of the processor with parallel Z3 3.2 (from bin_mt or x64_mt directory) with PAR_NUM_THREADS=2 on Windows7. The same 50% and no time difference with single threaded version.

Is parallel version supported for these logics or it works with QF_IDL only?

Answer 1

By mistake, parallel execution hasn't been included in Z3 3.2. That's why Z3 still runs sequentially when you set PAR_NUM_THREADS=2. Z3 team has corrected the mistake so parallel feature will be available in the next release.

EDIT:

As @Leo mentioned in the comment, parallel feature is now planned for Z3 4.1.