Hi,
For this formula,

(declare-fun a () Real)
(assert (= (/ (* 2 a) a) (/ a a) 1))
(check-sat)

Z3 reports unsat, while CVC4 reports sat.
If I feed this model to Z3:

(define-fun a () Real 0.0)

Z3 reports sat

OS: Ubuntu 18.04
Revision: d95b549