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

Question

看完strategies guide Z3 和 this answer利奥，我预计(check-sat)和 (check-sat-using smt)是等价的。然而，当针对我们的测试套件(230 个 SMTLIB2 文件)运行 Z3 4.3.2 三次时，(check-sat) 花费了 198s/192s/195s 秒。 , 但 275s/283s/270s 与 (check-sat-using smt) .我还尝试了 nightly build Z3 4.4.0 d3fb5f2a4cda，差异是相似的。

为什么会这样？

可能相关的更多信息:

• Windows 7 x64、Z3 x64
• 我们所有的测试都配置了 auto_config false和 smt.mbqi false
• 全部使用量词和未解释的函数
• 一些使用(非线性)整型和/或实数运算
• 所有人都大量使用推弹 block

编辑:我最终想做的是为一些设置超时check-sat电话，但不适合所有人。据我所知，这对于 check-sat 是不可能的本身，而是check-sat-using (using-params smt :soft_timeout $timeout)应该管用。是吗？

Answer 1

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

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

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