qe2 qsat incorrect answer

[muchang]

Hi,
For this formula,

(declare-sort S 0)
(assert (forall ((a S) (b S)) (= a b)))
(check-sat)
(check-sat-using (then qe smt))
(check-sat-using (then qe-light smt))
(check-sat-using (then qe_rec smt))
(check-sat-using (then qsat smt))
(check-sat-using (then qe2 smt))

default qe qe-light qe_rec correctly reports sat, while qsat and qe2 incorrectly reports unsat.

OS: Ubuntu 18.04
Revision: a4cc27