(check-sat) vs (check-sat-using smt)

Question

看完Z3的strategies guide和Leo的this answer，我以为(check-sat)和(check-sat-using smt)是等价的。然而，当针对我们的测试套件（230 个 SMTLIB2 文件）运行 Z3 4.3.2 三次时，(check-sat) 需要 198s/192s/195s 秒，而(check-sat-using smt) 需要 275s/283s/270s。我也试过nightly build Z3 4.4.0 d3fb5f2a4cda，差别也差不多。

为什么会这样？

更多可能相关的信息：

• Windows 7 x64、Z3 x64
• 我们所有的测试都配置了auto_config false和smt.mbqi false
• 都使用量词和未解释的函数
• 有些使用（非线性）int 和/或实数算术
• 所有人都大量使用 push-pop 块

编辑：我最终想做的是为 一些 check-sat 调用设置超时，但不是全部。 AFAIK，check-sat 本身是不可能的，但check-sat-using (using-params smt :soft_timeout $timeout) 应该可以工作。对吗？

Answer 1

我假设您在 SMT2 文件上运行 Z3？

Z3 具有在未指定基准时确定基准逻辑的工具（参见例如default_tactic.cpp）。 smt 策略是没有其他策略适用时的后备策略。当 Z3 使用 -v:10 运行时，它会显示运行的是哪个（子）策略。

在最近的过去，我们还遇到了一些配置参数无法通过 smt 内核的问题。我们已经修复了这些，但当然也有可能某个地方仍然存在错误。