在模型中排序不匹配

Question

我用z3分析了QF_AUFLIA中的公式.结果是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错过了宏应用程序中的某些类型错误.这个问题已得到解决.下一个版本将正确报告类型错误(即排序不匹配).这是一个揭示问题的最小示例:

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