(set-option :smt.phase_selection 5)
(set-option :proof true)
(set-option :model_validate true)
(declare-fun a () Real)
(assert (> (/ 2 a) (/ 1 a) 0))
(check-sat)
(check-sat)
(get-model)

[648] % z3debug small.smt2
sat
sat
(model 
  (define-fun a () Real
    0.0)
  (define-fun /0 ((x!0 Real) (x!1 Real)) Real
    (ite (and (= x!0 2.0) (= x!1 0.0)) 2.0
      1.0))
)
[649] % z3 small.smt2
unknown
sat
(error "line 7 column 10: an invalid model was generated")
(model 
  (define-fun a () Real
    0.0)
)
[650] % 
[650] % cat small.smt2
(set-option :smt.phase_selection 5)
(set-option :proof true)
(set-option :model_validate true)
(declare-fun a () Real)
(assert (> (/ 2 a) (/ 1 a) 0))
(check-sat)
(check-sat)
(get-model)