Weird array quantification behavior -- smallest example

[DavidLDill]

;; Are there flags that could make this work better? Any other ideas?
;; z3 --version
;; Z3 version 4.11.2 - 64 bit
;; This is greatly reduced from a larger example. Array quantification
;; does not seem to work well. MBQI doesn't help.
;; My z3 returns "unknown" immediately. It does not seem
;; to be trying very hard.
;; This is frustrating, because it could literally use anything for T2
;; and Q(x) = true for all x, and it would find a model
;; If we change the consequent to (not (select Q x)), it comes back
;; "sat" immediately.

(declare-sort C 0)
(declare-const Q (Array C Bool))

(assert
(forall ( (T2 (Array C Bool)) )
(forall ((x C))
(=> (select T2 x)
(select Q x)))))

(check-sat)

[NikolajBjorner]

I think there are some updates since the version you are using.
It goes through for me in the current version.

MBQI has been dealing with various issues when using quantified arrays.
For this example, was likely that z3 didn't track how lambda terms creating during instantiation were not tracked correctly.
I am therefore closing it as already fixed.
Overall MBQI was first designed for the array property fragment where arrays are encoded using first-order functions.

The array free version of this is

(declare-sort C 0)
(declare-sort BArray 0)
(declare-fun sel (BArray C) Bool)

(declare-const Q BArray)
(assert
(forall ( (T2 BArray) ) (forall ((x C)) (=> (sel T2 x) (sel Q x)))))
(check-sat)

Side note: z3 arrays allow lambda expressions as arrays. So every lambda term can be used as an array.

[DavidLDill]

I confirmed that a more recent release returns "sat" very quickly.

Here is a somewhat less reduced example with the same property that Q = (lambda ((x C)) true) satisfies it.

If I move the existential quantifier to top level, it is "sat".

(declare-sort C 0)

(assert
(forall ((T1 (Array C Bool)))
(exists ((Q (Array C Bool)))
(forall ((x C))
(=> (select T1 x)
(select Q x))))))

(check-sat)

[NikolajBjorner]

It is hitting some areas related to arrays and MBQI that are not well supported in the legacy core.
It solves with small patches, but I wouldn't apply them without a lot of testing.
(It also solves with a new core "sat.smt=true" which contains a fresh reimplementation of MBQI, but the new core is typically much worse still)