Сортировка несоответствия в модели

Question

Я проанализировал формулу в QF_AUFLIA с z3. Результат: sat. Модель возвращаемого (get-model) содержит следующие строки:

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

Согласно моему пониманию языка SMTLIBv2, это утверждение неверно сформированное. = следует применять только к аргументам того же типа. Однако 2 имеет сортировку Int и false имеет сортировку Bool.

Когда я кормлю назад как раз эти две линии z3, он согласен со мной, говоря:

invalid function application, sort mismatch on argument at position 2 

Является ли это ошибка?

Если нет, то как я должен интерпретировать (= 2 false)?

Answer 1

Проблема возникла из-за ошибки типа на входе. Z3 3.2 пропускает некоторые ошибки типа в макроприложениях. Эта проблема была исправлена. В следующем выпуске будет правильно сообщаться ошибка типа (aka sort несоответствие). Ниже приведен минимальный пример, который ставит проблему:

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