Different check-sat answers when asserting same property in between

Question

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?

score 2 · Answer 1 · answered Mar 20 '15 at 22:41

2

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.

answered Mar 20 '15 at 22:41

Nikolaj Bjorner

8,229
14
15

Is there anything we could do in such a situation (despite giving up incremental solving, we definitely need that)? E.g. prevent the conversion to NNF? – Malte Schwerhoff Apr 22 '15 at 11:24

score 2 · Answer 2 · answered Mar 21 '15 at 17:21

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

answered Mar 21 '15 at 17:21

Christoph Wintersteiger

8,234
1
16
30

Could we somehow encourage the other solver to not give up so early? – Malte Schwerhoff Apr 22 '15 at 11:25

Different check-sat answers when asserting same property in between

2 Answers2

Linked