(rewriter.sort_sums) solution soundness issue

[merlinsun]

Hi,
For this instance, z3 eb2ee34 incorrectly gives sat.

$ z3 small.smt2
unsat
$ z3 rewriter.sort_sums=true small.smt2
sat
$ cat small.smt2
(declare-const x Real)
(declare-fun a () Real)
(declare-fun v () Real)
(declare-fun ex () Real)
(assert (exists ((t Real)) (< (- 1) ex)))
(assert (forall ((e Real)) (exists ((V Real)) (= (* ex ex (+ (* v a) ex)) (+ x (* e e (- 1)))))))
(check-sat)

[zhendongsu]

It should be a dup of #2650.

z3 rewriter.sort_sums=true small.smt2 nlsat.check_lemmas=true also leads to:

ASSERTION VIOLATION
File: ../src/nlsat/nlsat_solver.cpp
Line: 905
UNEXPECTED CODE WAS REACHED.