Несоответствие сортировки в модели

Я проанализировал формулу в 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)?