Z3 switching between unknown/unsat by just changing the range sort of array

[daneshvar-amrollahi]

Hi,

I am facing a weird result when using Z3. Consider these two benchmarks written in SMTLIB:

(declare-fun a () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (forall ((fqv (Array (_ BitVec 32) (_ BitVec 8))))
  (= (select a
                (concat (select fqv #x00000003)
                        (concat (select fqv #x00000002)
                                (concat (select fqv #x00000001)
                                        (select fqv #x00000000)))))
        (select b
                (concat (select fqv #x00000003)
                        (concat (select fqv #x00000002)
                                (concat (select fqv #x00000001)
                                        (select fqv #x00000000))))))))

(assert (= false (= (select a #x00000000) (select b #x00000000))))
(check-sat)
(get-model)

and

(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (forall ((fqv (Array (_ BitVec 32) (_ BitVec 8))))
  (= (select a
                (concat (select fqv #x00000003)
                        (concat (select fqv #x00000002)
                                (concat (select fqv #x00000001)
                                        (select fqv #x00000000)))))
        (select b
                (concat (select fqv #x00000003)
                        (concat (select fqv #x00000002)
                                (concat (select fqv #x00000001)
                                        (select fqv #x00000000))))))))

(assert (= false (= (select a #x00000000) (select b #x00000000))))
(check-sat)
(get-model)

Their only difference is in the range of a and b. In the first case, it is a bit-vector of size 32. While in the second case, it is a bit-vector of size 8.

The interesting part is that (check-sat) is returning unsat for the first case, and unknown for the second one.

Is there an explanation for this?

Here is a link where anyone can quickly run this experiment: https://people.csail.mit.edu/cpitcla/z3.wasm/z3.html

[NikolajBjorner]

Is there an explanation for this?

It uses MBI for arrays to find an instantiation for fbv. For some cases it finds a useful instantiation, for other cases it never finds one. It ends up depending on the current equivalence classes of terms. In one case the term 0 is not equivalent to any other term so instantiation doesn't try to generalize 0 to some term. In the other case 0 gets generalized to a term that is currently equal to 0. However, this is counter-productive: using 0 is useful. The other terms that are instantiated with are not useful.
The algorithm for generalization would have to be changed to be either "fair" or take into account a priority that allows it to determine when the generalization is productive.