Z3 给出的序列模型错误

Question

(declare-const s (Seq Int))
(declare-const t1 (Seq Int))
(declare-const t2 (Seq Int))
(declare-const n Int)

(assert (= (seq.len s) n))
(assert (>= n 3))
(assert (= (seq.extract s 0 (- n 1)) t1))
(assert (= (seq.extract s 1 (- n 1)) t2))
(assert (= t1 t2))
;;(assert (not (= (seq.at s 0) (seq.at s (- n 1)))))

(check-sat)
(get-model)

结果是

sat
(model 
  (define-fun s () (Seq Int)
    (seq.++ (seq.unit 14) (seq.++ (seq.unit 16) (seq.unit 18))))
  (define-fun t2 () (Seq Int)
    (seq.++ (seq.unit 16) (seq.unit 18)))
  (define-fun n () Int
    3)
  (define-fun t1 () (Seq Int)
    (seq.++ (seq.unit 16) (seq.unit 18)))
)

这个模型是错误的。 (seq.extract s 0 (- n 1)) 应该是 [14; 16] 而不是 [16; 18].

是我理解错了什么还是Z3的错误？

Answer 1

顺序逻辑在 z3 中发生了很多变化，自 z3 的 rise4fun 版本发布以来修复了许多错误。在最近的构建中，我得到：

sat
(model
  (define-fun s () (Seq Int)
    (seq.++ (seq.unit 4) (seq.unit 4) (seq.unit 4)))
  (define-fun t2 () (Seq Int)
    (seq.++ (seq.unit 4) (seq.unit 4)))
  (define-fun t1 () (Seq Int)
    (seq.++ (seq.unit 4) (seq.unit 4)))
  (define-fun n () Int
    3)
)

这对我来说是正确的。

长话短说：rise4fun 的 z3 版本对于这个问题来说太旧了，而且有 bug。看看您是否可以从 https://github.com/Z3Prover/z3/releases

下载更新的版本（甚至每晚构建）

Z3 给出的序列模型错误

Wrong model given by Z3 for sequence

z3