(rewriter.flat=false) Solution soundness issue on QF_NRA formula

[muchang]

For this formula, z3 incorrectly gives sat with rewriter.flat=false:

[634] % z3release small.smt2
unsat
[635] % z3release rewriter.flat=false small.smt2
sat
[636] % 
[636] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun c () Real)
(declare-fun k () Real)
(declare-fun f () Real)
(declare-fun i () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun j () Real)
(declare-fun p () Real)
(declare-fun l () Real)
(assert (not (exists ((m Real)) (=> (= (<= 0 m (/ (- (- a
 102.63866249241141) (* 227.8039164317522 c)) (- 557.7326656771409)))
 (>= (+ (* (- (/ e f)) m) l) 0 (+ (* (- (/ e f)) m) l))) (> g (/ (* l
 l) p j)) (> (/ e f) 0) (>= (+ (* (- (/ e f)) d) l) 0)))))
(assert (= a (+ (* 227.8039164317522 c) (* (- 557.7326656771409) h)) (/ b h)))
(assert (= d h k p i))
(check-sat)
[637] %

Commit: e16acd0