Brittle use of quantifiers

[RustanLeino]

The SMT2 input below exhibits brittle behavior in how quantifiers are instantiated or used. We frequently see this kind of brittleness through Dafny, but it's been difficult to construct a small repro. Here is one!

Description of the problem

The formula to be verified essentially has the form

A &&     ; marked (**0) in the input below
B &&     ; marked (**1) in the input below
...
==>
; C &&   ; (**2)
D        ; (**3)

(but with the proof goal negated in the usual way).

As is, this formula is not verified (that is, Z3 returns unknown). However, there are two different ways to make Z3 verify it (that is, to return unsat).

• One way to make Z3 prove the formula is to uncomment C. That may not seem so odd. But it is, because B is a universal quantifier whose matching pattern is matched by D. Hence, Z3 ought to instantiate B. And that instantiation would then give D <==> C. This should let Z3 meet the proof goal by proving C, just as if C had been given at (**2) in the input.
• The other way to make Z3 prove the formula is to remove A. Removing an antecedent ought to make a proof be more difficult, but in this case, removing the antecedent lets Z3 find the proof. What's even more odd is that the property stated by A is, logically, not useful in the proof, so whether or not A is included ought not matter.

From the looks of it, there's something about this input that affects which quantifiers are triggered and used. It ought to be that the formula would be proved valid whether or not A and C are included in the input.

Versions and options

I have used Z3 version 4.12.1 to get the behaviors I described above. However, a colleague used Z3 version 4.13.0 (on a slightly larger version of this example) and got the same results.

Note that the example requires trigger-based quantifiers. That is, :auto_config and :smt.mbqi are set to false.

More unusually, the input sets

(set-option :smt.case_split 3)
(set-option :smt.qi.eager_threshold 100)
(set-option :smt.delay_units true)
(set-option :smt.arith.solver 2)

These are the options that Dafny uses (via Boogie). The example does not use arithmetic, so I doubt the :smt.arith.solver setting matters. I understand what :smt.qi.eager_threshold does, and removing it does not affect this example.

I do not understand what :smt.case_split 3 and :smt.delay_units true do. These are settings that Dafny and Boogie have used for over a decade. The :smt.case_split 3 setting does make a difference in this example. In particular, if this setting is omitted, then:

• If A is included, then Z3 fails to verify the input, regardless of whether or not C is included.
• If A is removed, then Z3 verifies the input, regardless of whether or not C is included.

So, while the buggy behavior is affected by :smt.case_split 3, this setting does not seem to be the one that causes the buggy behavior.

The 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.arith.solver 2)
(set-option :smt.mbqi false)
(set-option :model.compact false)
(set-option :model.v2 true)
(set-option :pp.bv_literals false)
; done setting options


