Unexpected proof failure due to minor input tweak

[RustanLeino]

The SMT input below (very quickly) gives unsat, as expected. The input has the form

... (P or Q) ...
implies
    (P and X    implies    false)                ; (*)
    and
    ((not P)    implies    false)                ; (***)

However, by removing the X, which is not used anywhere, Z3 instead (very quickly) gives unknown. Likewise, if (*) and (**) is replaced by just false (which perhaps is what Z3 ends up doing in the absence of and X), then the answer is again unknown. In other words, it is as if the (*) and (**) prompts Z3 to do the necessary case split on P and then Q. But, since P or Q is already given, I would expect that case split to already be available to Z3. (My hunch is that there's something wrong with the instantiation of quantifiers. Like, the quantifiers don't get appropriately instantiated just from the P or Q.)

I get this behavior with Z3 version 4.13.3 (and also with version 4.12.1).

Input

(set-option :print-success false)
(set-info :smt-lib-version 2.6)

(set-option :auto_config false)
(set-option :type_check true)
(set-option :smt.case_split 3)
(set-option :smt.qi.eager_threshold 100)
(set-option :smt.delay_units true)
(set-option :smt.mbqi false)
(set-option :model.compact false)
(set-option :model.v2 true)
(set-option :pp.bv_literals false)


(declare-sort T@Fuel 0)
(declare-sort T@ORDINAL 0)
(declare-fun P (T@Fuel T@ORDINAL) Bool)
(declare-fun S (T@Fuel) T@Fuel)
(declare-fun CanCallP (T@ORDINAL) Bool)
(declare-fun |ORD#Offset| (T@ORDINAL) Int)
(declare-fun |ORD#Less| (T@ORDINAL T@ORDINAL) Bool)
(declare-fun Q (T@Fuel T@ORDINAL) Bool)
(declare-fun CanCallQ (T@ORDINAL) Bool)
(assert (forall ((fuel T@Fuel) (k T@ORDINAL) ) (!  (=> (CanCallP k) (=> (= 0 (|ORD#Offset| k)) (= (P (S fuel) k) (exists ((|k'| T@ORDINAL) ) (!  (and (|ORD#Less| |k'| k) (P fuel |k'|))
 :pattern ( (P fuel |k'|))
)))))
 :pattern ( (P (S fuel) k))
)))
(assert (forall ((fuel@@0 T@Fuel) (k@@0 T@ORDINAL) ) (!  (=> (CanCallQ k@@0) (=> (= 0 (|ORD#Offset| k@@0)) (= (Q (S fuel@@0) k@@0) (exists ((|k'@@0| T@ORDINAL) ) (!  (and (|ORD#Less| |k'@@0| k@@0) (Q fuel@@0 |k'@@0|))
 :pattern ( (Q fuel@@0 |k'@@0|))
)))))
 :pattern ( (Q (S fuel@@0) k@@0))
)))
(assert (forall ((fuel@@1 T@Fuel) (k@@1 T@ORDINAL) ) (! (= (Q (S fuel@@1) k@@1) (Q fuel@@1 k@@1))
 :pattern ( (Q (S fuel@@1) k@@1))
)))
(assert (forall ((fuel@@2 T@Fuel) (k@@2 T@ORDINAL) ) (! (= (P (S fuel@@2) k@@2) (P fuel@@2 k@@2))
 :pattern ( (P (S fuel@@2) k@@2))
)))
(push 1)
(declare-fun Zero () T@Fuel)
(declare-fun k@@3 () T@ORDINAL)
(declare-fun UnusedUnknonwnBoolean () Bool)

(assert
 (not
  (=>
   (and
    (CanCallP k@@3)
    (=> (not (P (S Zero) k@@3)) (CanCallQ k@@3))
    ; The following line essentially says "P or Q"
    (or (P (S (S Zero)) k@@3) (Q (S (S Zero)) k@@3))
    (forall ((fuel@@3 T@Fuel) (ih_k T@ORDINAL) )
            (! (=> (and (or (P (S fuel@@3) ih_k) (Q (S fuel@@3) ih_k)) (|ORD#Less| ih_k k@@3)) false)
               :pattern ( (Q (S fuel@@3) ih_k))
               :pattern ( (P (S fuel@@3) ih_k))
               ))
    (= (|ORD#Offset| k@@3) 0)
    )

   ; The following proof obligations are:
   ;     (P and UnusedUnknonwnBoolean  implies  false)
   ;     and
   ;     ((not P)  implies  false)
   (and
    (=> (and (P (S (S Zero)) k@@3)
            ; By commenting out the next line, the proof no longer goes through
            UnusedUnknonwnBoolean
            )
       false)
    (=> (and (not (P (S (S Zero)) k@@3))
            )
       false)
    )
   )))
(check-sat)

[RustanLeino]

I have now come across a second example that suffers from this issue. Hence, I'm all the more eager to see a resolution to this. ;)

[NikolajBjorner]

Your eagerness is my command

[CanCebeci]

Hi Rustan. You’re right, the problem is a missing quantifier instantiation, and it’s due to relevancy filtering. Running with smt.relevancy=0 gives unsat.

In the version of the query where (*) and (**) are replaced with false, with relevancy=2 (the default), Z3 can’t close the branch corresponding to the assignment P(1,k)=true, P(2,k)=false, Q(2,k)=true. Without relevancy filtering, that branch closes as follows:

1. k’ < k ∧ P(0, k’), where k’ is fresh [first axiom instantiated with P(1,k)]
2. ~ (∃ k’’. k’’ < k ∧ P(1, k’’)) [first axiom instantiated with ~P(2,k)]
3. ~P(1,k’) [(2) instantiated with k’, (1)]
4. ~P(0,k’) [fourth axiom instantiated with P(1,k’)]
5. conflict between (3), (4)

With relevancy filtering, the instantiation in the second step never happens. Given Q(2,k)=true, the solver assumes P(2,k) to be irrelevant in the current branch (since it is not required to satisfy the disjunction) and so does not propagate it for quantifier instantiation.

When you include (*) but not (**), P(2,k) appears in a position that is not irrelevant in the same branch, so its propagation is not filtered. This works whether or not you comment out UnusedUnknonwnBoolean.

When you include (**) as well and comment out UnusedUnknonwnBoolean, I believe (but have not confirmed) that an earlier rewrite phase essentially replaces (*) and (**) with false.

I'm not sure what would be a good fix here, since relevancy filtering is behaving as intended. One solution is to fix the triggers so that proofs don't depend on irrelevant atoms.

• changing the trigger on line 56 to :pattern ( (P fuel@@3 ih_k)) leads to a different conflict that closes the branch. Perhaps this is the intended conflict? With the current trigger, the quantifier will never produce facts about P(0,k) or Q(0, k). Note that the modified trigger can lead to an instantiation loop (and does so with relevancy=0, running forever).