(declare-fun a () Real) 
(declare-fun b () Real) 
(declare-fun c () Real) 
(declare-fun d () Real) 
(declare-fun e () Real) 
(assert (< (+ (/ (* c c) (* 2.0 e))) d)) 
(assert (= a (+ b c))) 
(check-sat)  

$ z3/build/z3 small.smt2 
sat
(error "line 11 column 10: an invalid model was generated")
$ cat small.smt2 
(set-option :model_validate true)
(set-option :nlsat.reorder false) 
(set-option :rewriter.arith_ineq_lhs true) 
(declare-fun a () Real) 
(declare-fun b () Real) 
(declare-fun c () Real) 
(declare-fun d () Real) 
(declare-fun e () Real) 
(assert (< (+ (/ (* c c) (* 2.0 e))) d)) 
(assert (= a (+ b c))) 
(check-sat)