Configuring Parallel Z3

Multi-Core Usage

By default, all versions of parallel Z3 behave like the sequential Z3. To run a parallel Z3, run z3.exe in the directory bin_mt (or x64_mt for 64 bit machines) and supply the number of cores that you want to run, e.g.,

   z3 <file.smt> CC_NUM_THREADS=4

Lemma sharing may be configured via two options:

• CC_SHARING Sets the sharing mode (0=off, 1=dynamic, 2=static)

• CC_SHARING_LIMIT_NEAR Sets the maximum lemma size for inter-core sharing.

E.g., to run four cores with static sharing of lemmas up to size 8, use

   z3 <file.smt> CC_NUM_THREADS=4 CC_SHARING=2 CC_SHARING_LIMIT_NEAR=8

Portfolio Setup

By default, Z3 will start up to eight different SAT-strategies. Users can configure their own portfolio on the command line; automatic configuration is turned off if this feature is used. For example, to run on three cores with identical configuration, but different initial restart intervals, use

   z3 <file.smt> CC_NUM_THREADS=3 RESTART_INITIAL=100{200,300}  

where 100 is the default option and {200,300} configures the first two cores. I.e., using the above configuration, the first two cores on the machine will use 200 and 300 as their intial restart intervals, while the third core uses 100.