Interesting UNKNOWN with QF_ABV

[LeventErkok]

I'm curious why the following benchmark:

(set-logic QF_ABV)
(define-fun s1 () (Array (_ BitVec 1) (_ BitVec 1)) (store (store ((as const (Array (_ BitVec 1) (_ BitVec 1))) #b0) #b0 #b0) #b1 #b1))
(define-fun s3 () (Array (_ BitVec 1) (_ BitVec 1)) (store (store ((as const (Array (_ BitVec 1) (_ BitVec 1))) #b1) #b0 #b0) #b1 #b1))
(assert (distinct s1 s3))
(check-sat)
(get-info :reason-unknown)

causes z3 to respond unknown, with the reason:

unknown
(:reason-unknown "smt tactic failed to show goal to be sat/unsat (incomplete (theory array))")

If you change the logic to ALL, it correctly responds unsat.

While this isn't necessarily a big deal, I'm curious why QF_ABV logic isn't able to decide this rather simple query.

(Not that it's relevant; but cvc5 returns unsat with either logic.)