5

我已经用 z3 分析了 QF_AUFLIA 中的一个公式。结果是sat。返回的模型(get-model)包含以下几行：

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

根据我对 SMTLIBv2 语言的理解，这个语句是畸形的。=只能应用于相同类型的参数。但是，2有 sortInt和false有 sort Bool。

当我将这两行反馈给 z3 时，它同意我的说法：

invalid function application, sort mismatch on argument at position 2

这是一个错误吗？

如果不是，我应该如何解释(= 2 false)？

4

1 回答 1

5

问题是由于输入中的类型错误造成的。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)
于 2012-01-05T00:45:43.200 回答