z3cvc4alt-ergo

How to run the following SMT-LIB code using Alt-Ergo

The following SMT-LIB code runs without problems in Z3, MathSat and CVC4 but it is not running in Alt-Ergo, please let me know what happens, many thanks:

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

Run this example online here

  1. In Z3, the message unsupported ; :incremental is generated but this does not alter the computations and the correct answer is obtained.

  2. In mathsat, some messages unsupportedare generated but the correct answer is displayed.

  3. In Cvc4 the code is executed without problems and the correct answer is obtained.

  4. In Alt-Ergo the code is executed without messages but wrong answer unsat is generated ( the correct answer is : unsat, sat).

Solution

  • Regarding Alt-Ergo and SMT-LIB2, please consider reading the answer to one of your previous posts here: How to execute the following SMT-LIB code using Alt-Ergo