Z3 -p 通过运行获得的参数的文档。通过运行获得有关特定选项的详细信息Z3 -pp：OPTION_NAME 。

The documentation for the parameters is obtained by running z3 -p. More information about a particular option is obtained by running z3 -pp:option_name.

参数的基础设施已经看到了在4.3.2重大变化;现在有参数模块和soft_timeout所在的SMT模块中，即正确的名称是 smt.soft_timeout 。没有设置逻辑，但我们不能假设它会自动确定（仅适用于其中的一些）。相反，我们现在可以构造求解器（通过在C ++中求解::求解器（上下文和C，字符常量*逻辑））对象为特定的逻辑，或使用一个在predefined SMT战术（如见，在战略教程）

The parameter infrastructure has seen major changes in 4.3.2; there are now parameter modules and the soft_timeout resides in the smt module, i.e., the proper name is smt.soft_timeout. There is no setting for the logic, but we can't assume that it will be determined automatically (works only for some of them). Instead, we can now construct Solver objects for a particular logic (in C++ via solver::solver(context & c, char const * logic)), or use one of the predefined SMT tactics (see e.g., the strategies tutorial)