Problem with arrays that use bit vectors as index sort

[olibeck]

Dear Z3 Team,
I ran into a problem with arrays that use bit vectors as index sort. Z3 returns sat for formulas that I expected to be unsat.
The following code is an example for which the problem occurs for me:

(set-option :random-seed 0)
(set-option :produce-models true)
(set-option :produce-unsat-cores true)
; 
(set-info :status unsat)
(assert (! 
 (let ((?x277 ((as const (Array (_ BitVec 4) String)) "")))
 (let ((?x225 (store ?x277 (_ bv2 4) "a")))
 (let ((?x467 ((as const (Array (_ BitVec 4) String)) "a")))
 (let ((?x146 (store ?x467 (_ bv0 4) "")))
 (= ?x146 ?x225))))) :named a0))
(check-sat)

(get-unsat-core)
(get-info :reason-unknown)

I tested this code on the release version 4.8.12 as well as on the current master branch (96e117d) and both times Z3 returned sat.

OS: Ubuntu 20.04

[NikolajBjorner]

fixed