z3 - smtlib 代码有问题

Question

我有以下代码

(set-logic QF_LIA)
(declare-fun w () Int)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (> x y))
(assert (> y z))
(push 1)
(assert (> z x))
(check-sat) ; unsat
(get-info :statistics)
(pop 1)
(push 1)
(check-sat (= x w)) ; sat

代码应该在第一个（check-sat）返回 unsat 并在第二个（check-sat）返回，但我不知道。

有人可以告诉我有什么问题。我正在使用 Windows 7，使用 cygwin 的 jSMTLIB

谢谢赛义夫

Answer 1

我不知道您使用 jSMTLIB 中的哪个后端来解决这个问题。但是，(check-sat (= x w))在 SMT-LIB v2 中甚至不合法。

当我将该行更改为：

(assert (= x w))
(check-sat)

我从 Z3 Web 界面获得unsat和来自我们的期望。sat

注意(get-info :statistics)也是不正确的；正确的选项是(get-info :all-statistics)。您可以在他们的文档中阅读有关 SMT-LIB v2 标准的更多信息。