(检查-卫星)与(使用smt的校验-卫星)

Question

在阅读了狮子座的“战略指南 of Z3”和“这个答案”之后，我认为(check-sat)和(check-sat-using smt)是等价的。然而，当我们的测试套件(230个SMTLIB2文件)运行三次SMTLIB2 4.3.2时，(check-sat)需要198 s/192 s/195秒，而(check-sat-using smt)需要275 s/283 s/270秒。我还尝试了夜间构建Z3 4.4.0 d3fb5f2a4cda，两者之间的差别是相似的。

为什么会这样？

更多可能相关的信息：

• Windows 7 x64，Z3 x64
• 我们所有的测试都配置了auto_config false和smt.mbqi false。
• 都使用量词和未解释的函数。
• 一些使用(非线性) int和/或实算法。
• 所有的人都大量使用推弹块。

编辑：我最终想做的是为一些check-sat调用设置一个超时，但不是为所有的调用设置一个超时。AFAIK，这在check-sat本身是不可能的，但是check-sat-using (using-params smt :soft_timeout $timeout)应该能工作。是那么回事吗？

Answer 1

我猜你是在SMT2文件上运行SMT2吗？

当没有指定基准时，Z3具有确定基准测试逻辑的功能(例如，tactic.cpp)。smt策略是在没有其他策略适用的情况下的退路。当Z3与-v:10一起运行时，它将显示运行哪个(子)-tactic。

在最近的过去，我们也遇到了一些问题，配置参数不能通过smt内核。我们已经解决了这些问题，但当然有可能在某个地方还存在一个bug。