1

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_UF)
(set-option :incremental true)
(set-option :produce-models true)
(declare-fun m () Bool)
(declare-fun p () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun r () Bool)
(declare-fun al () Bool)
(declare-fun all () Bool)
(declare-fun la () Bool)
(declare-fun lal () Bool)
(declare-fun g () Bool)
(declare-fun a () Bool)
(define-fun conjecture () Bool
(and (= (and (not r) c) m) (= p m) (= b m) (= c (not g)) 
     (= (and (not al) (not all)) r) (= (and la b) al) 
     (= (or al la lal) all) (= (and (not g) p a) la) 
     (= (and (not g) (or la a)) lal)))
(push 1)
(assert (and conjecture (= a false) (= g false)))
(check-sat)
(get-model)
(pop 1)
(push 1)
(assert (and conjecture (= a false) (= g true)))
(check-sat)
(get-model)
(pop 1)
(push 1)
(assert (and conjecture (= a true) (= g true)))
(check-sat)
(get-model)
(pop 1)
(push 1)
(assert (and conjecture (= a true) (= g false)))
(check-sat)
(get-model)
Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
Juan Ospina
  • 1,317
  • 1
  • 7
  • 15
  • 1
    I've tried the Windows version of Alt-Ergo. It complains about "(get-model)". Once I removed theses lines, I got unknown/unsat results which should be "sat". I also tried adding the "-sat" commandline parameter, but this did not change anything. Strange! – Axel Kemper Jun 02 '13 at 10:40
  • Many thanks for your answer. You are right, when the lines "(get-model)" are removed the code runs in Alt-Ergo but the generated output is wrong: unsat, unsat, unsat, unsat. – Juan Ospina Jun 02 '13 at 13:01

1 Answers1

2

For now, Alt-Ergo does not provide a full support for the SMT-2 format. In particular, the command get-model is not recognized.

Moreover, the commands push and pop are ignored. This is why Alt-Ergo says sat, unsat, ..., unsat on the given code (when get-model is removed).

iguerNL
  • 464
  • 2
  • 8