z3 smt.arith.solver=1 and smt.arith.solver=3 give incorrect answer on LRA formula with exists operator

Hi,
For this formula,
```
(declare-fun a () Real)
(declare-fun b () Real)
(assert (exists ((c Real)) (and (or (< b c 0) (> a 0)) (> b 0) (> (+ a b) 0))))
(check-sat)
```
both Z3 smt.arith.solver=1 and smt.arith.solver=3 incorrectly give `unsat`, while this formula should be `sat`.

OS: Ubuntu 18.04
Revision: 1fdde9e
