Quantifiers and Arrays in Z3

Question

Z3 answers with "unknown" when given this code using quantifiers over arrays:

(declare-const ia Int)
(declare-const ib Int)
(declare-const la Int)
(declare-const lb Int)
(declare-const A (Array Int Int))
(declare-const a (Array Int Int))
(declare-const b (Array Int Int))

(assert 
    (exists 
        ((ia_1 Int) (ia_2 Int) (ib_1 Int) (la_0 Int) (lb_0 Int) (A_0 (Array Int Int)) (a_0 (Array Int Int)) (b_0 (Array Int Int)))
        (and (= ia ia_2) (= ib ib_1) (= la la_0) (= lb lb_0) (= A A_0) (= a a_0) (= b b_0) (= ia_1 0) (= ib_1 0) (< ia_1 la_0) (< ib_1 lb_0) (< (select a_0 ia_1) (select b_0 ib_1)) (= ia_2 (+ ia_1 1)))))

(assert 
    (not 
        (exists 
            ((ia_1 Int) (ib_1 Int) (la_0 Int) (lb_0 Int) (A_0 (Array Int Int)) (a_0 (Array Int Int)) (b_0 (Array Int Int)))
            (and (= ia ia_1) (= ib ib_1) (= la la_0) (= lb lb_0) (= A A_0) (= a a_0) (= b b_0) (= ib_1 0)))))

(check-sat)

Is there a way to obtain the correct answer ("unsat") in such a case?

edit: Z3 answers correctly with "sat" if adding, for example, the constraint (= ia_1 0) to the second conjunction.

Answer 1

Here, "unknown" is a "correct" answer. In general, quantifiers over arrays are not decidable (at least not under further assumptions). Z3 gives up on this example because its default quantifier instantiation heuristics don't pick up the right instantiation patterns. For more info see the section on quantifiers in the Z3 tutorial.

We can specify our own instantiation patterns to help Z3, or we can at least restate the problem so that the heuristics find the right patterns automatically. In this case I was successful by rewriting the second quantifier like so:

(assert 
    (forall ((la_0 Int) (lb_0 Int) (A_0 (Array Int Int)))
            (and 
                (= A A_0) 
                (= la la_0) 
                (= lb lb_0)
                (forall ((b_0 (Array Int Int)) (ib_1 Int))
                    (and 
                        (= b b_0)
                        (= ib ib_1)
                        (= ib_1 0)
                        (forall ((a_0 (Array Int Int)) (ia_1 Int))
                            (not (and (= ia ia_1) (= a a_0))))                       
                        )))))

With fewer arguments to each sub-quantifier, chances are better that it will pick up something useful (I think), but that will of course not always be enough.