Detailed documentation of Z3 INI options

Is there any detailed documentation of the INI options of Z3. I had to do a trial and error approach to figure out the best options for my QF_BV problems. I am still not sure if there are more o开发者_开发问答ptions that would make my z3-run faster. It would be great if someone can point to any existing detailed explanation of the INI options.

Thanks.

We are currently restructuring Z3, and moving away from the approach: a solver with “thousand” parameters. We are moving Z3 into a more modular and flexible approach for combining solvers and specifying strategies. You can find more information about this new approach in the following draft.

Regarding INI options, several of them are deprecated, and only exist because we didn’t finish the transition to the new approach yet. Several of these options were added for particular projects, and are obsolete now. They only exist for backward compatibility.

Regarding QF_BV, Z3 3.2 contains two QF_BV solvers: old (the one from 2.x) and new. The new (official) one is only available in the Z3 official input format: SMT 2.0. SMT 1.0, Simplify and Z3 low level input formats are obsolete. Most of the performance improvements in Z3 3.x are only available when one uses SMT 2.0 input format.

In a couple of months, the strategy specification language will be officially supported in Z3. We will have a tutorial and documentation describing how to use it. In the meantime, I strongly recommend that you use the default configuration and the SMT 2.0 input format for logics such as QF_BV.