Sort Mismatch w Modelu

Question

Przeanalizowałem formułę w QF_AUFLIA z Z3. Wynikiem było sat. Model zwrócony przez (get-model) zawierał następujące linie:

(define-fun PCsc5_() Int 
    (ite (= 2 false) 23 33) 

Według mojego rozumienia języka SMTLIBv2, to stwierdzenie jest źle sformułowany. = należy stosować tylko do argumentów tego samego rodzaju. Jednak 2 ma sortowanie Int i false ma sortowanie Bool.

Kiedy zwrotnie tylko te dwie linie do Z3, to zgadza się ze mną, mówiąc:

invalid function application, sort mismatch on argument at position 2 

Czy to błąd?

Jeśli nie, jak mam interpretować (= 2 false)?

Answer 1

Problem spowodowany był błędem typu na wejściu. Z3 3.2 pomija niektóre błędy typów w aplikacjach makr. Ten problem został rozwiązany. Następne wydanie poprawnie zgłosi błąd typu (niezgodność sortowania aka). Oto minimalny przykład, który ujawnia problem:

(set-option :produce-models true) 
(declare-fun q (Int) Bool) 
;; p1 is a macro 
(define-fun p1 ((z Int) (y Int)) Bool 
    (ite (q y) (= z 0) (= z 1))) 
(declare-const a Int) 
(declare-const b Bool) 
(assert (p1 a b)) ;; << TYPE ERROR: b must be an Int 
(check-sat) 
(get-model)