如何使用 Alt-Ergo 运行以下 SMT-LIB 代码

Question

以下 SMT-LIB 代码在 Z3、MathSat 和 CVC4 中运行没有问题，但在 Alt-Ergo 中没有运行，请告诉我发生了什么，非常感谢：

(set-logic QF_LIA)
(set-option :interactive-mode true) 
(set-option :incremental true)
(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)
(pop 1)
(get-info :all-statistics)
(push 1)
(assert (= x w))
(check-sat)
(get-assertions)
(exit)

在线运行这个例子here

1. 在 Z3 中，会生成消息 unsupported ; :incremental，但这不会改变计算并获得正确的答案。

2. 在 mathsat 中，会生成一些消息 unsupported，但会显示正确答案。

3. 在Cvc4中代码执行没有问题，得到正确答案。

4. 在 Alt-Ergo 中，代码在没有消息的情况下执行，但会生成错误答案 unsat（正确答案是：unsat, sat）。

Answer 1

关于 Alt-Ergo 和 SMT-LIB2，请考虑在此处阅读您之前帖子之一的答案：How to execute the following SMT-LIB code using Alt-Ergo