0

以下 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)

在此处在线运行此示例

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

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

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

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

4

1 回答 1

1

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

于 2013-11-30T19:57:44.763 回答