Issue with tactic

[merlinsun]

Hi, For this following instance, z3 https://github.com/Z3Prover/z3/commit/cafe3acff1d4aedf2b08a4700574fcb41b4e4355 incorrectly gives unsat with (check-sat-using qe).

$ cat small.smt2 
(declare-fun a () Real)
(assert (and (forall ((v Real)) (= (= a v) (= v 0)))))
(check-sat-using qe)
(check-sat)
$ z3 small.smt2 
unsat
sat

[NikolajBjorner]

Note: this is not related to qel