Different check-sat answers when asserting same pr

问题:

Given the following input

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

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?

回答1:

Good example.

It is a limitation of how Z3 processes the formulas: 1. When using push/pop it does not detect the contradiction among the asserted formulas, instead it converts formulas to negation normal form and skolemizes quantified formulas. 2. When calling check-sat the second time, it does not keep track that the state was not retracted from a previous unsatisfiable state.

It isn't an unsoundness bug, but sure the behavior is not what a user would expect.

回答2:

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