根据http://research.microsoft.com/en-us/um/people/leonardo/z3_doc/parallel.html，如果我使用的是.smt文件，则可以从z3命令行设置CC_NUM_THREADS = 4。
如果我使用的是z3py API，该怎么办？
最佳答案
支持引理共享的投资组合求解器不是最新版本的Z3的一部分。因此，不支持这些参数，也不支持允许每个参数使用多个值的参数格式（在命令行或通过python）。
也就是说，仍然存在一种利用多个内核的方法，这是同等策略。参见例如Z3 Strategy Tutorial（搜索par-or）。该示例显示了如何通过SMT2输入语言并行运行多种策略（在此示例中，具有不同的随机种子）。在z3py中，我们将使用ParOr function来创建这种并行策略。