什么是重新激活Z3水货版本目前的计划是什么？
Answer 1:
Z3从未有过的并行广泛的支持。 在2.x版本，包括我们的实验性功能，允许用户在并行执行多个副本不同的配置选项。 不同的副本也可以共享信息和修剪互相搜索空间。 此功能有一定的局限性。 例如，它不是编程API可用。 这也与发生冲突的长期研究目标和方向。 因此，这个功能已经从最近的版本中删除。
话虽这么说，Z3的4.x的API中，可以安全地创建多个上下文（Z3_Context），并从不同的线程同时访问它们。 在以前的版本中不是线程安全的。 在Z3 4.x中，我们可以定义使用并行组合程序自定义策略。 例如，组合子(par-or t1 t2)执行策略t1和t2平行。 这些组合子是编程API和SMT 2.0前端中提供。 以下在线教程包含附加信息： http://rise4fun.com/Z3/tutorial/strategies
下面的命令（用于SMT 2.0前端）将检查用的策略的两个拷贝的断言式smt用不同的随机种子。
(check-sat-using (par-or (! smt :random-seed 10) (! smt :random-seed 20)))
文章来源: When will the Z3 parallel version be reactivated? [closed]
