在两者之间断言相同的属性时，不同的 check-sat 答案

问题描述

给定以下输入

(set-option :auto_config false)
(set-option :smt.mbqi false)

(declare-fun len (Int) Int)
(declare-fun idx (Int Int) Int)
(declare-const x Int)

(define-fun FOO () Bool
  (forall ((i Int)) (!
    (implies
      (and (<= 0 i) (< i (len x)))
      (exists ((j Int)) (!
        (implies
          (and (<= 0 j) (< j (len x)))
          (> (idx x j) 0))))))))

(assert FOO)

; (push)
(assert (not FOO))
(check-sat)
; (pop)

; (push)
(assert (not FOO))
(check-sat)
; (pop)

Z3 4.3.2 x64 报告第一个 check-sat 的 unsat(如预期)，但第二个报告 unknown.如果注释的 push/pop 未注释，则 check-sat 都会产生 unknown.

Z3 4.3.2 x64 reports unsat for the first check-sat (as expected), but unknown for the second. If the commented push/pops are uncommented, both check-sats yield unknown.

我的猜测是，这是一个错误，或者是 Z3 在到达第二个 check-sat 时切换到增量模式的结果.后者也可以解释为什么如果使用 push/pop，两个 check-sat 都会产生 unknown 因为 Z3 会(据我所知)在第一次 push 时切换到增量模式.

My guess is that this is either a bug, or a consequence of Z3 switching to incremental mode when it reaches the second check-sat. The latter could also explain why both check-sats yield unknown if push/pop is used because Z3 will (as far as I understand) switch to incremental mode on first push.

问题:这是错误还是预期后果?

Question: Is it a bug or an expected consequence?

推荐答案

除了 Nikolaj 的回答:是的，这是因为 Z3 切换到不同的求解器，它会更早放弃.我们可以通过设置(set-option :combined_solver.ignore_solver1 true)来达到同样的效果.

In addition to Nikolaj's answer: Yes, this is because Z3 switches to a different solver, which will give up earlier. We can get the same effect by setting (set-option :combined_solver.ignore_solver1 true).

这篇关于在两者之间断言相同的属性时，不同的 check-sat 答案的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！