Sort Mismatch nel modello

Question

Ho analizzato una formula in QF_AUFLIA con z3. Il risultato è stato sat. Il modello restituito da (get-model) conteneva le seguenti righe:

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

Secondo la mia comprensione della lingua SMTLIBv2, questa affermazione non è valido. = deve essere applicato solo agli argomenti dello stesso tipo. Tuttavia, 2 ha ordinamento Int e false ha ordinamento Bool.

Quando ho feed back solo queste due righe per Z3, è d'accordo con me dicendo:

invalid function application, sort mismatch on argument at position 2 

È questo un bug?

In caso contrario, come dovrei interpretare (= 2 false)?

Answer 1

Il problema era dovuto a un errore di tipo nell'input. Z3 3.2 manca alcuni errori di tipo nelle applicazioni macro. Questo problema è stato risolto. La prossima versione riporterà correttamente l'errore di tipo (noto anche come mancata corrispondenza). Ecco un esempio minimale che espone il problema:

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