(declare-sort T@Box 0)
(declare-fun |Set#Union| ((Array T@Box Bool) (Array T@Box Bool)) (Array T@Box Bool))
(declare-fun |Set#Disjoint| ((Array T@Box Bool) (Array T@Box Bool)) Bool)
(declare-fun |Set#Difference| ((Array T@Box Bool) (Array T@Box Bool)) (Array T@Box Bool))
(declare-sort T@ref 0)
(declare-sort T@Ty 0)
(declare-fun $Is_824 (T@ref T@Ty) Bool)
(declare-fun Tclass._module.Mutex? () T@Ty)
(declare-fun null () T@ref)
(declare-fun dtype (T@ref) T@Ty)
(declare-fun $Is_2110 ((Array T@Box Bool) T@Ty) Bool)
(declare-fun TSet (T@Ty) T@Ty)
(declare-fun $IsBox (T@Box T@Ty) Bool)
(declare-sort T@Field 0)
(declare-fun $Unbox_833 (T@Box) T@ref)
(declare-fun _module.Mutex.data () T@Field)
(declare-fun $IsGoodHeap ((Array T@ref (Array T@Field T@Box))) Bool)
(declare-fun Tclass._module.OwnedU32 () T@Ty)
(declare-fun Tclass._module.Object () T@Ty)
(declare-fun Tclass._module.Object? () T@Ty)
(declare-fun Tclass._module.OwnedU32? () T@Ty)
(declare-fun Tclass._module.MutexGuardU32 () T@Ty)
(declare-fun Tclass._module.MutexGuardU32? () T@Ty)
(declare-fun Tclass._module.Mutex () T@Ty)
(declare-fun $Box_833 (T@ref) T@Box)
(declare-fun |Set#UnionOne| ((Array T@Box Bool) T@Box) (Array T@Box Bool))
(declare-fun $Box_2585 ((Array T@Box Bool)) T@Box)
(declare-fun $Unbox_2642 (T@Box) (Array T@Box Bool))
(declare-fun |Set#Empty| () (Array T@Box Bool))
(declare-fun Tclass._module.OwnedObject? () T@Ty)


; (**0)
; By REMOVING the following assumption, the proof goal is met!
(assert (forall ((a (Array T@Box Bool)) (b (Array T@Box Bool)) ) (!  (=> (|Set#Disjoint| a b) (= (|Set#Difference| (|Set#Union| a b) a) b))
 :pattern ( (|Set#Union| a b))
)))


; (**1)
(assert (forall ((v (Array T@Box Bool)) (t0 T@Ty) ) (!
   (=
    ($Is_2110 v (TSet t0))
    (forall ((bx T@Box) ) (!
       (=> (select v bx) ($IsBox bx t0))
       :pattern ( (select v bx))
       )))
   :pattern ( ($Is_2110 v (TSet t0)))
)))



(assert (forall (($o T@ref) ) (! (= ($Is_824 $o Tclass._module.Mutex?)  (or (= $o null) (= (dtype $o) Tclass._module.Mutex?)))
 :pattern ( ($Is_824 $o Tclass._module.Mutex?))
)))
(assert (forall (($h (Array T@ref (Array T@Field T@Box))) ($o@@0 T@ref) ) (!  (=> (and (and ($IsGoodHeap $h) (not (= $o@@0 null))) (= (dtype $o@@0) Tclass._module.Mutex?)) ($Is_824 ($Unbox_833 (select (select $h $o@@0) _module.Mutex.data)) Tclass._module.OwnedU32))
 :pattern ( ($Unbox_833 (select (select $h $o@@0) _module.Mutex.data)))
)))
(assert (forall ((|c#0| T@ref) ) (! (= ($Is_824 |c#0| Tclass._module.Object)  (and ($Is_824 |c#0| Tclass._module.Object?) (not (= |c#0| null))))
 :pattern ( ($Is_824 |c#0| Tclass._module.Object))
 :pattern ( ($Is_824 |c#0| Tclass._module.Object?))
)))
(assert (forall ((|c#0@@0| T@ref) ) (! (= ($Is_824 |c#0@@0| Tclass._module.OwnedU32)  (and ($Is_824 |c#0@@0| Tclass._module.OwnedU32?) (not (= |c#0@@0| null))))
 :pattern ( ($Is_824 |c#0@@0| Tclass._module.OwnedU32))
 :pattern ( ($Is_824 |c#0@@0| Tclass._module.OwnedU32?))
)))
(assert (forall ((|c#0@@1| T@ref) ) (! (= ($Is_824 |c#0@@1| Tclass._module.MutexGuardU32)  (and ($Is_824 |c#0@@1| Tclass._module.MutexGuardU32?) (not (= |c#0@@1| null))))
 :pattern ( ($Is_824 |c#0@@1| Tclass._module.MutexGuardU32))
 :pattern ( ($Is_824 |c#0@@1| Tclass._module.MutexGuardU32?))
)))
(assert (forall ((|c#0@@2| T@ref) ) (! (= ($Is_824 |c#0@@2| Tclass._module.Mutex)  (and ($Is_824 |c#0@@2| Tclass._module.Mutex?) (not (= |c#0@@2| null))))
 :pattern ( ($Is_824 |c#0@@2| Tclass._module.Mutex))
 :pattern ( ($Is_824 |c#0@@2| Tclass._module.Mutex?))
)))
(assert (forall ((bx@@0 T@Box) ) (!  (=> ($IsBox bx@@0 Tclass._module.MutexGuardU32) (and (= ($Box_833 ($Unbox_833 bx@@0)) bx@@0) ($Is_824 ($Unbox_833 bx@@0) Tclass._module.MutexGuardU32)))
 :pattern ( ($IsBox bx@@0 Tclass._module.MutexGuardU32))
)))
(assert (forall ((a@@0 (Array T@Box Bool)) (x T@Box) (o T@Box) ) (! (= (select (|Set#UnionOne| a@@0 x) o)  (or (= o x) (select a@@0 o)))
 :pattern ( (select (|Set#UnionOne| a@@0 x) o))
)))
(assert (forall ((v@@0 (Array T@Box Bool)) (t T@Ty) ) (! (= ($IsBox ($Box_2585 v@@0) t) ($Is_2110 v@@0 t))
 :pattern ( ($IsBox ($Box_2585 v@@0) t))
)))
(assert (forall ((v@@1 T@ref) (t@@0 T@Ty) ) (! (= ($IsBox ($Box_833 v@@1) t@@0) ($Is_824 v@@1 t@@0))
 :pattern ( ($IsBox ($Box_833 v@@1) t@@0))
)))
(assert (forall ((x@@0 T@Box) ) (! (= ($Box_2585 ($Unbox_2642 x@@0)) x@@0)
 :pattern ( ($Unbox_2642 x@@0))
)))
(assert (forall ((x@@1 T@Box) ) (! (= ($Box_833 ($Unbox_833 x@@1)) x@@1)
 :pattern ( ($Unbox_833 x@@1))
)))
(assert (forall ((o@@0 T@Box) ) (!  (not (select |Set#Empty| o@@0))
 :pattern ( (select |Set#Empty| o@@0))
)))
(assert (forall (($o@@1 T@ref) ) (!  (=> ($Is_824 $o@@1 Tclass._module.OwnedObject?) ($Is_824 $o@@1 Tclass._module.Object?))
 :pattern ( ($Is_824 $o@@1 Tclass._module.OwnedObject?))
)))
(assert (forall (($o@@2 T@ref) ) (!  (=> ($Is_824 $o@@2 Tclass._module.OwnedU32?) ($Is_824 $o@@2 Tclass._module.OwnedObject?))
 :pattern ( ($Is_824 $o@@2 Tclass._module.OwnedU32?))
)))
(assert (forall (($o@@3 T@ref) ) (!  (=> ($Is_824 $o@@3 Tclass._module.MutexGuardU32?) ($Is_824 $o@@3 Tclass._module.OwnedObject?))
 :pattern ( ($Is_824 $o@@3 Tclass._module.MutexGuardU32?))
)))
(assert (forall ((a@@1 (Array T@Box Bool)) (b@@0 (Array T@Box Bool)) (o@@1 T@Box) ) (! (= (select (|Set#Union| a@@1 b@@0) o@@1)  (or (select a@@1 o@@1) (select b@@0 o@@1)))
 :pattern ( (select (|Set#Union| a@@1 b@@0) o@@1))
)))
(push 1)
(declare-fun ControlFlow (Int Int) Int)
(declare-fun this.data@0 () T@Box)
(declare-fun $Heap () (Array T@ref (Array T@Field T@Box)))
(declare-fun this () T@ref)
(declare-fun s@0 () (Array T@Box Bool))
(declare-fun union@0 () (Array T@Box Bool))
(declare-fun |guards#0| () (Array T@Box Bool))
(set-info :boogie-vc-id MyFunction)
(set-option :timeout 0)
(set-option :rlimit 0)
(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.arith.solver 2)
(set-option :smt.mbqi false)
(set-option :model.compact false)
(set-option :model.v2 true)
(set-option :pp.bv_literals false)




(assert (not
   (let ((anon0_correct
          (=>
           (and
            (= this.data@0 (select (select $Heap this) _module.Mutex.data))
            (= s@0 (|Set#UnionOne| |Set#Empty| this.data@0))
            (= union@0 (|Set#Union| |guards#0| s@0))
            )
           (and
            ; Here are two proof obligations, (**2) and (**3). Both verify. But if (**2) is commented out, then
            ; (**3) no longer verifies. In other words, (**2) acts as a lemma for (**3) -- nothing odd with
            ; that. The odd thing, however, is that (**2) is a simple consequence of instantiating the axiom (**1)
            ; above, since (**3) should trigger the matching pattern of axiom (**1).

            ; (**2)
;            (forall ((bx@@1 T@Box) ) (!
;                (=>
;                 (select union@0 bx@@1)
;                 ($IsBox bx@@1 Tclass._module.Object))
;                :pattern ( (select union@0 bx@@1))
;            ))

            ; (**3)
            ($Is_2110 union@0 (TSet Tclass._module.Object))
        ))))
     (let ((PreconditionGeneratedEntry_correct
            (=>
             (and
              ($IsGoodHeap $Heap)
              (not (= this null))
              ($Is_824 this Tclass._module.Mutex)
              ($Is_2110 |guards#0| (TSet Tclass._module.MutexGuardU32))
              )
             anon0_correct)))
PreconditionGeneratedEntry_correct))
))



(check-sat)
(get-info :reason-unknown)
(get-info :rlimit)
(pop 1)

[RustanLeino]

Anyone got any thoughts about this one? It's a major issue for Dafny.