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

Question

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

(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)

在线运行此示例这里

1. 在Z3中，将生成消息unsupported ; :incremental，但这不会改变计算结果并获得正确的答案。
2. 在mathsat中，会生成一些消息unsupported，但会显示正确的答案。
3. 在Cvc4中，代码没有问题地执行，并得到正确的答案。
4. 在answer中，代码是在没有消息的情况下执行的，但是生成了错误的答案unsat (正确的答案是：unsat, sat)。

Answer 1

关于Alt-Ergo和SMT-LIB2 2，请考虑阅读您之前的一篇文章的答案：如何使用Alt执行以下SMT代码。