Longstanding soundness bug in Array logic, qflra tactic

[wintered]

[565] % z3-4.8.5 small.smt2 
unsat
sat
[566] % z3-4.8.5 small.smt2 
unsat
sat
[567] % z3-4.8.6 small.smt2 
unsat
sat
[568] % z3-4.8.7 small.smt2 
unsat
sat
[569] % z3 small.smt2 
unsat
sat
[570] % 
[570] % cat small.smt2 
(declare-fun b ((Array Int (Array Int Int))) Bool)
(declare-fun d () (Array Int (Array Int Int)))
(assert (forall ((a (Array Int (Array Int Int)))) (b a)))
(assert (not (b d)))
(check-sat)
(check-sat-using (then qe2 qflra))
[571] %

OS: Ubuntu 18.04
Commit: 9ea1cf3