Does the parallel version of Z3 use BV logic?

Question

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

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

Answer 1

By mistake, parallel execution was not included in Z3 3.2. Therefore, Z3 is still executed sequentially when you set PAR_NUM_THREADS=2 . The Z3 team fixed the error, so the parallel function will be available in the next version.

EDIT:

As mentioned in a comment by @Leo, a parallel function is now planned in Z3 4.1.