How to use Z3 on formulas with quantifiers over sets?

Question

I have a simple formulas with quantifiers over sets of arrays, Z3(4.3.2) returns "unknown".

(assert (forall ((a (Array Int Int)) (b (Array Int Int))) (=> (forall ((i Int)) (= (select a i) (select b i))) (= a b))))
(check-sat)

The verbose is:

(simplifier :num-exprs 12 :num-asts 185 :time 0.00 :before-memory 2.49 :after-memory 2.49)
(smt.simplifier-done)
(smt.searching)
(smt.mbqi)
(smt.simplifier-done)
(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 1)
(smt.simplifier-done)
(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 1)
(smt.mbqi :failed k!1)
(smt.restarting :propagations 0 :decisions 0 :conflicts 0 :restart 100 :agility 0.00)
(tactic-exception "smt tactic failed to show goal to be sat/unsat")

It seems Z3 allow this kind of formulas. Did I miss some tactics to use, from my incomplete understanding of the verbose? Could you help solving this formula?

Answer 1

The Z3 tutorial (Section Quantifiers) describes for which fragments Z3 is complete. The general problem is undecidable.

Regarding your example, Z3 will fail on satisfiable instances that contain quantifiers ranging over arrays. Note that your formula is satisfiable. If we negate it, then Z3 automatically proves it to be unsatisfiable.

(assert (not (forall ((a (Array Int Int)) (b (Array Int Int))) 
             (=> (forall ((i Int)) (= (select a i) (select b i))) (= a b)))))
(check-sat)

Remark: Z3 is essentially a satisfiability checker. To prove a formula F, we show that the negation is unsatisfiable.

Answer 2

Actually, you can try to eliminate the quantifiers at first. Using Tactic 'qe', 'qe-sat' or 'qe-light' may help. I tried it and it seems to be turned into 'True'.