Issue with tactic

[merlinsun]

Hi,
For this following instance, z3 c2610cb yields unsat with (check-sat-using qe2), while cvc5 gives sat.

$ cat test.smt2
(declare-fun a () Int)  
(declare-fun b () Int)   
(declare-fun c () Int)     
(declare-fun d () Bool) 
(declare-fun e () (Array Bool Bool))  
(assert (forall ((f (Array Int Bool)) (g Int)) (=> (=> (= g c) (distinct e (store e d false))) (select (store (store f 1 true) b false) a))))   
(check-sat) 
(check-sat-using qe2) 
$ z3 test.smt2
unknown
unsat
$ cvc5 test.smt2
sat