smt2_solver gives incorrect result on multidimensional arrays

[romainbrenguier]

I encountered a problem on an smt2 instance that I minimized into this example:

; SMT 2

; a = nondet && a < 2
(declare-fun |a| () (_ BitVec 64))
(assert (not (bvuge |a| (_ bv2 64))))

; int input_array[][]
(declare-fun input_array () (Array (_ BitVec 64) (Array (_ BitVec 64) (_ BitVec 64))))

; tmp_array = input_array with a <- (input_array[a] with 0 <- 2)
(define-fun |tmp_array| () (Array (_ BitVec 64) (Array (_ BitVec 64) (_ BitVec 64))) (store input_array |a| (store (select input_array |a|) (_ bv0 64) (_ bv2 64))))

; result_array == {tmp_array[0]; tmp_array[1]}
(declare-fun result_array () (Array (_ BitVec 64) (Array (_ BitVec 64) (_ BitVec 64))))
(assert (= (select result_array (_ bv0 64)) (select |tmp_array| (_ bv0 64))))
(assert (= (select result_array (_ bv1 64)) (select |tmp_array| (_ bv1 64))))

; p == result_array[a][0]
(declare-fun |p| () (_ BitVec 64))
(assert (= |p| (select (select result_array |a|) (_ bv0 64))))

; p != 2
(assert (not (= |p| (_ bv2 64))))

(check-sat)
(exit)
; end of SMT2 file

CBMC version: 5.12
Operating system: 64-bit x86_64 linux
Exact command line resulting in the issue: smt2_solver test.smt2
What behaviour did you expect: this should be unsat, as is confirmed by running z3 on the same file
What happened instead: smt2_solver returns sat