Consolidated invalid model bugs

$ z3 model_validate=true /tmp/bug.smt2
sat
(error "line 6 column 10: an invalid model was generated")

$ cat /tmp/bug.smt2
(declare-const x Real)
(assert (= x 0.0))
(assert (not (= (^ (* x 2.0) (/ 1.0 x))
                (^ (* 0.0 (/ 1.0 x))
                   (* x (/ 1.0 2.0))))))
(check-sat)