如何在Z3Py中设置软超时（-t参数）

Z3命令行的-t参数对应Z3Py中的timeout配置项，单位为毫秒，以下是正确的设置方式：

• 全局生效（所有Solver/Optimize实例都会应用该超时）：

  from z3 import *
  set_option("timeout", 60 * 1000)  # 设置60秒软超时
  

• 仅针对单个Optimize实例生效：

  opt = Optimize()
  opt.set("timeout", 60 * 1000)  # 当前Optimize实例使用60秒软超时
  

你之前尝试的soft_timeout、t、smt.soft_timeout等参数名均不符合Z3Py的API规范，所以无法生效。

内容的提问来源于stack exchange，提问作者谭思危