Z3 fails to find simple sat solution after quantified bitvector assertion (stuck in loop)

[klinvill]

I noticed that if I create my own array type that stores bitvectors and assert the first array update axiom, simple assertions afterwards fail to find a solution (my example below neither returns sat nor unsat but just keeps running):

(declare-sort MyArray)
; Indices into the array
(declare-sort Id)

; Returns the value in the array located at the specified index
(declare-fun index
    (MyArray Id)
    (_ BitVec 8))

; Updates the array so that the provided value is stored at the specified index
(declare-fun upd 
    (MyArray Id (_ BitVec 8))
    MyArray)

; First array update axiom
(assert (forall ((a MyArray) (i Id) (v (_ BitVec 8)))
    (=
        (index (upd a i v) i)
        v)))

(declare-const x Int)
(declare-const y Int)
(echo "")
(echo "Sanity check, should be sat:")
(assert (= x y))
(check-sat)

However, if I instead specify that my array stores a custom sort z3 finds a solution very quickly:

(declare-sort MyArray)
; Indices into the array
(declare-sort Id)
; Values stored in the array
(declare-sort Elem)

; Returns the value in the array located at the specified index
(declare-fun index
    (MyArray Id)
    Elem)

; Updates the array so that the provided value is stored at the specified index
(declare-fun upd 
    (MyArray Id Elem)
    MyArray)

; First array update axiom
(assert (forall ((a MyArray) (i Id) (v Elem))
    (=
        (index (upd a i v) i)
        v)))

(declare-const x Int)
(declare-const y Int)
(echo "")
(echo "Sanity check, should be sat:")
(assert (= x y))
(check-sat)

Is this expected behavior, or a bug? An answerer on stack overflow mentioned that is surprising behavior to them. Is this likely related to a former note from Nikolaj that the quantifier elimination tactic is currently fairly simplistic when it comes to bit-vectors?

[NikolajBjorner]

It has to produce an interpretation for index that is consistent with the update axiom. The search space for interpretations is by finite function tables. The finite function table for when you have bit-vector values of n-bits is at least 2^n.

[klinvill]

Ah ok thanks! I was able to confirm that it finds a solution pretty quickly for small bitvectors ((_ BitVec 4)) but quickly gets untractable to the point that searching for a solution with (_ BitVec 8) runs for at least 7 hours without finding a solution. Is it accurate then to say that using quantifiers with bitvectors to try to find sat is generally not tractable and therefore uninterpreted sorts should be used in place of bitvectors instead if quantifiers must be used?

[NikolajBjorner]

Scalability depends on formulas and it depends on the heuristics available to solve quantifiers.
It is not easy to make general statements.

The essentially uninterpreted fragment does not allow quantified variables in positive positions on either side of an equality.
For example, (= (index (upd a i v) i) v)) uses the quantified variable v on the right side of =. In such cases it cannot find instantiations that are independent of the domain size.

z3 does not attempt to be "smarter". One can learn from examples like these. If the interpretation of upd was \lambda j . ite(j = i, v, index a j), it would quickly be able to establish satisfiability. Similarly with a simplification ordering it may be possible to establish satisfiability without building a model directly.